Renamed Aig_ManForEachPi/Po to be ...Ci/Co and Aig_ObjCreatePi/Po to be ...Ci/Co.

7 files changed, 35 insertions, 35 deletions

diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 6b36fe30..57d6e7d0 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/int/intCheck.c
@@ -67,13 +67,13 @@ Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
     Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
     // create variables for register outputs
     Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pFrames );
+        pObj->pData = Aig_ObjCreateCi( pFrames );
     // add timeframes
     for ( f = 0; f < nFrames; f++ )
     {
         // create PI nodes for this frame
         Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -84,7 +84,7 @@ Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
         Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
         {
             pObjLo->pData = pObjLi->pData;
-            Aig_ObjCreatePo( pFrames, (Aig_Obj_t *)pObjLo->pData );
+            Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLo->pData );
         }
     }
     Aig_ManCleanup( pFrames );
@@ -240,7 +240,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
             assert( RetValue );
         }
         // add equality clauses for the flop variables
-        Aig_ManForEachPi( pCnfInt->pMan, pObj, i )
+        Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
         {
             pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
             Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c
index 58b408d7..213c557c 100644
--- a/src/proof/int/intContain.c
+++ b/src/proof/int/intContain.c
@@ -121,7 +121,7 @@ Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t **
     *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
     Saig_ManForEachLo( pAig, pObj, i )
     {
-        pObj->pData = Aig_ObjCreatePi( pFrames );
+        pObj->pData = Aig_ObjCreateCi( pFrames );
         Vec_PtrPush( *pvMapReg, pObj->pData );
     }
     // add timeframes
@@ -129,7 +129,7 @@ Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t **
     {
         // create PI nodes for this frame
         Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -165,14 +165,14 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
     // create the PIs
     Aig_ManCleanData( pOld );
     Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( pOld, pObj, i )
+    Aig_ManForEachCi( pOld, pObj, i )
         pObj->pData = ppNewPis[i];
     // duplicate internal nodes
     Aig_ManForEachNode( pOld, pObj, i )
         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     // add one PO to new
     pObj = Aig_ManPo( pOld, 0 );
-    Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
+    Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
 }
 
 
@@ -287,7 +287,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
 
     // get the counter-example
     vPis = Vec_IntAlloc( 100 );
-    Aig_ManForEachPi( pCnf->pMan, pObj, k )
+    Aig_ManForEachCi( pCnf->pMan, pObj, k )
         Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] );
     assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) );
     pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize );
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 9ba8c9df..22e689f4 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -61,7 +61,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
     {
         // create PI nodes for this frame
         Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -76,7 +76,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
     }
     // create POs for the output of the last frame
     pObj = Aig_ManPo( pAig, 0 );
-    Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+    Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     Aig_ManCleanup( pFrames );
     return pFrames;
 }
diff --git a/src/proof/int/intDup.c b/src/proof/int/intDup.c
index 551473ef..adc692cb 100644
--- a/src/proof/int/intDup.c
+++ b/src/proof/int/intDup.c
@@ -52,9 +52,9 @@ Aig_Man_t * Inter_ManStartInitState( int nRegs )
     ppInputs = ABC_ALLOC( Aig_Obj_t *, nRegs );
     p = Aig_ManStart( nRegs );
     for ( i = 0; i < nRegs; i++ )
-        ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) );
+        ppInputs[i] = Aig_Not( Aig_ObjCreateCi(p) );
     pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
-    Aig_ObjCreatePo( p, pRes );
+    Aig_ObjCreateCo( p, pRes );
     ABC_FREE( ppInputs );
     return p;
 }
@@ -83,8 +83,8 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pNew );
+    Aig_ManForEachCi( p, pObj, i )
+        pObj->pData = Aig_ObjCreateCi( pNew );
     // set registers
     pNew->nTruePis = p->nTruePis;
     pNew->nTruePos = Saig_ManConstrNum(p);
@@ -98,12 +98,12 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
     {
         if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
             continue;
-        Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+        Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
     }
 
     // create register inputs with MUXes
     Saig_ManForEachLi( p, pObj, i )
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
     Aig_ManCleanup( pNew );
     return pNew;
 }
