diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-09 11:07:58 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-09 11:07:58 -0800 |
| commit | 6f8820fb95ea7918aec1826f343f8b868bc3a25d (patch) | |
| tree | 3a0b5796484ce4164288f1ea56bc5a84889b8c63 /src/base/wlc | |
| parent | 6a997172df35e0c41578d5081ec70911a3823cc1 (diff) | |
| download | abc-6f8820fb95ea7918aec1826f343f8b868bc3a25d.tar.gz abc-6f8820fb95ea7918aec1826f343f8b868bc3a25d.tar.bz2 abc-6f8820fb95ea7918aec1826f343f8b868bc3a25d.zip | |
%pdra: count the number of reused clauses
Diffstat (limited to 'src/base/wlc')
| -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 ); |