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

17 files changed, 157 insertions, 157 deletions

diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c
index b0dd3c86..2ddecf48 100644
--- a/src/proof/fra/fraBmc.c
+++ b/src/proof/fra/fraBmc.c
@@ -395,10 +395,10 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
     if ( fVerbose )
     {
         printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
-            Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig),
+            Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig),
             Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
         printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
-            nFrames, Aig_ManPiNum(pBmc->pAigFrames), Aig_ManPoNum(pBmc->pAigFrames), 
+            nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames), 
             Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) );
         ABC_PRT( "Time", clock() - clk );
     }
@@ -417,7 +417,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
     clk = clock();
     iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
     if ( iOutput >= 0 )
-        pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
+        pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
     else
     {
         pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
@@ -428,7 +428,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew
             ABC_FREE( pBmc->pAigFraig->pData );
         }
         else if ( iOutput >= 0 )
-            pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
+            pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput );
     }
     if ( fVerbose )
     {
diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c
index ac11b0bb..0acca245 100644
--- a/src/proof/fra/fraCec.c
+++ b/src/proof/fra/fraCec.c
@@ -60,8 +60,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
         pMan->pData = NULL;
 
         // derive CNF
-        pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
-    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+        pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
+    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
 
         if ( fFlipBits ) 
             Cnf_DataTranformPolarity( pCnf, 0 );
@@ -166,8 +166,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
         pMan->pData = NULL;
 
         // derive CNF
-        pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
-    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
+        pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
+    //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
 
         if ( fFlipBits ) 
             Cnf_DataTranformPolarity( pCnf, 0 );
@@ -293,8 +293,8 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 //    assert( RetValue == -1 );
     if ( RetValue == 0 )
     {
-        pAig->pData = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
-        memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) );
+        pAig->pData = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
+        memset( pAig->pData, 0, sizeof(int) * Aig_ManCiNum(pAig) );
         return RetValue;
     }
 
@@ -406,7 +406,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi
         if ( fVerbose )
         {
             printf( "Verifying part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
-                i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), 
+                i+1, Vec_PtrSize(vParts), Aig_ManCiNum(pAig), Aig_ManCoNum(pAig), 
                 Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
             fflush( stdout );
         }
@@ -459,18 +459,18 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
     //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
     int RetValue, clkTotal = clock();
 
-    if ( Aig_ManPiNum(pMan1) != Aig_ManPiNum(pMan1) )
+    if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) )
     {
         printf( "Abc_CommandAbc8Cec(): Miters have different number of PIs.\n" );
         return 0;
     }
-    if ( Aig_ManPoNum(pMan1) != Aig_ManPoNum(pMan1) )
+    if ( Aig_ManCoNum(pMan1) != Aig_ManCoNum(pMan1) )
     {
         printf( "Abc_CommandAbc8Cec(): Miters have different number of POs.\n" );
         return 0;
     }
-    assert( Aig_ManPiNum(pMan1) == Aig_ManPiNum(pMan1) );
-    assert( Aig_ManPoNum(pMan1) == Aig_ManPoNum(pMan1) );
+    assert( Aig_ManCiNum(pMan1) == Aig_ManCiNum(pMan1) );
+    assert( Aig_ManCoNum(pMan1) == Aig_ManCoNum(pMan1) );
 
     // make sure that the first miter has more nodes
     if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) )
@@ -484,7 +484,7 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
     if ( nPartSize )
         RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose );
     else // no partitioning
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManPoNum(pMan1), 0, fVerbose );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManCoNum(pMan1), 0, fVerbose );
 
     // report the miter
     if ( RetValue == 1 )
diff --git a/src/proof/fra/fraClass.c b/src/proof/fra/fraClass.c
index f7850241..cef2f673 100644
--- a/src/proof/fra/fraClass.c
+++ b/src/proof/fra/fraClass.c
@@ -291,12 +291,12 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
     {
         if ( fLatchCorr )
         {
-            if ( !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsCi(pObj) )
                 continue;
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                 continue;
             // skip the node with more that the given number of levels
             if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
@@ -349,7 +349,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
     nEntries = 0;
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         // skip the nodes that are not representatives of non-trivial classes
         if ( pObj->fMarkA == 0 )
@@ -800,7 +800,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
     Aig_Obj_t ** pLatches, ** ppEquivs;
     int i, k, f, nFramesAll = nFramesK + 1;
     assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
     assert( nFramesK > 0 );
     // start the fraig package
     pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
@@ -832,7 +832,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
         if ( f == nFramesAll - 1 )
             break;
         if ( f == nFramesAll - 2 )
-            pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+            pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
         // save the latch input values
         k = 0;
         Aig_ManForEachLiSeq( p->pAig, pObj, i )
@@ -845,9 +845,9 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
     ABC_FREE( pLatches );
     ABC_FREE( ppEquivs );
     // mark the asserts
-    assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
+    assert( Aig_ManCoNum(pManFraig) % nFramesAll == 0 );
 printf( "Assert miters = %6d. Output miters = %6d.\n", 
-       pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
+       pManFraig->nAsserts, Aig_ManCoNum(pManFraig) - pManFraig->nAsserts );
     // remove dangling nodes
     Aig_ManCleanup( pManFraig );
     return pManFraig;
diff --git a/src/proof/fra/fraClau.c b/src/proof/fra/fraClau.c
index 28e9e9b9..6c692afa 100644
--- a/src/proof/fra/fraClau.c
+++ b/src/proof/fra/fraClau.c
@@ -108,7 +108,7 @@ Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf )
     Vec_Int_t * vVars;
     Aig_Obj_t * pObj;
     int i;
-    vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) );
+    vVars = Vec_IntAlloc( Aig_ManCoNum(pMan) );
     Aig_ManForEachCo( pMan, pObj, i )
         Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
     return vVars;