@@ -133,11 +133,11 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
+    Aig_ManForEachCi( p, pObj, i )
     {
         if ( i == Saig_ManPiNum(p) )
-            pCtrl = Aig_ObjCreatePi( pNew );
-        pObj->pData = Aig_ObjCreatePi( pNew );
+            pCtrl = Aig_ObjCreateCi( pNew );
+        pObj->pData = Aig_ObjCreateCi( pNew );
     }
     // set registers
     pNew->nRegs    = fAddFirstPo? 0 : p->nRegs;
@@ -152,14 +152,14 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     {
         if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
             continue;
-        Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+        Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
     }
 
     // add the PO
     if ( fAddFirstPo )
     {
         pObj = Aig_ManPo( p, 0 );
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
     }
     else
     {
@@ -168,7 +168,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
         {
             pObj = Aig_Mux( pNew, pCtrl, (Aig_Obj_t *)pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
     //        pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
-            Aig_ObjCreatePo( pNew, pObj );
+            Aig_ObjCreateCo( pNew, pObj );
         }
     }
     Aig_ManCleanup( pNew );
diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c
index 0fbab6cb..8e74d99a 100644
--- a/src/proof/int/intFrames.c
+++ b/src/proof/int/intFrames.c
@@ -63,14 +63,14 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
     else
     {
         Saig_ManForEachLo( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
     }
     // add timeframes
     for ( f = 0; f < nFrames; f++ )
     {
         // create PI nodes for this frame
         Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
+            pObj->pData = Aig_ObjCreateCi( pFrames );
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
@@ -79,7 +79,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
         {
             if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
                 continue;
-            Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+            Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
         }
         if ( f == nFrames - 1 )
             break;
@@ -94,13 +94,13 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
     if ( fAddRegOuts )
     {
         Saig_ManForEachLi( pAig, pObj, i )
-            Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+            Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     }
     // create the only PO of the manager
     else
     {
         pObj = Aig_ManPo( pAig, 0 );
-        Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+        Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     }
     Aig_ManCleanup( pFrames );
     return pFrames;
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index 139c9bbd..c37cb2c6 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -113,7 +113,7 @@ sat_solver * Inter_ManDeriveSatSolver(
     }
     else
     {
-        Aig_ManForEachPi( pInter, pObj, i )
+        Aig_ManForEachCi( pInter, pObj, i )
         {
             pObj2 = Saig_ManLo( pAig, i );
 
@@ -137,7 +137,7 @@ sat_solver * Inter_ManDeriveSatSolver(
     Vec_IntClear( vVarsAB );
     if ( fUseBackward )
     {
-        Aig_ManForEachPo( pFrames, pObj, i )
+        Aig_ManForEachCo( pFrames, pObj, i )
         {
             assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );
             Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
@@ -155,7 +155,7 @@ sat_solver * Inter_ManDeriveSatSolver(
     }
     else
     {
-        Aig_ManForEachPi( pFrames, pObj, i )
+        Aig_ManForEachCi( pFrames, pObj, i )
         {
             if ( i == Aig_ManRegNum(pAig) )
                 break;
diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c
index 7c011426..6164a389 100644
--- a/src/proof/int/intM114p.c
+++ b/src/proof/int/intM114p.c
@@ -87,7 +87,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
             assert( 0 );
     }
     // connector clauses
-    Aig_ManForEachPi( pInter, pObj, i )
+    Aig_ManForEachCi( pInter, pObj, i )
     {
         pObj2 = Saig_ManLo( pAig, i );
         Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
@@ -109,7 +109,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
             assert( 0 );
     }
     // connector clauses
-    Aig_ManForEachPi( pFrames, pObj, i )
+    Aig_ManForEachCi( pFrames, pObj, i )
     { 
         if ( i == Aig_ManRegNum(pAig) )
             break;
@@ -296,7 +296,7 @@ Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapR
     Vec_IntFree( vLiterals );
     Vec_IntFree( vClauses );
     Vec_IntFree( vResolvent );
-    Aig_ObjCreatePo( p, pInter );
+    Aig_ObjCreateCo( p, pInter );
     Aig_ManCleanup( p );
     return p;
 }
@@ -372,7 +372,7 @@ Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots,
 
     assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
     Vec_PtrFree( vInters );
-    Aig_ObjCreatePo( p, pInter );
+    Aig_ObjCreateCo( p, pInter );
     Aig_ManCleanup( p );
     assert( Aig_ManCheck(p) );
     return p;