Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)...

9 files changed, 39 insertions, 39 deletions

diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c
index 57d6e7d0..2b14d8ae 100644
--- a/src/proof/int/intCheck.c
+++ b/src/proof/int/intCheck.c
@@ -112,10 +112,10 @@ Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK )
     p->vAssLits = Vec_IntAlloc( 100 );
     // generate the timeframes 
     p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
-    assert( Aig_ManPiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
-    assert( Aig_ManPoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
+    assert( Aig_ManCiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
+    assert( Aig_ManCoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
     // convert to CNF
-    p->pCnf = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) ); 
+    p->pCnf = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) ); 
     p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
     // assign parameters
     p->nFramesK = nFramesK;
@@ -221,9 +221,9 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
 {
     Aig_Obj_t * pObj, * pObj2;
     int i, f, VarA, VarB, RetValue, Entry, status;
-    int nRegs = Aig_ManPiNum(pCnfInt->pMan);
-    assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
-    assert( Aig_ManPoNum(pCnfInt->pMan) == 1 );
+    int nRegs = Aig_ManCiNum(pCnfInt->pMan);
+    assert( Aig_ManCoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
+    assert( Aig_ManCoNum(pCnfInt->pMan) == 1 );
 
     // set runtime limit
     if ( nTimeNewOut )
@@ -242,7 +242,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
         // add equality clauses for the flop variables
         Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
         {
-            pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
+            pObj2 = f ? Aig_ManCo(p->pFrames, i + (f-1) * nRegs) : Aig_ManCi(p->pFrames, i);
             Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
         }
         // add final clauses
@@ -251,14 +251,14 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
             if ( f == Vec_IntSize(p->vOrLits) ) // find time here
             {
                 // add literal to this frame
-                VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+                VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
                 Vec_IntPush( p->vOrLits, VarB );
             }
             else
             {
                 // add OR gate for this frame
                 VarA = Vec_IntEntry( p->vOrLits, f );
-                VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+                VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
                 Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
                 Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
             }
@@ -266,7 +266,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut
         else
         {
             // add AND gate for this frame
-            VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
+            VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
             Vec_IntPush( p->vAndLits, VarB );
         }
         // update variable IDs
diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c
index 213c557c..a031c7a4 100644
--- a/src/proof/int/intContain.c
+++ b/src/proof/int/intContain.c
@@ -161,7 +161,7 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
 {
     Aig_Obj_t * pObj;
     int i;
-    assert( Aig_ManPoNum(pOld) == 1 );
+    assert( Aig_ManCoNum(pOld) == 1 );
     // create the PIs
     Aig_ManCleanData( pOld );
     Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
@@ -171,7 +171,7 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew
     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 );
+    pObj = Aig_ManCo( pOld, 0 );
     Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
 }
 
@@ -283,7 +283,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
         return 1;
 //    assert( Saig_ManPoNum(p) == 1 );
     assert( Aig_ManRegNum(p) > 0 );
-    assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) );
+    assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
 
     // get the counter-example
     vPis = Vec_IntAlloc( 100 );
@@ -303,12 +303,12 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
     for ( i = 0; i < nFrames; i++ )
         Aig_ManForEachPiSeq( p, pObj, k )
             Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i );
-    assert( iBit == Aig_ManPiNum(pCnf->pMan) );
+    assert( iBit == Aig_ManCiNum(pCnf->pMan) );
     // run simulation
     Fra_SmlSimulateOne( pSml );
 
     // check if the given output has failed
-//    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, 0) );
+//    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManCo(pAig, 0) );
 //    assert( RetValue );
 
     // check values at the internal nodes
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index 10a8fc74..8bef9c59 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -139,7 +139,7 @@ clk2 = clock();
             p->pInter = Inter_ManStartOneOutput( pAig, 1 );
         else
             p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
-        assert( Aig_ManPoNum(p->pInter) == 1 );
+        assert( Aig_ManCoNum(p->pInter) == 1 );
 clk = clock();
         p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
 p->timeCnf += clock() - clk;    
@@ -157,7 +157,7 @@ p->timeRwr += clock() - clk;
         // can also do SAT sweeping on the timeframes...
 clk = clock();
         if ( pPars->fUseBackward )
-            p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );  
+            p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );  
         else
 //            p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );  
             p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 );  
@@ -285,7 +285,7 @@ clk = clock();
 p->timeRwr += clock() - clk;
 
             // check if interpolant is trivial