@@ -130,7 +130,7 @@ Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStar
     Vec_Int_t * vVars;
     Aig_Obj_t * pObj;
     int i;
-    vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting );
+    vVars = Vec_IntAlloc( Aig_ManCiNum(pMan) - nStarting );
     Aig_ManForEachCi( pMan, pObj, i )
     {
         if ( i < nStarting )
@@ -217,7 +217,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     Aig_Man_t * pFramesMain;
     Aig_Man_t * pFramesTest;
     Aig_Man_t * pFramesBmc;
-    assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
+    assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
 
     // start the manager
     p = ABC_ALLOC( Cla_Man_t, 1 );
@@ -232,8 +232,8 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     // derive two timeframes to be checked
     pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs
 //Aig_ManShow( pFramesMain, 0, NULL );
-    assert( Aig_ManPoNum(pFramesMain) == 2 );
-    Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
+    assert( Aig_ManCoNum(pFramesMain) == 2 );
+    Aig_ObjChild0Flip( Aig_ManCo(pFramesMain, 0) ); // complement the first output
     pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
 //Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
     p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
@@ -249,7 +249,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
 
     // derive one timeframe to be checked
     pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL );
-    assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
+    assert( Aig_ManCoNum(pFramesTest) == Aig_ManRegNum(pMan) );
     pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
     p->pSatTest = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
     p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
@@ -257,12 +257,12 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     // derive one timeframe to be checked for BMC
     pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL );
 //Aig_ManShow( pFramesBmc, 0, NULL );
-    assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
+    assert( Aig_ManCoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
     pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
     p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
 
     // create variable sets
-    p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) );
+    p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManCiNum(pMan)-Aig_ManRegNum(pMan)) );
     p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 );
     p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 );
     p->vSatVarsBmcNs  = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc );
@@ -638,7 +638,7 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose )
 {
     Cla_Man_t * p;
     int Iter, RetValue, fFailed, i;
-    assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
+    assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
     // create the manager
     p = Fra_ClauStart( pMan );
     if ( p == NULL )
diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c
index f27c63ce..571cc510 100644
--- a/src/proof/fra/fraClaus.c
+++ b/src/proof/fra/fraClaus.c
@@ -97,7 +97,7 @@ int Fra_ClausRunBmc( Clu_Man_t * p )
     int Lits[2], nLitsTot, RetValue, i;
     // set the output literals
     nLitsTot = 2 * p->pCnf->nVars;
-    pObj = Aig_ManPo(p->pAig, 0);
+    pObj = Aig_ManCo(p->pAig, 0);
     for ( i = 0; i < p->nPref + p->nFrames; i++ )
     {
         Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
@@ -126,7 +126,7 @@ int Fra_ClausRunSat( Clu_Man_t * p )
     int i, RetValue;
     pLits = ABC_ALLOC( int, p->nFrames + 1 );
     // set the output literals
-    pObj = Aig_ManPo(p->pAig, 0);
+    pObj = Aig_ManCo(p->pAig, 0);
     for ( i = 0; i <= p->nFrames; i++ )
         pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames ); 
     // try to solve the problem
@@ -154,7 +154,7 @@ int Fra_ClausRunSat0( Clu_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int Lits[2], RetValue;
-    pObj = Aig_ManPo(p->pAig, 0);
+    pObj = Aig_ManCo(p->pAig, 0);
     Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
     RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
@@ -523,7 +523,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
     {
         Aig_Obj_t * pObj;
         int Lits[1];
-        pObj = Aig_ManPo( p->pAig, 0 );
+        pObj = Aig_ManCo( p->pAig, 0 );
         Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); 
         Vec_IntPush( p->vLits, Lits[0] );
         Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
@@ -1242,7 +1242,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
         Aig_Obj_t * pObj;
         int Lits[2];
         // set the output literals
-        pObj = Aig_ManPo(p->pAig, 0);
+        pObj = Aig_ManCo(p->pAig, 0);
         Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); 
         // add the clause
         RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
@@ -1637,9 +1637,9 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
             pVar2Id[ p->pCnf->pVarNums[i] ] = i;
         }
     // get storage for one assignment and all assignments
-    assert( Aig_ManPoNum(p->pAig) > 2 );
-    pResultOne = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 0)->Id );
-    pResultTot = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 1)->Id );
+    assert( Aig_ManCoNum(p->pAig) > 2 );
+    pResultOne = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 0)->Id );
+    pResultTot = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 1)->Id );
     // start the OR of don't-cares
     for ( w = 0; w < nCombSimWords; w++ )
         pResultTot[w] = 0;
@@ -1693,13 +1693,13 @@ if ( p->fVerbose )
 //ABC_PRT( "Sim-seq", clock() - clk );
 }
 
-    assert( !p->fTarget || Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
+    assert( !p->fTarget || Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
 
 clk = clock();
     // derive CNF
 //    if ( p->fTarget )
 //        p->pAig->nRegs++;
-    p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
+    p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManCoNum(p->pAig) );
 //    if ( p->fTarget )
 //        p->pAig->nRegs--;
 if ( fVerbose )
@@ -1846,8 +1846,8 @@ clk = clock();
         assert( p->nBatches == 1 );
         pTable = fopen( "stats.txt", "a+" );
         fprintf( pTable, "%s ",  pAig->pName );
-        fprintf( pTable, "%d ",  Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig) );
-        fprintf( pTable, "%d ",  Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig) );
+        fprintf( pTable, "%d ",  Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig) );
+        fprintf( pTable, "%d ",  Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig) );
         fprintf( pTable, "%d ",  Aig_ManRegNum(pAig) );
         fprintf( pTable, "%d ",  Aig_ManNodeNum(pAig) );
         fprintf( pTable, "%d ",  p->nCuts );
