summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/pdr')
-rw-r--r--src/proof/pdr/pdr.h1
-rw-r--r--src/proof/pdr/pdrCore.c106
-rw-r--r--src/proof/pdr/pdrInt.h3
-rw-r--r--src/proof/pdr/pdrInv.c2
-rw-r--r--src/proof/pdr/pdrMan.c102
-rw-r--r--src/proof/pdr/pdrSat.c2
-rw-r--r--src/proof/pdr/pdrTsim.c112
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 13:27:07 +0000