From f01c63f712a31726af27340b6255fc1ffbee87b7 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Wed, 22 Feb 2017 17:57:19 -0800 Subject: working on %pdra -m --- src/base/wlc/wlcAbs.c | 27 ++++++++++++++++++++++++--- 1 file changed, 24 insertions(+), 3 deletions(-) (limited to 'src') 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 ); -- cgit v1.2.3