summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/pdr/pdrSat.c2
-rw-r--r--src/sat/pdr/pdrTsim.c28
2 files changed, 15 insertions, 15 deletions
diff --git a/src/sat/pdr/pdrSat.c b/src/sat/pdr/pdrSat.c
index 4ba22e84..79a675eb 100644
--- a/src/sat/pdr/pdrSat.c
+++ b/src/sat/pdr/pdrSat.c
@@ -219,7 +219,7 @@ void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t
int iVar, i;
Vec_IntClear( vValues );
pSat = Pdr_ManSolver(p, k);
- Aig_ManForEachNodeVec( p->pAig, vObjIds, pObj, i )
+ Aig_ManForEachObjVec( vObjIds, p->pAig, pObj, i )
{
iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
diff --git a/src/sat/pdr/pdrTsim.c b/src/sat/pdr/pdrTsim.c
index ae457352..6fec1605 100644
--- a/src/sat/pdr/pdrTsim.c
+++ b/src/sat/pdr/pdrTsim.c
@@ -112,7 +112,7 @@ void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiO
Vec_IntClear( vNodes );
Aig_ManIncrementTravId( pAig );
Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
- Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
+ Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes );
}
@@ -166,20 +166,20 @@ int Pdr_ManSimDataInit( Aig_Man_t * pAig,
int i;
// set the CI values
Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE );
- Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
+ Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) );
// set the FOs to remove
if ( vCi2Rem != NULL )
- Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
+ Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
// perform ternary simulation
- Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
+ Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
Pdr_ManExtendOneEval( pAig, pObj );
// transfer results to the output
- Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
+ Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
Pdr_ManExtendOneEval( pAig, pObj );
// check the results
- Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
+ Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) )
return 0;
return 1;
@@ -212,7 +212,7 @@ int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec
// traverse
Vec_IntClear( vVis );
Vec_IntPush( vVis, Aig_ObjId(pObj) );
- Aig_ManForEachNodeVec( pAig, vVis, pObj, i )
+ Aig_ManForEachObjVec( vVis, pAig, pObj, i )
{
Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k )
{
@@ -252,7 +252,7 @@ void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo )
{
Aig_Obj_t * pObj;
int i, Value;
- Aig_ManForEachNodeVec( pAig, vUndo, pObj, i )
+ Aig_ManForEachObjVec( vUndo, pAig, pObj, i )
{
Value = Vec_IntEntry(vUndo, ++i);
assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND );
@@ -277,7 +277,7 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi
int i, Lit;
// mark removed flop outputs
Aig_ManIncrementTravId( pAig );
- Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
+ Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
{
assert( Saig_ObjIsLo( pAig, pObj ) );
Aig_ObjSetTravIdCurrent(pAig, pObj);
@@ -285,7 +285,7 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi
// collect flop outputs that are not marked
Vec_IntClear( vRes );
Vec_IntClear( vPiLits );
- Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
+ Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
{
if ( Saig_ObjIsPi(pAig, pObj) )
{
@@ -322,10 +322,10 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
pBuff[i] = '-';
pBuff[i] = 0;
- Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
+ Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
if ( vCi2Rem )
- Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
+ Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
pBuff[Aig_ObjPioNum(pObj)] = 'x';
printf( "%s\n", pBuff );
ABC_FREE( pBuff );
@@ -402,7 +402,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
// try removing high-priority flops
Vec_IntClear( vCi2Rem );
- Aig_ManForEachNodeVec( p->pAig, vCiObjs, pObj, i )
+ Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
{
if ( !Saig_ObjIsLo( p->pAig, pObj ) )
continue;
@@ -416,7 +416,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
Pdr_ManExtendUndo( p->pAig, vUndo );
}
// try removing low-priority flops
- Aig_ManForEachNodeVec( p->pAig, vCiObjs, pObj, i )
+ Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
{
if ( !Saig_ObjIsLo( p->pAig, pObj ) )
continue;