diff options
Diffstat (limited to 'src/base/wlc/wlcAbs.c')
-rw-r--r-- | src/base/wlc/wlcAbs.c | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 79da6235..cb30fff1 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1028,6 +1028,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL; Vec_Int_t * vBlacks = NULL; int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1; + int nTotalCla = 0; // start the bitmap to mark objects that cannot be abstracted because of refinement // currently, this bitmap is empty because abstraction begins without refinement Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) ); @@ -1247,6 +1248,13 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) // spurious CEX, continue solving vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + if ( vClauses && pPars->fVerbose ) + { + int i; + Vec_Ptr_t * vVec; + Vec_VecForEachLevel( vClauses, vVec, i ) + nTotalCla += Vec_PtrSize( vVec ); + } Pdr_ManStop( pPdr ); @@ -1291,6 +1299,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Abc_PrintTime( 1, "Time", tTotal ); if ( pPars->fVerbose ) + Abc_Print( 1, "PDRA reused %d clauses.\n", nTotalCla ); + if ( pPars->fVerbose ) { ABC_PRTP( "PDR ", tPdr, tTotal ); ABC_PRTP( "CEX Refine ", tCbr, tTotal ); |