From 6bf50cbb8660616bfc4de4715f55e439465c2603 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Thu, 16 Mar 2017 12:50:27 -0700 Subject: %pdra: added a structural support profiling of PPIs --- src/base/wlc/wlcAbs.c | 117 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 117 insertions(+) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index ca1d14a9..ebe4cbe1 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -54,6 +54,33 @@ int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +void Wlc_NtkAbsGetSupp_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vCiMarks, Vec_Int_t * vSuppRefs, Vec_Int_t * vSuppList ) +{ + int i, iFanin, iObj; + if ( pObj->Mark ) // visited + return; + pObj->Mark = 1; + iObj = Wlc_ObjId( p, pObj ); + if ( Vec_BitEntry( vCiMarks, iObj ) ) + { + if ( vSuppRefs ) + Vec_IntAddToEntry( vSuppRefs, iObj, 1 ); + if ( vSuppList ) + Vec_IntPush( vSuppList, iObj ); + return; + } + Wlc_ObjForEachFanin( pObj, iFanin, i ) + Wlc_NtkAbsGetSupp_rec( p, Wlc_NtkObj(p, iFanin), vCiMarks, vSuppRefs, vSuppList ); +} + +void Wlc_NtkAbsGetSupp( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vCiMarks, Vec_Int_t * vSuppRefs, Vec_Int_t * vSuppList) +{ + assert( vSuppRefs || vSuppList ); + Wlc_NtkCleanMarks( p ); + + Wlc_NtkAbsGetSupp_rec( p, pObj, vCiMarks, vSuppRefs, vSuppList ); +} + int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) { int num = 0; @@ -65,6 +92,92 @@ int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) return num; } +void Wlc_NtkAbsAnalyzeRefine( Wlc_Ntk_t * p, Vec_Int_t * vBlacks, Vec_Bit_t * vUnmark, int * nDisj, int * nNDisj ) +{ + Vec_Bit_t * vCurCis, * vCandCis; + Vec_Int_t * vSuppList; + Vec_Int_t * vDeltaB; + Vec_Int_t * vSuppRefs; + int i, Entry; + Wlc_Obj_t * pObj; + + vCurCis = Vec_BitStart( Wlc_NtkObjNumMax( p ) ); + vCandCis = Vec_BitStart( Wlc_NtkObjNumMax( p ) ); + vDeltaB = Vec_IntAlloc( Vec_IntSize(vBlacks) ); + vSuppList = Vec_IntAlloc( Wlc_NtkCiNum(p) + Vec_IntSize(vBlacks) ); + vSuppRefs = Vec_IntAlloc( Wlc_NtkObjNumMax( p ) ); + + Vec_IntFill( vSuppRefs, Wlc_NtkObjNumMax( p ), 0 ); + + Wlc_NtkForEachCi( p, pObj, i ) + { + Vec_BitWriteEntry( vCurCis, Wlc_ObjId(p, pObj), 1 ) ; + Vec_BitWriteEntry( vCandCis, Wlc_ObjId(p, pObj), 1 ) ; + } + + Vec_IntForEachEntry( vBlacks, Entry, i ) + { + Vec_BitWriteEntry( vCurCis, Entry, 1 ); + if ( !Vec_BitEntry( vUnmark, Entry ) ) + Vec_BitWriteEntry( vCandCis, Entry, 1 ); + else + Vec_IntPush( vDeltaB, Entry ); + } + assert( Vec_IntSize( vDeltaB ) ); + + Wlc_NtkForEachCo( p, pObj, i ) + Wlc_NtkAbsGetSupp( p, pObj, vCurCis, vSuppRefs, NULL ); + + /* + Abc_Print( 1, "SuppCurrentAbs =" ); + Wlc_NtkForEachObj( p, pObj, i ) + if ( Vec_IntEntry(vSuppRefs, i) > 0 ) + Abc_Print( 1, " %d", i ); + Abc_Print( 1, "\n" ); + */ + + Vec_IntForEachEntry( vDeltaB, Entry, i ) + Wlc_NtkAbsGetSupp( p, Wlc_NtkObj(p, Entry), vCandCis, vSuppRefs, NULL ); + + Vec_IntForEachEntry( vDeltaB, Entry, i ) + { + int iSupp, ii; + int fDisjoint = 1; + + Vec_IntClear( vSuppList ); + Wlc_NtkAbsGetSupp( p, Wlc_NtkObj(p, Entry), vCandCis, NULL, vSuppList ); + + //Abc_Print( 1, "SuppCandAbs =" ); + Vec_IntForEachEntry( vSuppList, iSupp, ii ) + { + //Abc_Print( 1, " %d(%d)", iSupp, Vec_IntEntry( vSuppRefs, iSupp ) ); + if ( Vec_IntEntry( vSuppRefs, iSupp ) >= 2 ) + { + fDisjoint = 0; + break; + } + } + //Abc_Print( 1, "\n" ); + + if ( fDisjoint ) + { + //Abc_Print( 1, "PPI[%d] is disjoint.\n", Entry ); + ++(*nDisj); + } + else + { + //Abc_Print( 1, "PPI[%d] is non-disjoint.\n", Entry ); + ++(*nNDisj); + } + } + + Vec_BitFree( vCurCis ); + Vec_BitFree( vCandCis ); + Vec_IntFree( vDeltaB ); + Vec_IntFree( vSuppList ); + Vec_IntFree( vSuppRefs ); +} + static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, Vec_Bit_t * vMark, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars ) { Vec_Int_t * vCores = NULL; @@ -1046,6 +1159,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Vec_Int_t * vBlacks = NULL; int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1; int nTotalCla = 0; + int nDisj = 0, nNDisj = 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) ); @@ -1290,6 +1404,9 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pCex->iFrame, Vec_IntSize(vRefine) ); } + Wlc_NtkAbsAnalyzeRefine( p, vBlacks, vUnmark, &nDisj, &nNDisj ); + if ( pPars->fVerbose ) + Abc_Print( 1, "Refine analysis (total): %d disjoint PPIs and %d non-disjoint PPIs\n", nDisj, nNDisj ); tCbr += Abc_Clock() - clk2; Vec_IntFree( vRefine ); -- cgit v1.2.3 From b9971b2348cd8940cf74db7b3d6e0c7146db6af2 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Thu, 16 Mar 2017 13:33:14 -0700 Subject: added another function for printing wlc --- src/base/wlc/wlcAbs.c | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index ebe4cbe1..23e60b0d 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -54,6 +54,35 @@ int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +void Wlc_NtkPrintNtk( Wlc_Ntk_t * p ) +{ + int i; + Wlc_Obj_t * pObj; + + Abc_Print( 1, "PIs:"); + Wlc_NtkForEachPi( p, pObj, i ) + Abc_Print( 1, " %s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) ); + Abc_Print( 1, "\n\n"); + + Abc_Print( 1, "POs:"); + Wlc_NtkForEachPo( p, pObj, i ) + Abc_Print( 1, " %s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) ); + Abc_Print( 1, "\n\n"); + + Abc_Print( 1, "FO(Fi)s:"); + Wlc_NtkForEachCi( p, pObj, i ) + if ( !Wlc_ObjIsPi( pObj ) ) + Abc_Print( 1, " %s(%s)", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) ); + Abc_Print( 1, "\n\n"); + + Abc_Print( 1, "Objs:\n"); + Wlc_NtkForEachObj( p, pObj, i ) + { + if ( !Wlc_ObjIsCi(pObj) ) + Wlc_NtkPrintNode( p, pObj ) ; + } +} + void Wlc_NtkAbsGetSupp_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vCiMarks, Vec_Int_t * vSuppRefs, Vec_Int_t * vSuppList ) { int i, iFanin, iObj; @@ -107,6 +136,7 @@ void Wlc_NtkAbsAnalyzeRefine( Wlc_Ntk_t * p, Vec_Int_t * vBlacks, Vec_Bit_t * vU vSuppList = Vec_IntAlloc( Wlc_NtkCiNum(p) + Vec_IntSize(vBlacks) ); vSuppRefs = Vec_IntAlloc( Wlc_NtkObjNumMax( p ) ); + Vec_IntFill( vSuppRefs, Wlc_NtkObjNumMax( p ), 0 ); Wlc_NtkForEachCi( p, pObj, i ) @@ -1177,6 +1207,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this } + // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) { -- cgit v1.2.3 From ddd349cf96875baa1194f5f3ba8dcc5304f99572 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Thu, 16 Mar 2017 16:14:45 -0700 Subject: %pdra: created a new manager; refactored --- src/base/wlc/wlcAbs.c | 326 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 326 insertions(+) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 23e60b0d..d5a6ca91 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -45,6 +45,33 @@ struct Int_Pair_t_ int second; }; +typedef struct Wla_Man_t_ Wla_Man_t; +struct Wla_Man_t_ +{ + Pdr_Man_t * pPdr; + Pdr_Par_t * pPdrPars; + Vec_Vec_t * vClauses; + Vec_Int_t * vBlacks; + Aig_Man_t * pAig; + Abc_Cex_t * pCex; + Vec_Int_t * vPisNew; + Vec_Int_t * vRefine; + Gia_Man_t * pGia; + Wlc_Ntk_t * pAbs; + Wlc_Ntk_t * p; + Wlc_Par_t * pPars; + Vec_Bit_t * vUnmark; + + int nIters; + int nTotalCla; + int nDisj; + int nNDisj; + + abctime tPdr; + abctime tCbr; + abctime tPbr; +}; + int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b ) { return (*a)->second < (*b)->second; @@ -1178,7 +1205,305 @@ Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ + +Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla ) +{ + // get abstracted GIA and the set of pseudo-PIs (vPisNew) + if ( pWla->vBlacks == NULL ) + pWla->vBlacks = Wlc_NtkGetBlacks( pWla->p, pWla->pPars ); + else + Wlc_NtkUpdateBlacks( pWla->p, pWla->pPars, &pWla->vBlacks, pWla->vUnmark ); + pWla->pAbs = Wlc_NtkAbs2( pWla->p, pWla->vBlacks, NULL ); + pWla->vPisNew = Vec_IntDup( pWla->vBlacks ); + + return pWla->pAbs; +} + +Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla ) +{ + int nDcFlops; + Gia_Man_t * pTemp; + + pWla->pGia = Wlc_NtkBitBlast( pWla->pAbs, NULL, -1, 0, 0, 0, 0 ); + + // if the abstraction has flops with DC-init state, + // new PIs were introduced by bit-blasting at the end of the PI list + // here we move these variables to be *before* PPIs, because + // PPIs are supposed to be at the end of the PI list for refinement + nDcFlops = Wlc_NtkDcFlopNum(pWla->pAbs); + if ( nDcFlops > 0 ) // DC-init flops are present + { + pWla->pGia = Gia_ManPermuteInputs( pTemp = pWla->pGia, Wlc_NtkCountObjBits(pWla->p, pWla->vPisNew), nDcFlops ); + Gia_ManStop( pTemp ); + } + // if the word-level outputs have to be XORs, this is a place to do it + if ( pWla->pPars->fXorOutput ) + { + pWla->pGia = Gia_ManTransformMiter2( pTemp = pWla->pGia ); + Gia_ManStop( pTemp ); + } + if ( pWla->pPars->fVerbose ) + { + printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pWla->pAbs), Vec_IntSize(pWla->vPisNew) ); + Gia_ManPrintStats( pWla->pGia, NULL ); + } + + // try to prove abstracted GIA by converting it to AIG and calling PDR + pWla->pAig = Gia_ManToAigSimple( pWla->pGia ); + + Wlc_NtkFree( pWla->pAbs ); + + return pWla->pAig; +} + +int Wla_ManSolve( Wla_Man_t * pWla ) +{ + abctime clk; + int RetValue = -1; + + if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat ) + { + Pdr_Man_t * pPdr2; + + if ( Aig_ManAndNum( pWla->pAig ) <= 20000 ) + { + Aig_Man_t * pAigScorr; + Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars; + int nAnds; + + clk = Abc_Clock(); + + Ssw_ManSetDefaultParams( pScorrPars ); + pScorrPars->fStopWhenGone = 1; + pScorrPars->nFramesK = 1; + pAigScorr = Ssw_SignalCorrespondence( pWla->pAig, pScorrPars ); + assert ( pAigScorr ); + nAnds = Aig_ManAndNum( pAigScorr); + Aig_ManStop( pAigScorr ); + + if ( nAnds == 0 ) + { + if ( pWla->pPars->fVerbose ) + Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk ); + return 1; + } + else if ( pWla->pPars->fVerbose ) + { + Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + } + + clk = Abc_Clock(); + + pWla->pPdrPars->fVerbose = 0; + pPdr2 = Pdr_ManStart( pWla->pAig, pWla->pPdrPars, NULL ); + RetValue = IPdr_ManCheckCombUnsat( pPdr2 ); + Pdr_ManStop( pPdr2 ); + pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose; + + pWla->tPdr += Abc_Clock() - clk; + + if ( RetValue == 1 ) + { + if ( pWla->pPars->fVerbose ) + Abc_PrintTime( 1, "ABS becomes combinationally UNSAT. Time", Abc_Clock() - clk ); + return 1; + } + + if ( pWla->pPars->fVerbose ) + Abc_PrintTime( 1, "Check comb. unsat failed. Time", Abc_Clock() - clk ); + } + + clk = Abc_Clock(); + pWla->pPdr = Pdr_ManStart( pWla->pAig, pWla->pPdrPars, NULL ); + if ( pWla->vClauses ) { + assert( Vec_VecSize( pWla->vClauses) >= 2 ); + IPdr_ManRestore( pWla->pPdr, pWla->vClauses, NULL ); + } + + if ( !pWla->vClauses || RetValue != 1 ) + RetValue = IPdr_ManSolveInt( pWla->pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses ); + pWla->pPdr->tTotal += Abc_Clock() - clk; + pWla->tPdr += pWla->pPdr->tTotal; + + pWla->pCex = pWla->pAig->pSeqModel; + pWla->pAig->pSeqModel = NULL; + + // consider outcomes + if ( pWla->pCex == NULL ) + { + assert( RetValue ); // proved or undecided + return RetValue; + } + + // verify CEX + if ( Wlc_NtkCexIsReal( pWla->p, pWla->pCex ) ) + return 0; + + return -1; +} + +void Wla_ManRefine( Wla_Man_t * pWla ) +{ + abctime clk; + int nNodes; + // perform refinement + if ( pWla->pPars->fHybrid || !pWla->pPars->fProofRefine ) + { + clk = Abc_Clock(); + pWla->vRefine = Wlc_NtkAbsRefinement( pWla->p, pWla->pGia, pWla->pCex, pWla->vPisNew ); + pWla->tCbr += Abc_Clock() - clk; + } + else // proof-based only + { + pWla->vRefine = Vec_IntDup( pWla->vPisNew ); + } + if ( pWla->pPars->fProofRefine ) + { + clk = Abc_Clock(); + Wlc_NtkProofRefine( pWla->p, pWla->pPars, pWla->pCex, pWla->vPisNew, &pWla->vRefine ); + pWla->tPbr += Abc_Clock() - clk; + } + + pWla->vClauses = IPdr_ManSaveClauses( pWla->pPdr, 0 ); + if ( pWla->vClauses && pWla->pPars->fVerbose ) + { + int i; + Vec_Ptr_t * vVec; + Vec_VecForEachLevel( pWla->vClauses, vVec, i ) + pWla->nTotalCla += Vec_PtrSize( vVec ); + } + + // update the set of objects to be un-abstracted + clk = Abc_Clock(); + if ( pWla->pPars->fMFFC ) + { + nNodes = Wlc_NtkRemoveFromAbstraction( pWla->p, pWla->vRefine, pWla->vUnmark ); + if ( pWla->pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pWla->pCex->iFrame, Vec_IntSize(pWla->vRefine), nNodes ); + } + else + { + nNodes = Wlc_NtkUnmarkRefinement( pWla->p, pWla->vRefine, pWla->vUnmark ); + if ( pWla->pPars->fVerbose ) + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pWla->pCex->iFrame, Vec_IntSize(pWla->vRefine) ); + + } + Wlc_NtkAbsAnalyzeRefine( pWla->p, pWla->vBlacks, pWla->vUnmark, &pWla->nDisj, &pWla->nNDisj ); + if ( pWla->pPars->fVerbose ) + Abc_Print( 1, "Refine analysis (total): %d disjoint PPIs and %d non-disjoint PPIs\n", pWla->nDisj, pWla->nNDisj ); + pWla->tCbr += Abc_Clock() - clk; + + Pdr_ManStop( pWla->pPdr ); pWla->pPdr = NULL; + Gia_ManStop( pWla->pGia ); pWla->pGia = NULL; + Vec_IntFree( pWla->vPisNew ); pWla->vPisNew = NULL; + Vec_IntFree( pWla->vRefine ); pWla->vRefine = NULL; + Abc_CexFree( pWla->pCex ); pWla->pCex = NULL; + Aig_ManStop( pWla->pAig ); pWla->pAig = NULL; +} + +Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars ) +{ + Wla_Man_t * p = ABC_CALLOC( Wla_Man_t, 1 ); + Pdr_Par_t * pPdrPars; + p->p = pNtk; + p->pPars = pPars; + p->vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(pNtk) ); + + pPdrPars = ABC_CALLOC( Pdr_Par_t, 1 ); + Pdr_ManSetDefaultParams( pPdrPars ); + pPdrPars->fVerbose = pPars->fPdrVerbose; + pPdrPars->fVeryVerbose = 0; + if ( pPars->fPdra ) + { + pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction) + pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization) + pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) + pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this + } + p->pPdrPars = pPdrPars; + + p->nIters = 1; + p->nTotalCla = 0; + p->nDisj = 0; + p->nNDisj = 0; + + return p; +} + +void Wla_ManStop( Wla_Man_t * p ) +{ + if ( p->vBlacks ) Vec_IntFree( p->vBlacks ); + if ( p->pPdr ) Pdr_ManStop( p->pPdr ); + if ( p->pGia ) Gia_ManStop( p->pGia ); + if ( p->vPisNew ) Vec_IntFree( p->vPisNew ); + if ( p->vRefine ) Vec_IntFree( p->vRefine ); + if ( p->pCex ) Abc_CexFree( p->pCex ); + if ( p->pAig ) Aig_ManStop( p->pAig ); + Vec_BitFree( p->vUnmark ); + ABC_FREE( p->pPdrPars ); + ABC_FREE( p ); +} + int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) +{ + abctime clk = Abc_Clock(); + abctime tTotal; + Wla_Man_t * pWla = NULL; + int RetValue = -1; + + pWla = Wla_ManStart( p, pPars ); + + // perform refinement iterations + for ( pWla->nIters = 1; pWla->nIters < pPars->nIterMax; ++pWla->nIters ) + { + if ( pPars->fVerbose ) + printf( "\nIteration %d:\n", pWla->nIters ); + + Wla_ManCreateAbs( pWla ); + Wla_ManBitBlast( pWla ); + + RetValue = Wla_ManSolve( pWla ); + + if ( RetValue != -1 ) + break; + + Wla_ManRefine( pWla ); + } + + // report the result + if ( pPars->fVerbose ) + printf( "\n" ); + printf( "Abstraction " ); + if ( RetValue == 0 ) + printf( "resulted in a real CEX" ); + else if ( RetValue == 1 ) + printf( "is successfully proved" ); + else + printf( "timed out" ); + printf( " after %d iterations. ", pWla->nIters ); + tTotal = Abc_Clock() - clk; + Abc_PrintTime( 1, "Time", tTotal ); + + if ( pPars->fVerbose ) + Abc_Print( 1, "PDRA reused %d clauses.\n", pWla->nTotalCla ); + if ( pPars->fVerbose ) + { + ABC_PRTP( "PDR ", pWla->tPdr, tTotal ); + ABC_PRTP( "CEX Refine ", pWla->tCbr, tTotal ); + ABC_PRTP( "Proof Refine ", pWla->tPbr, tTotal ); + ABC_PRTP( "Misc. ", tTotal - pWla->tPdr - pWla->tCbr - pWla->tPbr, tTotal ); + ABC_PRTP( "Total ", tTotal, tTotal ); + } + + Wla_ManStop( pWla ); + + return RetValue; +} + +/* +int Wlc_NtkPdrAbs2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) { abctime clk = Abc_Clock(); abctime clk2; @@ -1476,6 +1801,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) return RetValue; } +*/ /**Function************************************************************* -- cgit v1.2.3 From 4d7cec5051d741888db0d5ef844b0270dc509830 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Fri, 17 Mar 2017 12:18:39 -0700 Subject: %pdra: disabled an experimental procedure --- src/base/wlc/wlcAbs.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index d5a6ca91..a1c263f4 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -1390,9 +1390,13 @@ void Wla_ManRefine( Wla_Man_t * pWla ) printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pWla->pCex->iFrame, Vec_IntSize(pWla->vRefine) ); } - Wlc_NtkAbsAnalyzeRefine( pWla->p, pWla->vBlacks, pWla->vUnmark, &pWla->nDisj, &pWla->nNDisj ); - if ( pWla->pPars->fVerbose ) + /* + if ( pWla->pPars->fVerbose ) + { + Wlc_NtkAbsAnalyzeRefine( pWla->p, pWla->vBlacks, pWla->vUnmark, &pWla->nDisj, &pWla->nNDisj ); Abc_Print( 1, "Refine analysis (total): %d disjoint PPIs and %d non-disjoint PPIs\n", pWla->nDisj, pWla->nNDisj ); + } + */ pWla->tCbr += Abc_Clock() - clk; Pdr_ManStop( pWla->pPdr ); pWla->pPdr = NULL; -- cgit v1.2.3 From 06a8d505446a3c7557384cf7e818fde61c6cf453 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Fri, 17 Mar 2017 13:04:03 -0700 Subject: %pdra: cleanup, refactor --- src/base/wlc/wlcAbs.c | 405 ++++++-------------------------------------------- 1 file changed, 49 insertions(+), 356 deletions(-) diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 2ec9c84b..c89ed187 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -48,18 +48,13 @@ struct Int_Pair_t_ typedef struct Wla_Man_t_ Wla_Man_t; struct Wla_Man_t_ { - Pdr_Man_t * pPdr; + Wlc_Ntk_t * p; + Wlc_Par_t * pPars; Pdr_Par_t * pPdrPars; Vec_Vec_t * vClauses; Vec_Int_t * vBlacks; - Aig_Man_t * pAig; Abc_Cex_t * pCex; - Vec_Int_t * vPisNew; - Vec_Int_t * vRefine; Gia_Man_t * pGia; - Wlc_Ntk_t * pAbs; - Wlc_Ntk_t * p; - Wlc_Par_t * pPars; Vec_Bit_t * vUnmark; int nIters; @@ -1208,32 +1203,34 @@ Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vF Wlc_Ntk_t * Wla_ManCreateAbs( Wla_Man_t * pWla ) { - // get abstracted GIA and the set of pseudo-PIs (vPisNew) + Wlc_Ntk_t * pAbs; + + // get abstracted GIA and the set of pseudo-PIs (vBlacks) if ( pWla->vBlacks == NULL ) pWla->vBlacks = Wlc_NtkGetBlacks( pWla->p, pWla->pPars ); else Wlc_NtkUpdateBlacks( pWla->p, pWla->pPars, &pWla->vBlacks, pWla->vUnmark ); - pWla->pAbs = Wlc_NtkAbs2( pWla->p, pWla->vBlacks, NULL ); - pWla->vPisNew = Vec_IntDup( pWla->vBlacks ); + pAbs = Wlc_NtkAbs2( pWla->p, pWla->vBlacks, NULL ); - return pWla->pAbs; + return pAbs; } -Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla ) +Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla, Wlc_Ntk_t * pAbs ) { int nDcFlops; Gia_Man_t * pTemp; + Aig_Man_t * pAig; - pWla->pGia = Wlc_NtkBitBlast( pWla->pAbs, NULL, -1, 0, 0, 0, 0, 0 ); + pWla->pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0 ); // if the abstraction has flops with DC-init state, // new PIs were introduced by bit-blasting at the end of the PI list // here we move these variables to be *before* PPIs, because // PPIs are supposed to be at the end of the PI list for refinement - nDcFlops = Wlc_NtkDcFlopNum(pWla->pAbs); + nDcFlops = Wlc_NtkDcFlopNum(pAbs); if ( nDcFlops > 0 ) // DC-init flops are present { - pWla->pGia = Gia_ManPermuteInputs( pTemp = pWla->pGia, Wlc_NtkCountObjBits(pWla->p, pWla->vPisNew), nDcFlops ); + pWla->pGia = Gia_ManPermuteInputs( pTemp = pWla->pGia, Wlc_NtkCountObjBits(pWla->p, pWla->vBlacks), nDcFlops ); Gia_ManStop( pTemp ); } // if the word-level outputs have to be XORs, this is a place to do it @@ -1244,28 +1241,25 @@ Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla ) } if ( pWla->pPars->fVerbose ) { - printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pWla->pAbs), Vec_IntSize(pWla->vPisNew) ); + printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(pWla->vBlacks) ); Gia_ManPrintStats( pWla->pGia, NULL ); } // try to prove abstracted GIA by converting it to AIG and calling PDR - pWla->pAig = Gia_ManToAigSimple( pWla->pGia ); - - Wlc_NtkFree( pWla->pAbs ); + pAig = Gia_ManToAigSimple( pWla->pGia ); - return pWla->pAig; + return pAig; } -int Wla_ManSolve( Wla_Man_t * pWla ) +int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig ) { abctime clk; + Pdr_Man_t * pPdr; int RetValue = -1; if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat ) { - Pdr_Man_t * pPdr2; - - if ( Aig_ManAndNum( pWla->pAig ) <= 20000 ) + if ( Aig_ManAndNum( pAig ) <= 20000 ) { Aig_Man_t * pAigScorr; Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars; @@ -1276,7 +1270,7 @@ int Wla_ManSolve( Wla_Man_t * pWla ) Ssw_ManSetDefaultParams( pScorrPars ); pScorrPars->fStopWhenGone = 1; pScorrPars->nFramesK = 1; - pAigScorr = Ssw_SignalCorrespondence( pWla->pAig, pScorrPars ); + pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars ); assert ( pAigScorr ); nAnds = Aig_ManAndNum( pAigScorr); Aig_ManStop( pAigScorr ); @@ -1297,9 +1291,9 @@ int Wla_ManSolve( Wla_Man_t * pWla ) clk = Abc_Clock(); pWla->pPdrPars->fVerbose = 0; - pPdr2 = Pdr_ManStart( pWla->pAig, pWla->pPdrPars, NULL ); - RetValue = IPdr_ManCheckCombUnsat( pPdr2 ); - Pdr_ManStop( pPdr2 ); + pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL ); + RetValue = IPdr_ManCheckCombUnsat( pPdr ); + Pdr_ManStop( pPdr ); pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose; pWla->tPdr += Abc_Clock() - clk; @@ -1316,19 +1310,20 @@ int Wla_ManSolve( Wla_Man_t * pWla ) } clk = Abc_Clock(); - pWla->pPdr = Pdr_ManStart( pWla->pAig, pWla->pPdrPars, NULL ); + pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL ); if ( pWla->vClauses ) { assert( Vec_VecSize( pWla->vClauses) >= 2 ); - IPdr_ManRestore( pWla->pPdr, pWla->vClauses, NULL ); + IPdr_ManRestore( pPdr, pWla->vClauses, NULL ); } - if ( !pWla->vClauses || RetValue != 1 ) - RetValue = IPdr_ManSolveInt( pWla->pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses ); - pWla->pPdr->tTotal += Abc_Clock() - clk; - pWla->tPdr += pWla->pPdr->tTotal; + RetValue = IPdr_ManSolveInt( pPdr, pWla->pPars->fCheckClauses, pWla->pPars->fPushClauses ); + pPdr->tTotal += Abc_Clock() - clk; + pWla->tPdr += pPdr->tTotal; + pWla->vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + Pdr_ManStop( pPdr ); - pWla->pCex = pWla->pAig->pSeqModel; - pWla->pAig->pSeqModel = NULL; + pWla->pCex = pAig->pSeqModel; + pAig->pSeqModel = NULL; // consider outcomes if ( pWla->pCex == NULL ) @@ -1348,25 +1343,25 @@ void Wla_ManRefine( Wla_Man_t * pWla ) { abctime clk; int nNodes; + Vec_Int_t * vRefine = NULL; // perform refinement if ( pWla->pPars->fHybrid || !pWla->pPars->fProofRefine ) { clk = Abc_Clock(); - pWla->vRefine = Wlc_NtkAbsRefinement( pWla->p, pWla->pGia, pWla->pCex, pWla->vPisNew ); + vRefine = Wlc_NtkAbsRefinement( pWla->p, pWla->pGia, pWla->pCex, pWla->vBlacks ); pWla->tCbr += Abc_Clock() - clk; } else // proof-based only { - pWla->vRefine = Vec_IntDup( pWla->vPisNew ); + vRefine = Vec_IntDup( pWla->vBlacks ); } if ( pWla->pPars->fProofRefine ) { clk = Abc_Clock(); - Wlc_NtkProofRefine( pWla->p, pWla->pPars, pWla->pCex, pWla->vPisNew, &pWla->vRefine ); + Wlc_NtkProofRefine( pWla->p, pWla->pPars, pWla->pCex, pWla->vBlacks, &vRefine ); pWla->tPbr += Abc_Clock() - clk; } - pWla->vClauses = IPdr_ManSaveClauses( pWla->pPdr, 0 ); if ( pWla->vClauses && pWla->pPars->fVerbose ) { int i; @@ -1379,15 +1374,15 @@ void Wla_ManRefine( Wla_Man_t * pWla ) clk = Abc_Clock(); if ( pWla->pPars->fMFFC ) { - nNodes = Wlc_NtkRemoveFromAbstraction( pWla->p, pWla->vRefine, pWla->vUnmark ); + nNodes = Wlc_NtkRemoveFromAbstraction( pWla->p, vRefine, pWla->vUnmark ); if ( pWla->pPars->fVerbose ) - printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pWla->pCex->iFrame, Vec_IntSize(pWla->vRefine), nNodes ); + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pWla->pCex->iFrame, Vec_IntSize(vRefine), nNodes ); } else { - nNodes = Wlc_NtkUnmarkRefinement( pWla->p, pWla->vRefine, pWla->vUnmark ); + nNodes = Wlc_NtkUnmarkRefinement( pWla->p, vRefine, pWla->vUnmark ); if ( pWla->pPars->fVerbose ) - printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pWla->pCex->iFrame, Vec_IntSize(pWla->vRefine) ); + printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pWla->pCex->iFrame, Vec_IntSize(vRefine) ); } /* @@ -1399,12 +1394,9 @@ void Wla_ManRefine( Wla_Man_t * pWla ) */ pWla->tCbr += Abc_Clock() - clk; - Pdr_ManStop( pWla->pPdr ); pWla->pPdr = NULL; + Vec_IntFree( vRefine ); Gia_ManStop( pWla->pGia ); pWla->pGia = NULL; - Vec_IntFree( pWla->vPisNew ); pWla->vPisNew = NULL; - Vec_IntFree( pWla->vRefine ); pWla->vRefine = NULL; Abc_CexFree( pWla->pCex ); pWla->pCex = NULL; - Aig_ManStop( pWla->pAig ); pWla->pAig = NULL; } Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars ) @@ -1439,12 +1431,8 @@ Wla_Man_t * Wla_ManStart( Wlc_Ntk_t * pNtk, Wlc_Par_t * pPars ) void Wla_ManStop( Wla_Man_t * p ) { if ( p->vBlacks ) Vec_IntFree( p->vBlacks ); - if ( p->pPdr ) Pdr_ManStop( p->pPdr ); if ( p->pGia ) Gia_ManStop( p->pGia ); - if ( p->vPisNew ) Vec_IntFree( p->vPisNew ); - if ( p->vRefine ) Vec_IntFree( p->vRefine ); if ( p->pCex ) Abc_CexFree( p->pCex ); - if ( p->pAig ) Aig_ManStop( p->pAig ); Vec_BitFree( p->vUnmark ); ABC_FREE( p->pPdrPars ); ABC_FREE( p ); @@ -1455,6 +1443,9 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) abctime clk = Abc_Clock(); abctime tTotal; Wla_Man_t * pWla = NULL; + Wlc_Ntk_t * pAbs = NULL; + Aig_Man_t * pAig = NULL; + int RetValue = -1; pWla = Wla_ManStart( p, pPars ); @@ -1465,10 +1456,13 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) if ( pPars->fVerbose ) printf( "\nIteration %d:\n", pWla->nIters ); - Wla_ManCreateAbs( pWla ); - Wla_ManBitBlast( pWla ); + pAbs = Wla_ManCreateAbs( pWla ); + + pAig = Wla_ManBitBlast( pWla, pAbs ); + Wlc_NtkFree( pAbs ); - RetValue = Wla_ManSolve( pWla ); + RetValue = Wla_ManSolve( pWla, pAig ); + Aig_ManStop( pAig ); if ( RetValue != -1 ) break; @@ -1506,307 +1500,6 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) return RetValue; } -/* -int Wlc_NtkPdrAbs2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) -{ - abctime clk = Abc_Clock(); - abctime clk2; - abctime tPdr = 0, tCbr = 0, tPbr = 0, tTotal = 0; - Pdr_Man_t * pPdr; - Vec_Vec_t * vClauses = NULL; - 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; - int nDisj = 0, nNDisj = 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) ); - // set up parameters to run PDR - Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; - Pdr_ManSetDefaultParams( pPdrPars ); - pPdrPars->fVerbose = pPars->fPdrVerbose; - pPdrPars->fVeryVerbose = 0; - - if ( pPars->fPdra ) - { - pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction) - pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization) - pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) - pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this - } - - - // perform refinement iterations - for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) - { - Aig_Man_t * pAig; - Abc_Cex_t * pCex; - Vec_Int_t * vPisNew = NULL; - Vec_Int_t * vRefine; - Gia_Man_t * pGia, * pTemp; - Wlc_Ntk_t * pAbs; - - if ( pPars->fVerbose ) - printf( "\nIteration %d:\n", nIters ); - - // get abstracted GIA and the set of pseudo-PIs (vPisNew) - if ( pPars->fAbs2 || pPars->fProofRefine ) - { - if ( vBlacks == NULL ) - vBlacks = Wlc_NtkGetBlacks( p, pPars ); - else - Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark ); - pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew ); - vPisNew = Vec_IntDup( vBlacks ); - } - else - { - if ( nIters == 1 && pPars->nLimit < ABC_INFINITY ) - Wlc_NtkSetUnmark( p, pPars, vUnmark ); - - pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose ); - } - pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0 ); - - // map old flops into new flops - if ( vFfOld ) - { - assert( nGiaFfNumOld >= 0 ); - vMap = Wlc_NtkFlopsRemap( p, vFfOld, vFfNew ); - //Vec_IntPrint( vMap ); - // if reset flop was added in the previous iteration, it will be added again in this iteration - // remap the last flop (reset flop) into the last flop (reset flop) of the current AIG - if ( Vec_IntSize(vMap) + 1 == nGiaFfNumOld ) - Vec_IntPush( vMap, Gia_ManRegNum(pGia)-1 ); - assert( Vec_IntSize(vMap) == nGiaFfNumOld ); - Vec_IntFreeP( &vFfOld ); - } - ABC_SWAP( Vec_Int_t *, vFfOld, vFfNew ); - nGiaFfNumOld = Gia_ManRegNum(pGia); - - // if the abstraction has flops with DC-init state, - // new PIs were introduced by bit-blasting at the end of the PI list - // here we move these variables to be *before* PPIs, because - // PPIs are supposed to be at the end of the PI list for refinement - nDcFlops = Wlc_NtkDcFlopNum(pAbs); - if ( nDcFlops > 0 ) // DC-init flops are present - { - pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops ); - Gia_ManStop( pTemp ); - } - // if the word-level outputs have to be XORs, this is a place to do it - if ( pPars->fXorOutput ) - { - pGia = Gia_ManTransformMiter2( pTemp = pGia ); - Gia_ManStop( pTemp ); - } - if ( pPars->fVerbose ) - { - printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); - Gia_ManPrintStats( pGia, NULL ); - } - Wlc_NtkFree( pAbs ); - // Gia_AigerWrite( pGia, "abs.aig", 0, 0 ); - - // try to prove abstracted GIA by converting it to AIG and calling PDR - pAig = Gia_ManToAigSimple( pGia ); - - - if ( vClauses && pPars->fCheckCombUnsat ) - { - Pdr_Man_t * pPdr2; - - if ( Aig_ManAndNum( pAig ) <= 20000 ) - { - Aig_Man_t * pAigScorr; - Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars; - int nAnds; - - clk2 = Abc_Clock(); - - Ssw_ManSetDefaultParams( pScorrPars ); - pScorrPars->fStopWhenGone = 1; - pScorrPars->nFramesK = 1; - pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars ); - assert ( pAigScorr ); - nAnds = Aig_ManAndNum( pAigScorr); - Aig_ManStop( pAigScorr ); - - if ( nAnds == 0 ) - { - if ( pPars->fVerbose ) - Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 ); - RetValue = 1; - Gia_ManStop( pGia ); - Vec_IntFree( vPisNew ); - Aig_ManStop( pAig ); - break; - } - else if ( pPars->fVerbose ) - { - Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 ); - } - } - - clk2 = Abc_Clock(); - - pPdrPars->fVerbose = 0; - pPdr2 = Pdr_ManStart( pAig, pPdrPars, NULL ); - RetValue = IPdr_ManCheckCombUnsat( pPdr2 ); - Pdr_ManStop( pPdr2 ); - pPdrPars->fVerbose = pPars->fPdrVerbose; - - tPdr += Abc_Clock() - clk2; - - if ( RetValue == 1 ) - { - if ( pPars->fVerbose ) - Abc_PrintTime( 1, "ABS becomes combinationally UNSAT. Time", Abc_Clock() - clk2 ); - Gia_ManStop( pGia ); - Vec_IntFree( vPisNew ); - Aig_ManStop( pAig ); - break; - } - - if ( pPars->fVerbose ) - Abc_PrintTime( 1, "Check comb. unsat failed. Time", Abc_Clock() - clk2 ); - } - - clk2 = Abc_Clock(); - pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); - if ( vClauses ) { - assert( Vec_VecSize( vClauses) >= 2 ); - IPdr_ManRestore( pPdr, vClauses, vMap ); - } - Vec_IntFreeP( &vMap ); - - if ( !vClauses || RetValue != 1 ) - RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses ); - pPdr->tTotal += Abc_Clock() - clk2; - tPdr += pPdr->tTotal; - - pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; - - // consider outcomes - if ( pCex == NULL ) - { - assert( RetValue ); // proved or undecided - Gia_ManStop( pGia ); - Vec_IntFree( vPisNew ); - Pdr_ManStop( pPdr ); - Aig_ManStop( pAig ); - break; - } - - // verify CEX - if ( Wlc_NtkCexIsReal( p, pCex ) ) - { - vRefine = NULL; - Abc_CexFree( pCex ); // return CEX in the future - Pdr_ManStop( pPdr ); - Aig_ManStop( pAig ); - break; - } - - // perform refinement - if ( pPars->fHybrid || !pPars->fProofRefine ) - { - clk2 = Abc_Clock(); - vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew ); - tCbr += Abc_Clock() - clk2; - } - else // proof-based only - { - vRefine = Vec_IntDup( vPisNew ); - } - if ( pPars->fProofRefine ) - { - clk2 = Abc_Clock(); - Wlc_NtkProofRefine( p, pPars, pCex, vPisNew, &vRefine ); - tPbr += Abc_Clock() - clk2; - } - Gia_ManStop( pGia ); - Vec_IntFree( vPisNew ); - if ( vRefine == NULL ) // real CEX - { - Abc_CexFree( pCex ); // return CEX in the future - Pdr_ManStop( pPdr ); - Aig_ManStop( pAig ); - break; - } - - // 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 ); - - // update the set of objects to be un-abstracted - clk2 = Abc_Clock(); - 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) ); - - } - Wlc_NtkAbsAnalyzeRefine( p, vBlacks, vUnmark, &nDisj, &nNDisj ); - if ( pPars->fVerbose ) - Abc_Print( 1, "Refine analysis (total): %d disjoint PPIs and %d non-disjoint PPIs\n", nDisj, nNDisj ); - tCbr += Abc_Clock() - clk2; - - Vec_IntFree( vRefine ); - Abc_CexFree( pCex ); - Aig_ManStop( pAig ); - } - - if ( vBlacks ) - Vec_IntFree( vBlacks ); - Vec_IntFreeP( &vFfOld ); - Vec_BitFree( vUnmark ); - // report the result - if ( pPars->fVerbose ) - printf( "\n" ); - printf( "Abstraction " ); - if ( RetValue == 0 ) - printf( "resulted in a real CEX" ); - else if ( RetValue == 1 ) - printf( "is successfully proved" ); - else - printf( "timed out" ); - printf( " after %d iterations. ", nIters ); - tTotal = Abc_Clock() - clk; - 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 ); - ABC_PRTP( "Proof Refine ", tPbr, tTotal ); - ABC_PRTP( "Misc. ", tTotal - tPdr - tCbr - tPbr, tTotal ); - ABC_PRTP( "Total ", tTotal, tTotal ); - } - - return RetValue; -} -*/ - /**Function************************************************************* Synopsis [Performs abstraction.] -- cgit v1.2.3