Changing the ordering of arguments in two iterators.

12 files changed, 57 insertions, 26 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