diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/pdr/pdr.h | 1 | ||||
-rw-r--r-- | src/proof/pdr/pdrCore.c | 106 | ||||
-rw-r--r-- | src/proof/pdr/pdrInt.h | 3 | ||||
-rw-r--r-- | src/proof/pdr/pdrInv.c | 2 | ||||
-rw-r--r-- | src/proof/pdr/pdrMan.c | 102 | ||||
-rw-r--r-- | src/proof/pdr/pdrSat.c | 2 | ||||
-rw-r--r-- | src/proof/pdr/pdrTsim.c | 112 |
7 files changed, 208 insertions, 120 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 9f9ef238..18b059c6 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -53,6 +53,7 @@ struct Pdr_Par_t_ int fTwoRounds; // use two rounds for generalization int fMonoCnf; // monolythic CNF int fNewXSim; // updated X-valued simulation + int fFlopPrio; // use structural flop priorities int fDumpInv; // dump inductive invariant int fUseSupp; // use support in the invariant int fShortest; // forces bug traces to be shortest diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 38792ef8..cfc79d85 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -63,6 +63,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->fSkipDown = 1; // apply down in generalization pPars->fCtgs = 0; // handle CTGs in down pPars->fMonoCnf = 0; // monolythic CNF + pPars->fFlopPrio = 0; // use structural flop priorities pPars->fNewXSim = 0; // updated X-valued simulation pPars->fDumpInv = 0; // dump inductive invariant pPars->fUseSupp = 1; // using support variables in the invariant @@ -313,7 +314,7 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube ) int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube ) { int * pOrder; - int i, j, n, Lit, RetValue; + int i, j, Lit, RetValue; Pdr_Set_t * pCubeTmp; // perform generalization if ( p->pPars->fSkipGeneral ) @@ -341,19 +342,14 @@ int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube ) if ( RetValue == 0 ) continue; - // remove j-th entry - for ( n = j; n < (*ppCube)->nLits-1; n++ ) - pOrder[n] = pOrder[n+1]; - j--; - // success - update the cube *ppCube = Pdr_SetCreateFrom( pCubeTmp = *ppCube, i ); Pdr_SetDeref( pCubeTmp ); assert( (*ppCube)->nLits > 0 ); - i--; - // get the ordering by decreasing priorit + // get the ordering by decreasing priority pOrder = Pdr_ManSortByPriority( p, *ppCube ); + j--; } return 0; } @@ -423,7 +419,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, { assert( pCubeMin->Lits[i] >= 0 ); assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); - Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 ); + Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); } Vec_VecPush( p->vClauses, l, pCubeMin ); // consume ref @@ -456,14 +452,14 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, return 0; if ( p->pPars->fVeryVerbose ) { - printf("Intersection:\n"); - ZPdr_SetPrint( *ppCube ); + printf("Intersection:\n"); + ZPdr_SetPrint( *ppCube ); } if ( Pdr_SetIsInit( *ppCube, -1 ) ) { - if ( p->pPars->fVeryVerbose ) - printf ("Failed initiation\n"); - return 0; + if ( p->pPars->fVeryVerbose ) + printf ("Failed initiation\n"); + return 0; } RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 ); if ( RetValue == -1 ) @@ -497,7 +493,7 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin ) { Pdr_Set_t * pCubeMin, * pCubeTmp = NULL, * pPred = NULL, * pCubeCpy = NULL; - int i, j, n, Lit, RetValue; + int i, j, Lit, RetValue; abctime clk = Abc_Clock(); int * pOrder; int added = 0; @@ -546,9 +542,9 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP // try removing this literal Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; if ( p->pPars->fSkipDown ) - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 ); else - RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1 ); + RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1 ); if ( RetValue == -1 ) { Pdr_SetDeref( pCubeMin ); @@ -557,52 +553,47 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP pCubeMin->Lits[i] = Lit; if ( RetValue == 0 ) { - if ( p->pPars->fSkipDown ) - continue; - pCubeCpy = Pdr_SetCreateFrom ( pCubeMin, i ); - RetValue = ZPdr_ManDown ( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added ); - if ( p->pPars->fCtgs ) - //CTG handling code messes up with the internal order array + if ( p->pPars->fSkipDown ) + continue; + pCubeCpy = Pdr_SetCreateFrom ( pCubeMin, i ); + RetValue = ZPdr_ManDown ( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added ); + if ( p->pPars->fCtgs ) + //CTG handling code messes up with the internal order array + pOrder = Pdr_ManSortByPriority( p, pCubeMin ); + if ( RetValue == -1 ) + { + Pdr_SetDeref( pCubeMin ); + Pdr_SetDeref( pCubeCpy ); + Pdr_SetDeref( pPred ); + return -1; + } + if ( RetValue == 0 ) + { + if ( keep ) + Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 ); + if ( pCubeCpy ) + Pdr_SetDeref( pCubeCpy ); + continue; + } + //Inductive subclause + added = 0; + Pdr_SetDeref( pCubeMin ); + pCubeMin = pCubeCpy; + assert( pCubeMin->nLits > 0 ); pOrder = Pdr_ManSortByPriority( p, pCubeMin ); - if ( RetValue == -1 ) - { - Pdr_SetDeref( pCubeMin ); - Pdr_SetDeref( pCubeCpy ); - Pdr_SetDeref( pPred ); - return -1; - } - if ( RetValue == 0 ) - { - if ( keep ) - Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 ); - if ( pCubeCpy ) - Pdr_SetDeref( pCubeCpy ); + j = -1; continue; - } - //Inductive subclause - added = 0; - Pdr_SetDeref( pCubeMin ); - pCubeMin = pCubeCpy; - assert( pCubeMin->nLits > 0 ); - pOrder = Pdr_ManSortByPriority( p, pCubeMin ); - j = -1; - continue; } added = 0; - // remove j-th entry - for ( n = j; n < pCubeMin->nLits-1; n++ ) - pOrder[n] = pOrder[n+1]; - j--; - // success - update the cube pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i ); Pdr_SetDeref( pCubeTmp ); assert( pCubeMin->nLits > 0 ); - i--; - // get the ordering by decreasing priorit + // get the ordering by decreasing priority pOrder = Pdr_ManSortByPriority( p, pCubeMin ); + j--; } if ( p->pPars->fTwoRounds ) @@ -628,19 +619,14 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP if ( RetValue == 0 ) continue; - // remove j-th entry - for ( n = j; n < pCubeMin->nLits-1; n++ ) - pOrder[n] = pOrder[n+1]; - j--; - // success - update the cube pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i ); Pdr_SetDeref( pCubeTmp ); assert( pCubeMin->nLits > 0 ); - i--; - // get the ordering by decreasing priorit + // get the ordering by decreasing priority pOrder = Pdr_ManSortByPriority( p, pCubeMin ); + j--; } } @@ -762,7 +748,7 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube ) { assert( pCubeMin->Lits[i] >= 0 ); assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) ); - Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 ); + Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift ); } Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref p->nCubes++; diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index 89b6f0d0..dae20f0c 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -82,6 +82,7 @@ struct Pdr_Man_t_ Vec_Wec_t * vVLits; // CNF literals // data representation int iOutCur; // current output + int nPrioShift;// priority shift Vec_Ptr_t * vCexes; // counter-examples for each output Vec_Ptr_t * vSolvers; // SAT solvers Vec_Vec_t * vClauses; // clauses by timeframe @@ -121,6 +122,8 @@ struct Pdr_Man_t_ int nQueCur; int nQueMax; int nQueLim; + int nXsimRuns; + int nXsimLits; // runtime abctime timeToStop; abctime timeToStopOne; diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 8b04c53b..16d98a36 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -467,6 +467,8 @@ void Pdr_ManReportInvariant( Pdr_Man_t * p ) Vec_Ptr_t * vCubes; int kStart = Pdr_ManFindInvariantStart( p ); vCubes = Pdr_ManCollectCubes( p, kStart ); +// Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (%.2f)\n", +// kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), 1.0*p->nXsimLits/p->nXsimRuns ); Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) ); Vec_PtrFree( vCubes ); diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 31446290..6fe4c28d 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "pdrInt.h" +#include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START @@ -33,6 +34,94 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* + Synopsis [Structural analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls, int * pnPrioShift ) +{ + Vec_Int_t * vRes = NULL; + Gia_Obj_t * pObj; + int MaxEntry = 0; + int i, * pPerm; + // create flop costs + Vec_Int_t * vCosts = Vec_IntStart( Gia_ManRegNum(p) ); + Gia_ManCreateRefs(p); + Gia_ManForEachRo( p, pObj, i ) + { + Vec_IntWriteEntry( vCosts, i, Gia_ObjRefNum(p, pObj) ); + MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) ); + } + MaxEntry++; + ABC_FREE( p->pRefs ); + // add costs due to MUX inputs + if ( fMuxCtrls ) + { + int fVerbose = 0; + Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) ); + Gia_Obj_t * pCtrl, * pData1, * pData0; + int nCtrls = 0, nDatas = 0, nBoth = 0; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjIsMuxType(pObj) ) + continue; + pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 ); + pCtrl = Gia_Regular(pCtrl); + pData1 = Gia_Regular(pData1); + pData0 = Gia_Regular(pData0); + Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 ); + Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 ); + Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 ); + } + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) ) + Vec_IntAddToEntry( vCosts, i, 2*MaxEntry ); + //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + // Vec_IntAddToEntry( vCosts, i, MaxEntry ); + MaxEntry *= 3; + // print out + if ( fVerbose ) + { + Gia_ManForEachRo( p, pObj, i ) + { + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) ) + nCtrls++; + if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + nDatas++; + if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) ) + nBoth++; + } + printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth ); + } + Vec_BitFree( vCtrls ); + Vec_BitFree( vDatas ); + } + *pnPrioShift = 1 + Abc_Base2Log( MaxEntry ); + // create ordering based on costs + pPerm = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) ); + vRes = Vec_IntAllocArray( pPerm, Vec_IntSize(vCosts) ); + Vec_IntFree( vCosts ); + vCosts = Vec_IntInvert( vRes, -1 ); + Vec_IntFree( vRes ); +//Vec_IntPrint( vCosts ); + return vCosts; +} +Vec_Int_t * Pdr_ManDeriveFlopPriorities( Aig_Man_t * pAig, int fMuxCtrls, int * pnPrioShift ) +{ + Gia_Man_t * pGia = Gia_ManFromAigSimple(pAig); + Vec_Int_t * vRes = Pdr_ManDeriveFlopPriorities2(pGia, fMuxCtrls, pnPrioShift); + Gia_ManStop( pGia ); + return vRes; +} + +/**Function************************************************************* + Synopsis [Creates manager.] Description [] @@ -56,7 +145,13 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio if ( !p->pPars->fMonoCnf ) p->vVLits = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) ); // internal use - p->vPrio = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) ); // priority flops + p->nPrioShift = 0; + if ( vPrioInit ) + p->vPrio = vPrioInit; + else if ( pPars->fFlopPrio ) + p->vPrio = Pdr_ManDeriveFlopPriorities(pAig, 0, &p->nPrioShift); + else + p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) ); p->vLits = Vec_IntAlloc( 100 ); // array of literals p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots @@ -69,7 +164,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->vRes = Vec_IntAlloc( 100 ); // final result p->pCnfMan = Cnf_ManStart(); // ternary simulation - p->pTxs = Txs_ManStart( p, pAig, p->vPrio ); + p->pTxs = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL; // additional AIG data-members if ( pAig->pFanData == NULL ) Aig_ManFanoutStart( pAig ); @@ -151,7 +246,8 @@ void Pdr_ManStop( Pdr_Man_t * p ) // CNF manager Cnf_ManStop( p->pCnfMan ); // terminary simulation - Txs_ManStop( p->pTxs ); + if ( p->pPars->fNewXSim ) + Txs_ManStop( p->pTxs ); // internal use Vec_IntFreeP( &p->vPrio ); // priority flops Vec_IntFree( p->vLits ); // array of literals diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index 936a8f90..b9403e6f 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -366,6 +366,8 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr else *ppPred = Pdr_ManTernarySim( p, k, pCube ); p->tTsim += Abc_Clock() - clk; + p->nXsimLits += (*ppPred)->nLits; + p->nXsimRuns++; } RetValue = 0; } diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 43f2ddb0..0bcb6e0c 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -404,67 +404,65 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL ); assert( RetValue ); -#if 1 - // try removing high-priority flops - Vec_IntClear( vCi2Rem ); - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + // iteratively remove flops + if ( p->pPars->fFlopPrio ) { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) - continue; - Vec_IntClear( vUndo ); - if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) - Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); - else - Pdr_ManExtendUndo( p->pAig, vUndo ); - } - // try removing low-priority flops - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) - { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) - continue; - Vec_IntClear( vUndo ); - if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) - Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); - else - Pdr_ManExtendUndo( p->pAig, vUndo ); - } -#else - // try removing low-priority flops - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) - { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) - continue; - Vec_IntClear( vUndo ); - if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) - Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); - else - Pdr_ManExtendUndo( p->pAig, vUndo ); + // collect flops and sort them by priority + Vec_IntClear( vRes ); + Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); + Vec_IntPush( vRes, Entry ); + } + Vec_IntSelectSortCost( Vec_IntArray(vRes), Vec_IntSize(vRes), vPrio ); + + // try removing flops starting from low-priority to high-priority + Vec_IntClear( vCi2Rem ); + Vec_IntForEachEntry( vRes, Entry, i ) + { + pObj = Aig_ManCi( p->pAig, Saig_ManPiNum(p->pAig) + Entry ); + assert( Saig_ObjIsLo( p->pAig, pObj ) ); + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } } - // try removing high-priority flops - Vec_IntClear( vCi2Rem ); - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + else { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) - continue; - Vec_IntClear( vUndo ); - if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) - Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); - else - Pdr_ManExtendUndo( p->pAig, vUndo ); + // try removing low-priority flops first + Vec_IntClear( vCi2Rem ); + Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); + if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) + continue; + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } + // try removing high-priority flops next + Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); + if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) + continue; + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } } -#endif if ( p->pPars->fVeryVerbose ) Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); |