diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-22 17:57:19 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-22 17:57:19 -0800 |
| commit | f01c63f712a31726af27340b6255fc1ffbee87b7 (patch) | |
| tree | e614ccf71680832407d0b0d238ac9381c182bbfc | |
| parent | 2f90e5e15d8308a9cbebdc15976f5b5b8d3d8032 (diff) | |
| download | abc-f01c63f712a31726af27340b6255fc1ffbee87b7.tar.gz abc-f01c63f712a31726af27340b6255fc1ffbee87b7.tar.bz2 abc-f01c63f712a31726af27340b6255fc1ffbee87b7.zip | |
working on %pdra -m
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 27 |
1 files changed, 24 insertions, 3 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index e33424f7..b22f9128 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -302,6 +302,17 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec return nNodes; } +static int Wlc_NtkUnmarkRefinement( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark ) +{ + Wlc_Obj_t * pObj; int i, nNodes = 0; + Wlc_NtkForEachObjVec( vRefine, p, pObj, i ) + { + Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pObj), 1 ); + ++nNodes; + } + return nNodes; +} + /**Function************************************************************* Synopsis [Computes the map for remapping flop IDs used in the clauses.] @@ -480,9 +491,19 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Pdr_ManStop( pPdr ); // update the set of objects to be un-abstracted - nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); - if ( pPars->fVerbose ) - printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + if ( pPars->fMFFC ) + { + nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes ); + } + else + { + nNodes = Wlc_NtkUnmarkRefinement( p, vRefine, vUnmark ); + if ( pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pCex->iFrame, Vec_IntSize(vRefine) ); + + } Vec_IntFree( vRefine ); Abc_CexFree( pCex ); Aig_ManStop( pAig ); |