-            if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManPo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
+            if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManCo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
             { 
 //                printf( "interpolant is constant 0\n" );
                 if ( pPars->fVerbose )
@@ -300,7 +300,7 @@ p->timeRwr += clock() - clk;
 clk = clock();
             if ( pPars->fCheckKstep ) // k-step unique-state induction
             {
-                if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+                if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
                 {
                     if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 )
                     {
@@ -326,7 +326,7 @@ timeTemp = clock() - clk2;
             }
             else // combinational containment
             {
-                if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+                if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
                     Status = Inter_ManCheckContainment( p->pInterNew, p->pInter );
                 else
                     Status = 0;
diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c
index 22e689f4..04aaa271 100644
--- a/src/proof/int/intCtrex.c
+++ b/src/proof/int/intCtrex.c
@@ -75,7 +75,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
             pObjLo->pData = pObjLi->pData;
     }
     // create POs for the output of the last frame
-    pObj = Aig_ManPo( pAig, 0 );
+    pObj = Aig_ManCo( pAig, 0 );
     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 adc692cb..d7bc73d6 100644
--- a/src/proof/int/intDup.c
+++ b/src/proof/int/intDup.c
@@ -141,7 +141,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     }
     // set registers
     pNew->nRegs    = fAddFirstPo? 0 : p->nRegs;
-    pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1;
+    pNew->nTruePis = fAddFirstPo? Aig_ManCiNum(p) + 1 : p->nTruePis + 1;
     pNew->nTruePos = fAddFirstPo + Saig_ManConstrNum(p);
     // duplicate internal nodes
     Aig_ManForEachNode( p, pObj, i )
@@ -158,7 +158,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     // add the PO
     if ( fAddFirstPo )
     {
-        pObj = Aig_ManPo( p, 0 );
+        pObj = Aig_ManCo( p, 0 );
         Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
     }
     else
diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c
index 8e74d99a..7c5231b7 100644
--- a/src/proof/int/intFrames.c
+++ b/src/proof/int/intFrames.c
@@ -99,7 +99,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
     // create the only PO of the manager
     else
     {
-        pObj = Aig_ManPo( pAig, 0 );
+        pObj = Aig_ManCo( pAig, 0 );
         Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
     }
     Aig_ManCleanup( pFrames );
diff --git a/src/proof/int/intInter.c b/src/proof/int/intInter.c
index ef32294b..ffc462d3 100644
--- a/src/proof/int/intInter.c
+++ b/src/proof/int/intInter.c
@@ -45,10 +45,10 @@ ABC_NAMESPACE_IMPL_START
 Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
 {
     Aig_Man_t * pInterC;
-    assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) );
+    assert( Aig_ManCiNum(pInter) <= Aig_ManCiNum(pOther) );
     pInterC = Aig_ManDupSimple( pInter );
-    Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 );
-    assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) );
+    Aig_IthVar( pInterC, Aig_ManCiNum(pOther)-1 );
+    assert( Aig_ManCiNum(pInterC) == Aig_ManCiNum(pOther) );
     return pInterC;
 }
 
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c
index c37cb2c6..ed3ef80e 100644
--- a/src/proof/int/intM114.c
+++ b/src/proof/int/intM114.c
@@ -61,10 +61,10 @@ sat_solver * Inter_ManDeriveSatSolver(
     assert( Aig_ManRegNum(pInter) == 0 );
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManRegNum(pFrames) == 0 );
-    assert( Aig_ManPoNum(pInter) == 1 );
-    assert( Aig_ManPoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
-    assert( fUseBackward || Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
-//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+    assert( Aig_ManCoNum(pInter) == 1 );
+    assert( Aig_ManCoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
+    assert( fUseBackward || Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
+//    assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
 
     // prepare CNFs
     Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
@@ -93,12 +93,12 @@ sat_solver * Inter_ManDeriveSatSolver(
     {
         Saig_ManForEachLi( pAig, pObj2, i )
         {
-            if ( Saig_ManRegNum(pAig) == Aig_ManPiNum(pInter) )
-                pObj = Aig_ManPi( pInter, i );
+            if ( Saig_ManRegNum(pAig) == Aig_ManCiNum(pInter) )
+                pObj = Aig_ManCi( pInter, i );
             else
             {
-                assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pInter) );
-                pObj = Aig_ManPi( pInter, Aig_ManPiNum(pAig)-Saig_ManRegNum(pAig) + i );
+                assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pInter) );
+                pObj = Aig_ManCi( pInter, Aig_ManCiNum(pAig)-Saig_ManRegNum(pAig) + i );
             }
 
             Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c
index 6164a389..f143dc39 100644
--- a/src/proof/int/intM114p.c
+++ b/src/proof/int/intM114p.c
@@ -59,10 +59,10 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p(
     assert( Aig_ManRegNum(pInter) == 0 );
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManRegNum(pFrames) == 0 );
-    assert( Aig_ManPoNum(pInter) == 1 );
-    assert( Aig_ManPoNum(pFrames) == 1 );
-    assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
-//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+    assert( Aig_ManCoNum(pInter) == 1 );
+    assert( Aig_ManCoNum(pFrames) == 1 );
+    assert( Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) );
+//    assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
 
     // prepare CNFs
     Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );