luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding structural flop priority heuristics in 'pdr'.

This commit is contained in:
Alan Mishchenko 2017-02-03 19:51:53 -08:00
parent a2cebd3e20
commit 45bf0369a8
8 changed files with 214 additions and 122 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/base/abci/abc.c
View File

@ -26008,7 +26008,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmusipdegoncvwzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmuysipdegoncvwzh" ) ) != EOF )
{
switch ( c )
{
@ -26126,6 +26126,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'u':
pPars->fNewXSim ^= 1;
break;
case 'y':
pPars->fFlopPrio ^= 1;
break;
case 's':
pPars->fShortest ^= 1;
break;
@ -26194,7 +26197,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmusipdegoncvwzh]\n" );
Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmuysipdegoncvwzh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka IC3)\n" );
Abc_Print( -2, "\t pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@ -26212,6 +26215,7 @@ usage:
Abc_Print( -2, "\t-r : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
Abc_Print( -2, "\t-u : toggle updated X-valued simulation [default = %s]\n", pPars->fNewXSim? "yes": "no" );
Abc_Print( -2, "\t-y : toggle using structural flop priorities [default = %s]\n", pPars->fFlopPrio? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );
Abc_Print( -2, "\t-i : toggle clause pushing from an intermediate timeframe [default = %s]\n", pPars->fShiftStart? "yes": "no" );
Abc_Print( -2, "\t-p : toggle reusing proof-obligations in the last timeframe [default = %s]\n", pPars->fReuseProofOblig? "yes": "no" );

1
src/proof/pdr/pdr.h
View File

@ -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

106
src/proof/pdr/pdrCore.c
View File

@ -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++;

3
src/proof/pdr/pdrInt.h
View File

@ -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;

2
src/proof/pdr/pdrInv.c
View File

@ -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 );

102
src/proof/pdr/pdrMan.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "pdrInt.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
@ -31,6 +32,94 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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.]
@ -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

2
src/proof/pdr/pdrSat.c
View File

@ -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;
}

112
src/proof/pdr/pdrTsim.c
View File

@ -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 );
// 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 low-priority flops
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 );
}
}
#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 );
}
// try removing high-priority flops
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 );
}
#endif
if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );