Changing the ordering of arguments in two iterators.

16 files changed, 82 insertions, 51 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 655c0c99..a0216f37 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -419,20 +419,15 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
 // iterator over all objects, including those currently not used
 #define Aig_ManForEachObj( p, pObj, i )                                         \
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
+// iterator over the objects whose IDs are stored in an array
+#define Aig_ManForEachObjVec( vIds, p, pObj, i )                               \
+    for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))), 1); i++ )
 // iterator over all nodes
 #define Aig_ManForEachNode( p, pObj, i )                                        \
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
 // iterator over all nodes
 #define Aig_ManForEachExor( p, pObj, i )                                        \
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
-// iterator over the nodes whose IDs are stored in the array
-#define Aig_ManForEachNodeVec( p, vIds, pObj, i )                               \
-    for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
-// iterator over the nodes in the topological order
-#define Aig_ManForEachNodeInOrder( p, pObj )                                    \
-    for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1];     \
-          p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1);                  \
-          p->iNext = p->pOrderData[2*p->iPrev+1] )
 
 // these two procedures are only here for the use inside the iterator
 static inline int     Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId )  { assert(ObjId < p->nFansAlloc);  return p->pFanData[5*ObjId];                         }
diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c
index 87ea8f69..eca17d40 100644
--- a/src/aig/aig/aigJust.c
+++ b/src/aig/aig/aigJust.c
@@ -259,7 +259,7 @@ void Aig_ManJustExperiment( Aig_Man_t * pAig )
     pPack = Aig_ManPackStart( pAig );
     vNodes = Aig_ManPackConstNodes( pPack );
 //    Aig_ManForEachPo( pAig, pObj, i )
-    Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
+    Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
     {
         if ( pObj->fPhase ) // const 1
         {
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index a80277d5..6ca3082d 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -27,6 +27,12 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+// iterator over the nodes in the topological order
+#define Aig_ManForEachNodeInOrder( p, pObj )                                    \
+    for ( assert(p->pOrderData), p->iPrev = 0, p->iNext = p->pOrderData[1];     \
+          p->iNext && (((pObj) = Aig_ManObj(p, p->iNext)), 1);                  \
+          p->iNext = p->pOrderData[2*p->iPrev+1] )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/llb/llb1Group.c b/src/aig/llb/llb1Group.c
index 4ebfc3a3..d865c239 100644
--- a/src/aig/llb/llb1Group.c
+++ b/src/aig/llb/llb1Group.c
@@ -318,19 +318,19 @@ Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec
 
     // mark Cut1
     Aig_ManIncrementTravId( pMan->pAig );
-    Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i )
+    Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
         Aig_ObjSetTravIdCurrent( pMan->pAig, pObj );
     // collect unmarked Cut2
-    Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i )
+    Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
         if ( !Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
             Vec_PtrPush( p->vOuts, pObj );
 
     // mark nodes reachable from Cut2
     Aig_ManIncrementTravId( pMan->pAig );
-    Aig_ManForEachNodeVec( pMan->pAig, vCut2, pObj, i )
+    Aig_ManForEachObjVec( vCut2, pMan->pAig, pObj, i )
         Llb_ManGroupMarkNodes_rec( pMan->pAig, pObj );
     // collect marked Cut1
-    Aig_ManForEachNodeVec( pMan->pAig, vCut1, pObj, i )
+    Aig_ManForEachObjVec( vCut1, pMan->pAig, pObj, i )
         if ( Aig_ObjIsTravIdCurrent( pMan->pAig, pObj ) )
             Vec_PtrPush( p->vIns, pObj );
 
diff --git a/src/aig/llb/llb2Driver.c b/src/aig/llb/llb2Driver.c
index 3b4f23fc..041a39d5 100644
--- a/src/aig/llb/llb2Driver.c
+++ b/src/aig/llb/llb2Driver.c
@@ -172,7 +172,7 @@ DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, int Tim
     bRes = Cudd_ReadOne(dd);                                   Cudd_Ref( bRes );
 
     // mark the duplicated flop inputs
-    Aig_ManForEachNodeVec( p, vVarsNs, pObj, i )
+    Aig_ManForEachObjVec( vVarsNs, p, pObj, i )
     {
         if ( !Saig_ObjIsLi(p, pObj) )
             continue;
diff --git a/src/aig/llb/llb2Image.c b/src/aig/llb/llb2Image.c
index caf8f9f7..5baa5c57 100644
--- a/src/aig/llb/llb2Image.c
+++ b/src/aig/llb/llb2Image.c
@@ -262,7 +262,7 @@ DdNode * Llb_ImgComputeCube( Aig_Man_t * pAig, Vec_Int_t * vNodeIds, DdManager *
     int i, TimeStop;
     TimeStop = dd->TimeStop; dd->TimeStop = 0;
     bProd = Cudd_ReadOne(dd);   Cudd_Ref( bProd );
-    Aig_ManForEachNodeVec( pAig, vNodeIds, pObj, i )
+    Aig_ManForEachObjVec( vNodeIds, pAig, pObj, i )
     {
         bProd  = Cudd_bddAnd( dd, bTemp = bProd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)) ); Cudd_Ref( bProd );
         Cudd_RecursiveDeref( dd, bTemp );
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index 25ef8c96..69d741a5 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -340,7 +340,7 @@ Vec_Int_t * Llb_Nonlin4CreateOrder( Aig_Man_t * pAig )
     // mark internal nodes to be used
     Aig_ManCleanMarkA( pAig );
     vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 );
-    Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
+    Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
         pObj->fMarkA = 1;
 printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
 */
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 9d470164..66cf5586 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -337,7 +337,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
         // collect nodes starting from the roots
         Aig_ManIncrementTravId( pAig );
         vRoots = Vec_VecEntryInt( vFrameCos, f );
-        Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
             Saig_ManCbaUnrollCollect_rec( pAig, pObj, 
                 Vec_VecEntryInt(vFrameObjs, f),
                 (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
@@ -355,7 +355,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
     {
         // construct
         vObjs = Vec_VecEntryInt( vFrameObjs, f );
-        Aig_ManForEachNodeVec( pAig, vObjs, pObj, i )
+        Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
         {
             if ( Aig_ObjIsNode(pObj) )
                 pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -382,7 +382,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
             break;
         // transfer
         vRoots = Vec_VecEntryInt( vFrameCos, f );
-        Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
         {
             Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
             if ( *pvReg2Frame )
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
index f2a595f7..a22871b7 100644
--- a/src/aig/saig/saigAbsPba.c
+++ b/src/aig/saig/saigAbsPba.c
@@ -91,7 +91,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
             Vec_IntPush( vRoots, Aig_ObjId(pObj) );
         // collect nodes starting from the roots
         Aig_ManIncrementTravId( pAig );
-        Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
             Saig_ManUnrollForPba_rec( pAig, pObj, 
                 Vec_VecEntryInt( vFrameObjs, f ),
                 (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
@@ -112,7 +112,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
     {
         // construct
         vObjs = Vec_VecEntryInt( vFrameObjs, f );
-        Aig_ManForEachNodeVec( pAig, vObjs, pObj, i )
+        Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
         {
             if ( Aig_ObjIsNode(pObj) )
                 pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -132,7 +132,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
         if ( f == nFrames - 1 )
             break;
         vRoots = Vec_VecEntryInt( vFrameCos, f );
-        Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
         {
             if ( Saig_ObjIsLi(pAig, pObj) )
             {
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index ac397297..5dfcda01 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -321,6 +321,36 @@ Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
     return pCexMin;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCexMinGetCos( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, int f, Vec_Int_t * vTemp )
+{
+    Vec_Int_t * vFrameCisOne;
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_IntClear( vTemp );
+    if ( f == Vec_VecSize(vFrameCis) - 1 )
+    {
+        pObj = Aig_ManPo( pAig, pCex->iPo );
+        Vec_IntPush( vTemp, Aig_ObjId(pObj) );
+        return;
+    }
+    vFrameCisOne = Vec_VecEntryInt( vFrameCis, f+1 );
+    Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
+        if ( Saig_ObjIsLo(pAig, pObj) )
+            Vec_IntPush( vTemp, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 103cdf7b..fce6cf42 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -112,7 +112,7 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
         pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     // create POs
     assert( Vec_IntSize(vPairs) % 2 == 0 );
-    Aig_ManForEachNodeVec( pAig, vPairs, pObj, i )
+    Aig_ManForEachObjVec( vPairs, pAig, pObj, i )
     {
         pObj2  = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
         pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c
index d117c643..b2ea80a6 100644
--- a/src/aig/saig/saigRefSat.c
+++ b/src/aig/saig/saigRefSat.c
@@ -287,7 +287,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
         // collect nodes starting from the roots
         Aig_ManIncrementTravId( pAig );
         vRoots = Vec_VecEntryInt( vFrameCos, f );
-        Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
             Saig_ManUnrollCollect_rec( pAig, pObj, 
                 Vec_VecEntryInt(vFrameObjs, f),
                 (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
@@ -305,7 +305,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
     {
         // construct
         vObjs = Vec_VecEntryInt( vFrameObjs, f );
-        Aig_ManForEachNodeVec( pAig, vObjs, pObj, i )
+        Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
         {
             if ( Aig_ObjIsNode(pObj) )
                 pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -332,7 +332,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
             break;
         // transfer
         vRoots = Vec_VecEntryInt( vFrameCos, f );
-        Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
             Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
     }
     // create output
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index fb7abae9..e707c57e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -451,7 +451,7 @@ static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_At
 #define Abc_NtkForEachObj( pNtk, pObj, i )                                                         \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pObj) = Abc_NtkObj(pNtk, i)), 1); i++ )    \
         if ( (pObj) == NULL ) {} else
-#define Abc_NtkForEachObjVec( pNtk, vIds, pObj, i )                                                \
+#define Abc_NtkForEachObjVec( vIds, pNtk, pObj, i )                                                \
     for ( i = 0; i < Vec_IntSize(vIds) && (((pObj) = Abc_NtkObj(pNtk, Vec_IntEntry(vIds,i))), 1); i++ ) \
         if ( (pObj) == NULL ) {} else
 #define Abc_NtkForEachNet( pNtk, pNet, i )                                                         \
diff --git a/src/base/abci/abcMffc.c b/src/base/abci/abcMffc.c
index 0ffc6f1d..3fb4bdf1 100644
--- a/src/base/abci/abcMffc.c
+++ b/src/base/abci/abcMffc.c
@@ -455,14 +455,14 @@ void Abc_NktMffcPrintInt( char * pFileName, Abc_Ntk_t * pNtk, Vec_Int_t * vRoots
     pFile = fopen( pFileName, "wb" );
     fprintf( pFile, ".model %s_part\n", pNtk->pName );
     fprintf( pFile, ".inputs" );
-    Abc_NtkForEachObjVec( pNtk, vLeaves, pObj, i )
+    Abc_NtkForEachObjVec( vLeaves, pNtk, pObj, i )
         fprintf( pFile, " %s", Abc_ObjName(pObj) );
     fprintf( pFile, "\n" );
     fprintf( pFile, ".outputs" );
-    Abc_NtkForEachObjVec( pNtk, vRoots, pObj, i )
+    Abc_NtkForEachObjVec( vRoots, pNtk, pObj, i )
         fprintf( pFile, " %s", Abc_ObjName(pObj) );
     fprintf( pFile, "\n" );
-    Abc_NtkForEachObjVec( pNtk, vNodes, pObj, i )
+    Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
     {
         fprintf( pFile, ".names" );
         Abc_ObjForEachFanin( pObj, pFanin, k )
@@ -757,12 +757,12 @@ void Abc_NktMffCollectLeafRootInt( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, Vec_Int
     Abc_Obj_t * pObj, * pNext;
     int i, k;
     // mark
-    Abc_NtkForEachObjVec( pNtk, vNodes, pObj, i )
+    Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
         pObj->fMarkA = 1;
     // collect leaves
     Vec_IntClear( vLeaves );
     Abc_NtkIncrementTravId( pNtk );
-    Abc_NtkForEachObjVec( pNtk, vNodes, pObj, i )
+    Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
         Abc_ObjForEachFanin( pObj, pNext, k )
         {
             if ( pNext->fMarkA || Abc_NodeIsTravIdCurrent(pNext) )
@@ -774,7 +774,7 @@ void Abc_NktMffCollectLeafRootInt( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, Vec_Int
     if ( vRoots )
     {
         Vec_IntClear( vRoots );
-        Abc_NtkForEachObjVec( pNtk, vNodes, pObj, i )
+        Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
         {
             Abc_ObjForEachFanout( pObj, pNext, k )
                 if ( !pNext->fMarkA )
@@ -785,7 +785,7 @@ void Abc_NktMffCollectLeafRootInt( Abc_Ntk_t * pNtk, Vec_Int_t * vNodes, Vec_Int
         }
     }
     // unmark
-    Abc_NtkForEachObjVec( pNtk, vNodes, pObj, i )
+    Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
         pObj->fMarkA = 0;
 }
 
@@ -1051,7 +1051,7 @@ Abc_Obj_t * Abc_NktMffcFindBest( Abc_Ntk_t * pNtk, Vec_Int_t * vMarks, Vec_Int_t
     int i, Volume;
     // collect the fanouts of the fanins
     vOuts = Vec_IntAlloc( 100 );
-    Abc_NtkForEachObjVec( pNtk, vIns, pObj, i )
+    Abc_NtkForEachObjVec( vIns, pNtk, pObj, i )
     {
         vOuts2 = (Vec_Int_t *)Vec_PtrEntry( vFanouts, Abc_ObjId(pObj) );
         if ( Vec_IntSize(vOuts2) > 16 )
@@ -1060,7 +1060,7 @@ Abc_Obj_t * Abc_NktMffcFindBest( Abc_Ntk_t * pNtk, Vec_Int_t * vMarks, Vec_Int_t
         Vec_IntFree( vTemp );
     }
     // check the pairs
-    Abc_NtkForEachObjVec( pNtk, vOuts, pPivot2, i )
+    Abc_NtkForEachObjVec( vOuts, pNtk, pPivot2, i )
     {       
         if ( Vec_IntEntry(vMarks, Abc_ObjId(pPivot2)) == 0 )
             continue;
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;