diff --git a/src/proof/fra/fraCnf.c b/src/proof/fra/fraCnf.c
index 5021e750..7024c0f4 100644
--- a/src/proof/fra/fraCnf.c
+++ b/src/proof/fra/fraCnf.c
@@ -167,7 +167,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
 void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
 {
     // if the new node is complemented or a PI, another gate begins
-    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
          (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
     {
         Vec_PtrPushUnique( vSuper, pObj );
@@ -193,7 +193,7 @@ Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes )
 {
     Vec_Ptr_t * vSuper;
     assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsPi(pObj) );
+    assert( !Aig_ObjIsCi(pObj) );
     vSuper = Vec_PtrAlloc( 4 );
     Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
     return vSuper;
diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c
index 1969b36d..2148b467 100644
--- a/src/proof/fra/fraCore.c
+++ b/src/proof/fra/fraCore.c
@@ -81,7 +81,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
             continue;
         }
         // check if the output is a primary input
-        if ( Aig_ObjIsPi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis )
+        if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis )
         {
             CountNonConst0++;
             continue;
@@ -97,7 +97,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
 /*
     if ( p->pParams->fVerbose )
     {
-        printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) );
+        printf( "Miter has %d outputs. ", Aig_ManCoNum(p->pManAig) );
         printf( "Const0 = %d.  ", CountConst0 );
         printf( "NonConst0 = %d.  ", CountNonConst0 );
         printf( "Undecided = %d.  ", CountUndecided );
@@ -187,7 +187,7 @@ void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
 {
     Aig_Obj_t * pObj, ** ppClass;
     int i, c;
-    assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
+    assert( Aig_ManCiNum(p->pManAig) == Vec_IntSize(vCex) );
     // make sure the input pattern is not used
     Aig_ManForEachObj( p->pManAig, pObj, i )
         assert( !pObj->fMarkB );
diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c
index 03dd468a..338b5717 100644
--- a/src/proof/fra/fraHot.c
+++ b/src/proof/fra/fraHot.c
@@ -137,7 +137,7 @@ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
     Vec_Int_t * vOneHots;
     Aig_Obj_t * pObj1, * pObj2;
     int i, k;
-    int nTruePis = Aig_ManPiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
+    int nTruePis = Aig_ManCiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig);
     assert( pSim->pAig == p->pManAig );
     vOneHots = Vec_IntAlloc( 100 );
     Aig_ManForEachLoSeq( pSim->pAig, pObj1, i )
@@ -146,8 +146,8 @@ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim )
             continue;
         assert( i-nTruePis >= 0 );
 //        Aig_ManForEachLoSeq( pSim->pAig, pObj2, k )
-//        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
-        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, i+1 )
+//        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManCiNum(p)-Aig_ManRegNum(p) )
+        Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vCis, pObj2, k, i+1 )
         {
             if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) )
                 continue;
@@ -192,7 +192,7 @@ void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots )
 {
     Aig_Obj_t * pObj1, * pObj2;
     int i, Out1, Out2, pLits[2];
-    int nPiNum = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
+    int nPiNum = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
     assert( p->pPars->nFramesK == 1 ); // add to only one frame
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
@@ -200,8 +200,8 @@ void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots )
         Out2 = Vec_IntEntry( vOneHots, i+1 );
         if ( Out1 == 0 && Out2 == 0 )
             continue;
-        pObj1 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
+        pObj1 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out2) );
         pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) );
         pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) );
         // add constraint to solver
@@ -230,15 +230,15 @@ void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots )
 {
     Aig_Obj_t * pObj1, * pObj2;
     int RetValue, i, Out1, Out2;
-    int nTruePos = Aig_ManPoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
+    int nTruePos = Aig_ManCoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig);
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
         Out1 = Vec_IntEntry( vOneHots, i );
         Out2 = Vec_IntEntry( vOneHots, i+1 );
         if ( Out1 == 0 && Out2 == 0 )
             continue;
-        pObj1 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
+        pObj1 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out2) );
         RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) );
         if ( RetValue != 1 )
         {
@@ -267,7 +267,7 @@ int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots )
 {
     Aig_Obj_t * pObj1, * pObj2;
     int i, Out1, Out2, RetValue = 0;
-    int nPiNum = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    int nPiNum = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     assert( p->pSml->pAig == p->pManAig );
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
@@ -276,8 +276,8 @@ int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots )
         if ( Out1 == 0 && Out2 == 0 )
             continue;
         // get the corresponding nodes
-        pObj1 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
+        pObj1 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out2) );
         // check if implication holds using this simulation info
         if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) )
         {
@@ -405,22 +405,22 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
 //        Aig_ObjCreateCi(pNew);
     Aig_ManForEachCi( p->pManAig, pObj, i )
         Aig_ObjCreateCi(pNew);
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
     {
         Out1 = Vec_IntEntry( vOneHots, i );
         Out2 = Vec_IntEntry( vOneHots, i+1 );
         if ( Out1 == 0 && Out2 == 0 )
             continue;
-        pObj1 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out1) );
-        pObj2 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out2) );
+        pObj1 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out1) );
+        pObj2 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out2) );
         pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
         pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
         pObj  = Aig_Or( pNew, pObj1, pObj2 );
         Aig_ObjCreateCo( pNew, pObj );
     }
     Aig_ManCleanup(pNew);
-//    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
+//    printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManCoNum(pNew) );
     return pNew;
 }
 
@@ -450,8 +450,8 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots )
         Vec_IntForEachEntry( vGroup, Out1, i )
         Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 )
         {
-            pObj1 = Aig_ManPi( p->pManFraig, Out1 );
-            pObj2 = Aig_ManPi( p->pManFraig, Out2 );
+            pObj1 = Aig_ManCi( p->pManFraig, Out1 );
+            pObj2 = Aig_ManCi( p->pManFraig, Out2 );
             pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 );
             pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 );
             // add constraint to solver
diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c
index de24f179..f65aca5c 100644
--- a/src/proof/fra/fraImp.c
+++ b/src/proof/fra/fraImp.c
@@ -170,12 +170,12 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
         // skip non-PI and non-internal nodes
         if ( fLatchCorr )
         {
-            if ( !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsCi(pObj) )
                 continue;
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                 continue;
         }
         // skip nodes participating in the classes
@@ -203,12 +203,12 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
         // skip non-PI and non-internal nodes
         if ( fLatchCorr )
         {
-            if ( !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsCi(pObj) )
                 continue;
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
                 continue;
         }
         // skip nodes participating in the classes
@@ -708,7 +708,7 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
         return;
     // go through the implication
-    nPosOld = Aig_ManPoNum(pNew);
+    nPosOld = Aig_ManCoNum(pNew);
     Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
     {
         pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
@@ -719,7 +719,7 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
             Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); 
         Aig_ObjCreateCo( pNew, pMiter );
     }
-    pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
+    pNew->nAsserts = Aig_ManCoNum(pNew) - nPosOld;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c
index b8a1e6bf..29a76eea 100644
--- a/src/proof/fra/fraInd.c
+++ b/src/proof/fra/fraInd.c
@@ -61,16 +61,16 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p )
     // transfer PI/register pointers
     assert( p->pManFraig->nRegs == pTemp->nRegs );
     assert( p->pManFraig->nAsserts == pTemp->nAsserts );
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
     Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
     Aig_ManForEachPiSeq( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManPi(pTemp,nTruePis*p->pPars->nFramesK+i) );
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManCi(pTemp,nTruePis*p->pPars->nFramesK+i) );
     k = 0;
-    assert( Aig_ManRegNum(p->pManAig) == Aig_ManPoNum(pTemp) - pTemp->nAsserts );
+    assert( Aig_ManRegNum(p->pManAig) == Aig_ManCoNum(pTemp) - pTemp->nAsserts );
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
     {
-        pObjPo = Aig_ManPo(pTemp, pTemp->nAsserts + k++);
+        pObjPo = Aig_ManCo(pTemp, pTemp->nAsserts + k++);
         Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
     }
     // exchange
@@ -133,7 +133,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
     int i, k, f;
     assert( p->pManFraig == NULL );
     assert( Aig_ManRegNum(p->pManAig) > 0 );
-    assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
+    assert( Aig_ManRegNum(p->pManAig) < Aig_ManCiNum(p->pManAig) );
 
     // start the fraig package
     pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
@@ -170,7 +170,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
     }
 //    pManFraig->fAddStrash = 0;
     // mark the asserts
-    pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+    pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
     // add the POs for the latch outputs of the last frame
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
         Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
@@ -291,7 +291,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
             pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
             Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
             printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
-                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+                i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
             Aig_ManStop( pTemp );
         }
     }
@@ -309,7 +309,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
         nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
         if ( fVerbose )
             printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", 
-                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+                i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
         Aig_ManStop( pNew );
         Aig_ManStop( pTemp );
         ABC_FREE( pMapBack );
@@ -637,8 +637,8 @@ p->timeTotal = clock() - clk;
 finish:
     Fra_ManStop( p );
     // check the output
-//    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
-//        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
+//    if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
+//        if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
 //            printf( "Proved output constant 0.\n" );
     pParams->nIters = nIter;
     return pManAigNew;
diff --git a/src/proof/fra/fraIndVer.c b/src/proof/fra/fraIndVer.c
index 64437607..7c5e9e70 100644
--- a/src/proof/fra/fraIndVer.c
+++ b/src/proof/fra/fraIndVer.c
@@ -59,14 +59,14 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
     }
 
     // derive CNF
-    pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) );
+    pCnf = Cnf_DeriveSimple( pAig, Aig_ManCoNum(pAig) );
 /*
     // add the property
     {
         Aig_Obj_t * pObj;
         int Lits[1];
 
-        pObj = Aig_ManPo( pAig, 0 );
+        pObj = Aig_ManCo( pAig, 0 );
         Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); 
 
         Vec_IntPush( vLits, Lits[0] );
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index d24b37f6..8ea6d297 100644
--- a/src/proof/fra/fraLcr.c
+++ b/src/proof/fra/fraLcr.c
@@ -83,10 +83,10 @@ Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
     p = ABC_ALLOC( Fra_Lcr_t, 1 );
     memset( p, 0, sizeof(Fra_Lcr_t) );
     p->pAig = pAig;
-    p->pInToOutPart = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
-    memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
-    p->pInToOutNum = ABC_ALLOC( int, Aig_ManPiNum(pAig) );
-    memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
+    p->pInToOutPart = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
+    memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManCiNum(pAig) );
+    p->pInToOutNum = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
+    memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManCiNum(pAig) );
     p->vFraigs = Vec_PtrAlloc( 1000 );
     return p;
 }
@@ -205,8 +205,8 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
     Aig_Man_t * pFraig;
     Aig_Obj_t * pOut0, * pOut1;
     int nPart0, nPart1;
-    assert( Aig_ObjIsPi(pObj0) );
-    assert( Aig_ObjIsPi(pObj1) );
+    assert( Aig_ObjIsCi(pObj0) );
+    assert( Aig_ObjIsCi(pObj1) );
     // find the partition to which these nodes belong
     nPart0 = pLcr->pInToOutPart[(long)pObj0->pNext];
     nPart1 = pLcr->pInToOutPart[(long)pObj1->pNext];
@@ -220,8 +220,8 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
     assert( nPart0 == nPart1 );
     pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart0 );
     // get the fraig outputs
-    pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] );
-    pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] );
+    pOut0 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] );
+    pOut1 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] );
     return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
 }
 
@@ -243,12 +243,12 @@ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
     Aig_Man_t * pFraig;
     Aig_Obj_t * pOut;
     int nPart;
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     // find the partition to which these nodes belong
     nPart = pLcr->pInToOutPart[(long)pObj->pNext];
     pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart );
     // get the fraig outputs
-    pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] );
+    pOut = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] );
     return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
 }
 
@@ -306,7 +306,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
         pObj->pNext = (Aig_Obj_t *)(long)i;
     }
     // compute the LO/LI offset
-    Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig);
+    Offset = Aig_ManCoNum(pLcr->pAig) - Aig_ManCiNum(pLcr->pAig);
     // create the PIs
     Aig_ManCleanData( pLcr->pAig );
     pNew = Aig_ManStartFrom( pLcr->pAig );
@@ -316,8 +316,8 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
         pMiter = Aig_ManConst0(pNew);
         for ( c = 0; ppClass[c]; c++ )
         {
-            assert( Aig_ObjIsPi(ppClass[c]) );
-            pObjPo  = Aig_ManPo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
+            assert( Aig_ObjIsCi(ppClass[c]) );
+            pObjPo  = Aig_ManCo( pLcr->pAig, Offset+(long)ppClass[c]->pNext );
             pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
             pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
         }
@@ -326,8 +326,8 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
     // go over the constant candidates
     Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i )
     {
-        assert( Aig_ObjIsPi(pObj) );
-        pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext );
+        assert( Aig_ObjIsCi(pObj) );
+        pObjPo = Aig_ManCo( pLcr->pAig, Offset+(long)pObj->pNext );
         pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
         Aig_ObjCreateCo( pNew, pMiter );
     }
@@ -351,7 +351,7 @@ void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOu
     Aig_Obj_t ** ppClass, * pObjPi;
     int Out, Offset, i, k, c;
     // compute the LO/LI offset
-    Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig);
+    Offset = Aig_ManCoNum(pCla->pAig) - Aig_ManCiNum(pCla->pAig);
     Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i )
     {
         vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
@@ -398,7 +398,7 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return (Aig_Obj_t *)pObj->pData;
     Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
 //        Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
         Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
@@ -439,7 +439,7 @@ Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart )
     Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
     Vec_IntForEachEntry( vPart, Out, i )
     {
-        pObj = Aig_ManPo( p->pAig, Out );
+        pObj = Aig_ManCo( p->pAig, Out );
         if ( pObj->fMarkA )
         {
             pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
@@ -468,18 +468,18 @@ void Fra_ClassNodesMark( Fra_Lcr_t * p )
     Aig_Obj_t * pObj, ** ppClass;
     int i, c, Offset;
     // compute the LO/LI offset
-    Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
+    Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig);
     // mark the nodes remaining in the classes
     Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
     {
-        pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext );
+        pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext );
         pObj->fMarkA = 1;
     }
     Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
     {
         for ( c = 0; ppClass[c]; c++ )
         {
-            pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
+            pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
             pObj->fMarkA = 1;
         }
     }
@@ -501,18 +501,18 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
     Aig_Obj_t * pObj, ** ppClass;
     int i, c, Offset;
     // compute the LO/LI offset
-    Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
+    Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig);
     // mark the nodes remaining in the classes
     Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i )
     {
-        pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext );
+        pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext );
         pObj->fMarkA = 0;
     }
     Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i )
     {
         for ( c = 0; ppClass[c]; c++ )
         {
-            pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
+            pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext );
             pObj->fMarkA = 0;
         }
     }
diff --git a/src/proof/fra/fraMan.c b/src/proof/fra/fraMan.c
index 67832f83..5ffbc778 100644
--- a/src/proof/fra/fraMan.c
+++ b/src/proof/fra/fraMan.c
@@ -114,7 +114,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
     p->nFramesAll = pPars->nFramesK + 1;
     // allocate storage for sim pattern
-    p->nPatWords  = Abc_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
+    p->nPatWords  = Abc_BitWordNum( (Aig_ManCiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
     p->pPatWords  = ABC_ALLOC( unsigned, p->nPatWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
     // equivalence classes
diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c
index 6594ac0b..e3bb2850 100644
--- a/src/proof/fra/fraPart.c
+++ b/src/proof/fra/fraPart.c
@@ -74,7 +74,7 @@ ABC_PRT( "Supports", clock() - clk );
 
     // create reverse supports
 clk = clock();
-    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+    vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
     Aig_ManForEachCo( p, pObj, i )
     {
         vSup = Vec_VecEntryInt( vSupps, i );
@@ -86,10 +86,10 @@ ABC_PRT( "Inverse ", clock() - clk );
 clk = clock();
     // compute extended supports
     Largest = 0;
-    vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
-    vOverNew  = Vec_IntAlloc( Aig_ManPoNum(p) );
-    vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
-//    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
+    vSuppsNew = Vec_PtrAlloc( Aig_ManCoNum(p) );
+    vOverNew  = Vec_IntAlloc( Aig_ManCoNum(p) );
+    vQuantNew = Vec_IntAlloc( Aig_ManCoNum(p) );
+//    pProgress = Bar_ProgressStart( stdout, Aig_ManCoNum(p) );
     Aig_ManForEachCo( p, pObj, i )
     {
 //        Bar_ProgressUpdate( pProgress, i, NULL );
@@ -160,9 +160,9 @@ ABC_PRT( "Scanning", clock() - clk );
 
     // print cumulative statistics
     printf( "PIs = %6d. POs = %6d. Lim = %3d.   AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
-        Aig_ManPiNum(p), Aig_ManPoNum(p), nComLim,
-        nTotalSupp/Aig_ManPoNum(p), nTotalSupp2/Aig_ManPoNum(p),
-        Ratio/Aig_ManPoNum(p), Largest );
+        Aig_ManCiNum(p), Aig_ManCoNum(p), nComLim,
+        nTotalSupp/Aig_ManCoNum(p), nTotalSupp2/Aig_ManCoNum(p),
+        Ratio/Aig_ManCoNum(p), Largest );
 
     Vec_VecFree( vSupps );
     Vec_VecFree( vSuppsIn );
@@ -208,7 +208,7 @@ ABC_PRT( "Supports", clock() - clk );
 
     // create reverse supports
 clk = clock();
-    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+    vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) );
     Aig_ManForEachCo( p, pObj, i )
     {
         if ( i == p->nAsserts )
@@ -221,13 +221,13 @@ ABC_PRT( "Inverse ", clock() - clk );
 
     // create affective supports
 clk = clock();
-    pSupp = ABC_ALLOC( char, Aig_ManPiNum(p) );
+    pSupp = ABC_ALLOC( char, Aig_ManCiNum(p) );
     Aig_ManForEachCo( p, pObj, i )
     {
         if ( i % 50 != 0 )
             continue;
         vSup = Vec_VecEntryInt( vSupps, i );
-        memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) );
+        memset( pSupp, 0, sizeof(char) * Aig_ManCiNum(p) );
         // go through each input of this output
         Vec_IntForEachEntry( vSup, Entry, k )
         {
@@ -246,7 +246,7 @@ clk = clock();
         }
         // count the entries
         Counter = 0;
-        for ( m = 0; m < Aig_ManPiNum(p); m++ )
+        for ( m = 0; m < Aig_ManCiNum(p); m++ )
             Counter += pSupp[m];
         printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
     }
diff --git a/src/proof/fra/fraSat.c b/src/proof/fra/fraSat.c
index 38702d5e..2702113c 100644
--- a/src/proof/fra/fraSat.c
+++ b/src/proof/fra/fraSat.c
@@ -507,7 +507,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i
         return 0;
     Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
     // add the PI to the list
-    if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) )
+    if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsCi(pObj) )
         return 0;
     // set the factor of this variable
     // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c
index 8067b8c2..cde56809 100644
--- a/src/proof/fra/fraSec.c
+++ b/src/proof/fra/fraSec.c
@@ -142,8 +142,8 @@ clk = clock();
     if ( pParSec->fPhaseAbstract )
     {
         extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
-        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
         pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
         Aig_ManStop( pTemp );
         if ( pParSec->fVerbose )
@@ -301,8 +301,8 @@ ABC_PRT( "Time", clock() - clk );
     {
 //    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
-    pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-    pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+    pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
+    pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
 //        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
     pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
     Aig_ManStop( pTemp );
@@ -391,8 +391,8 @@ ABC_PRT( "Time", clock() - clk );
         {
 //        extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
-        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
 //        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
         pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
         Aig_ManStop( pTemp );
@@ -580,8 +580,8 @@ ABC_PRT( "Time", clock() - clk );
         pPars->fReorderImage = 1;
         pPars->fVerbose      = 0;
         pPars->fSilent       = pParSec->fSilent;
-        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
-        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); 
         RetValue = Aig_ManVerifyUsingBdds( pNew, pPars );
     }
 
diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c
index e54846bc..66579be3 100644
--- a/src/proof/fra/fraSim.c
+++ b/src/proof/fra/fraSim.c
@@ -221,7 +221,7 @@ void Fra_SmlSavePattern1( Fra_Man_t * p, int fInit )
     if ( !fInit )
         return;
     // clear the state bits to correspond to all-0 initial state
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     k = 0;
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
         Abc_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
@@ -251,9 +251,9 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
     if ( p->vCex )
     {
         Vec_IntClear( p->vCex );
-        for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
+        for ( i = 0; i < Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
             Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
-        for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
+        for ( i = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManCiNum(p->pManFraig); i++ )
             Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
     }
 
@@ -298,13 +298,13 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
     // determine the best pattern
     BestPat = i * 32 + k;
     // fill in the counter-example data
-    pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
+    pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pManFraig)+1 );
     Aig_ManForEachCi( p->pManAig, pObjPi, i )
     {
         pModel[i] = Abc_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
 //        printf( "%d", pModel[i] );
     }
-    pModel[Aig_ManPiNum(p->pManAig)] = pObjPo->Id;
+    pModel[Aig_ManCiNum(p->pManAig)] = pObjPo->Id;
 //    printf( "\n" );
     // set the model
     assert( p->pManFraig->pData == NULL );
@@ -328,7 +328,7 @@ int Fra_SmlCheckOutput( Fra_Man_t * p )
     Aig_Obj_t * pObj;
     int i;
     // make sure the reference simulation pattern does not detect the bug
-    pObj = Aig_ManPo( p->pManAig, 0 );
+    pObj = Aig_ManCo( p->pManAig, 0 );
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
     Aig_ManForEachCo( p->pManAig, pObj, i )
     {
@@ -359,7 +359,7 @@ void Fra_SmlAssignRandom( Fra_Sml_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
     int i;
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Fra_ObjSim( p, pObj->Id );
     for ( i = 0; i < p->nWordsTotal; i++ )
         pSims[i] = Fra_ObjRandomSim();
@@ -380,7 +380,7 @@ void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFram
 {
     unsigned * pSims;
     int i;
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
         pSims[i] = fConst1? ~(unsigned)0 : 0;
@@ -404,7 +404,7 @@ void Fra_SmlInitialize( Fra_Sml_t * p, int fInit )
     if ( fInit )
     {
         assert( Aig_ManRegNum(p->pAig) > 0 );
-        assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+        assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
         // assign random info for primary inputs
         Aig_ManForEachPiSeq( p->pAig, pObj, i )
             Fra_SmlAssignRandom( p, pObj );
@@ -441,16 +441,16 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
         Aig_ManForEachCi( p->pAig, pObj, i )
             Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
         // flip one bit
-        Limit = Abc_MinInt( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
+        Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 );
         for ( i = 0; i < Limit; i++ )
-            Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
+            Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 );
     }
     else
     {
         int fUseDist1 = 0;
 
         // copy the PI info for each frame
-        nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
+        nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig);
         for ( f = 0; f < p->nFrames; f++ )
             Aig_ManForEachPiSeq( p->pAig, pObj, i )
                 Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
@@ -458,14 +458,14 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
         k = 0;
         Aig_ManForEachLoSeq( p->pAig, pObj, i )
             Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
-//        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
+//        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pManFraig) );
 
         // flip one bit of the last frame
         if ( fUseDist1 ) //&& p->nFrames == 2 )
         {
             Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 );
             for ( i = 0; i < Limit; i++ )
-                Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
+                Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
         }
     }
 }
@@ -581,7 +581,7 @@ void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
     unsigned * pSims, * pSims0;
     int fCompl, fCompl0, i;
     assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsPo(pObj) );
+    assert( Aig_ObjIsCo(pObj) );
     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
     pSims  = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
@@ -615,8 +615,8 @@ void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
     int i;
     assert( !Aig_IsComplement(pOut) );
     assert( !Aig_IsComplement(pIn) );
-    assert( Aig_ObjIsPo(pOut) );
-    assert( Aig_ObjIsPi(pIn) );
+    assert( Aig_ObjIsCo(pOut) );
+    assert( Aig_ObjIsCi(pIn) );
     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
     pSims0 = Fra_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
@@ -918,12 +918,12 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
             }
         break;
     }
-    assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
+    assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
     assert( iFrame < p->nFrames );
     assert( iBit < 32 * p->nWordsFrame );
 
     // allocate the counter example
-    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
     pCex->iPo    = iPo;
     pCex->iFrame = iFrame;
 
@@ -972,16 +972,16 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
     // get the number of frames
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManRegNum(pFrames) == 0 );
-    nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
-    nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
-    nFrames = Aig_ManPiNum(pFrames) / nTruePis;
-    assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) );
-    assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) );
+    nTruePis = Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig);
+    nTruePos = Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig);
+    nFrames = Aig_ManCiNum(pFrames) / nTruePis;
+    assert( nTruePis * nFrames == Aig_ManCiNum(pFrames) );
+    assert( nTruePos * nFrames == Aig_ManCoNum(pFrames) );
     // find the PO that failed
     iPo = -1;
     iFrame = -1;
     Aig_ManForEachCo( pFrames, pObj, i )
-        if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] )
+        if ( pObj->Id == pModel[Aig_ManCiNum(pFrames)] )
         {
             iPo = i % nTruePos;
             iFrame = i / nTruePos;
@@ -994,7 +994,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in
     pCex->iFrame = iFrame;
 
     // copy the bit data
-    for ( i = 0; i < Aig_ManPiNum(pFrames); i++ )
+    for ( i = 0; i < Aig_ManCiNum(pFrames); i++ )
     {
         if ( pModel[i] )
             Abc_InfoSetBit( pCex->pData, pCex->nRegs + i );