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

17 files changed, 85 insertions, 85 deletions

diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c
index 5cdced62..cd0f0c7a 100644
--- a/src/proof/ssw/sswAig.c
+++ b/src/proof/ssw/sswAig.c
@@ -148,7 +148,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     int i, f, iLits;
     assert( p->pFrames == NULL );
     assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
     p->nConstrTotal = p->nConstrReduced = 0;
 
     // start the fraig package
@@ -216,7 +216,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
     int i;
     assert( p->pFrames == NULL );
     assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
     p->nConstrTotal = p->nConstrReduced = 0;
  
     // start the fraig package
diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index 0eabaa92..b2920177 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -51,7 +51,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
         pRes = Aig_ManConst1( pFrm->pFrames );
     else if ( Saig_ObjIsPi(pFrm->pAig, pObj) )
         pRes = Aig_ObjCreateCi( pFrm->pFrames );
-    else if ( Aig_ObjIsPo(pObj) )
+    else if ( Aig_ObjIsCo(pObj) )
     {
         Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
         pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f );
diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c
index 95f029d4..581b8aed 100644
--- a/src/proof/ssw/sswClass.c
+++ b/src/proof/ssw/sswClass.c
@@ -642,7 +642,7 @@ clk = clock();
         }
         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 )
diff --git a/src/proof/ssw/sswCnf.c b/src/proof/ssw/sswCnf.c
index 1970c62f..e3b422d5 100644
--- a/src/proof/ssw/sswCnf.c
+++ b/src/proof/ssw/sswCnf.c
@@ -276,7 +276,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
 void Ssw_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) || 
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || 
          (!fFirst && Aig_ObjRefs(pObj) > 1) || 
          (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
     {
@@ -303,7 +303,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
 void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
 {
     assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsPi(pObj) );
+    assert( !Aig_ObjIsCi(pObj) );
     Vec_PtrClear( vSuper );
     Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
 }
@@ -329,7 +329,7 @@ void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
         return;
 //    pObj->fMarkA = 1;
     // save PIs (used by register correspondence)
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         Vec_PtrPush( p->vUsedPis, pObj );
     Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
     sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) );
@@ -408,7 +408,7 @@ int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj )
         return sat_solver_var_value( p->pSat, nVarNum );
 //    if ( pObj->fMarkA == 1 )
 //        return 0;
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return 0;
     assert( Aig_ObjIsNode(pObj) );
     Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) );
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 6d8a152d..82977edb 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -51,7 +51,7 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
     int i, f;
     assert( Saig_ManConstrNum(p) > 0 );
     assert( Aig_ManRegNum(p) > 0 );
-    assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) );
+    assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
     // start the fraig package
     pFrames = Aig_ManStart( Aig_ManObjNumMax(p) * nFrames );
     // create latches for the first frame
@@ -165,7 +165,7 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
     assert( p->nConstrs > 0 );
     // create CNF
     nRegs = p->nRegs; p->nRegs = 0;
-    pCnf = Cnf_Derive( p, Aig_ManPoNum(p) );  
+    pCnf = Cnf_Derive( p, Aig_ManCoNum(p) );  
     p->nRegs = nRegs;  
     // create SAT solver
     pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
@@ -626,18 +626,18 @@ clk = clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
     // add constants
-    nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
     assert( (nConstrPairs & 1) == 0 );
     for ( i = 0; i < nConstrPairs; i += 2 )
     {
-        pObj  = Aig_ManPo( p->pFrames, i   );
-        pObj2 = Aig_ManPo( p->pFrames, i+1 );
+        pObj  = Aig_ManCo( p->pFrames, i   );
+        pObj2 = Aig_ManCo( p->pFrames, i+1 );
         Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
     }
     // build logic cones for register inputs
     for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
     {
-        pObj  = Aig_ManPo( p->pFrames, nConstrPairs + i );
+        pObj  = Aig_ManCo( p->pFrames, nConstrPairs + i );
         Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
     }
 
diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c
index df48a5b8..c51d421c 100644
--- a/src/proof/ssw/sswCore.c
+++ b/src/proof/ssw/sswCore.c
@@ -191,13 +191,13 @@ void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose )
     Aig_Obj_t * pObj;
     int i, nTotal = 0, nRemoved = 0;
     // collect the nodes in the cone of constraints
-    pArray  = (Aig_Obj_t **)Vec_PtrArray(pAig->vPos);
+    pArray  = (Aig_Obj_t **)Vec_PtrArray(pAig->vCos);
     pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig);
     vCones  = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) );
     // remove all the node that are equiv to something and are in the cones
     Aig_ManForEachObj( pAig, pObj, i )
     {
-        if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
             continue;
         if ( pAig->pReprs[i] != NULL )
             nTotal++;
@@ -213,7 +213,7 @@ void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose )
         }
     }
     // collect statistics    
-    p->nConesTotal   = Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig);
+    p->nConesTotal   = Aig_ManCiNum(pAig) + Aig_ManNodeNum(pAig);
     p->nConesConstr  = Vec_PtrSize(vCones);
     p->nEquivsTotal  = nTotal;
     p->nEquivsConstr = nRemoved;
@@ -341,7 +341,7 @@ clk = clock();
                     printf( "R =%4d. ",   p->nRecycles-nRecycles );
                 }
                 printf( "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal, 
-                    (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManPo(p->pAig,0))))? "+" : "-" );
+                    (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" );
                 ABC_PRT( "T", clock() - clk );
             } 
 //            if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 )
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index 0f6002fa..f20a7b78 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -54,7 +54,7 @@ void Ssw_ManLabelPiNodes( Ssw_Man_t * p )
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
             pObjFrames = Ssw_ObjFrame( p, pObj, f );
-            assert( Aig_ObjIsPi(pObjFrames) );
+            assert( Aig_ObjIsCi(pObjFrames) );
             assert( pObjFrames->fMarkB == 0 );
             pObjFrames->fMarkA = 1;
             pObjFrames->fMarkB = 1;
@@ -79,7 +79,7 @@ void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
     if ( pObj->fMarkA )
         return;
     pObj->fMarkA = 1;
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Vec_PtrPush( vNewPis, pObj );
         return;
@@ -110,10 +110,10 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos
     pObj->fMarkB = 1;
     if ( pObj->Id > p->nSRMiterMaxId )
         return;
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         // skip if it is a register input PO
-        if ( Aig_ObjPioNum(pObj) >= Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
+        if ( Aig_ObjPioNum(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
             return;
         // add the number of this constraint
         Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 );
@@ -180,8 +180,8 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
     // check if the corresponding pairs are added
     Vec_IntForEachEntry( p->vNewPos, iConstr, i )
     {
-        pObj0 = Aig_ManPo( p->pFrames, 2*iConstr   );
-        pObj1 = Aig_ManPo( p->pFrames, 2*iConstr+1 );
+        pObj0 = Aig_ManCo( p->pFrames, 2*iConstr   );
+        pObj1 = Aig_ManCo( p->pFrames, 2*iConstr+1 );
 //        if ( pObj0->fMarkB && pObj1->fMarkB )
         if ( pObj0->fMarkB || pObj1->fMarkB )
         {
@@ -224,7 +224,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
             continue;
         }
         assert( !Aig_IsComplement(pObjFraig) );
-        assert( Aig_ObjIsPi(pObjFraig) );
+        assert( Aig_ObjIsCi(pObjFraig) );
         pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
         Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
     }
@@ -235,7 +235,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
         {
             pObjFraig = Ssw_ObjFrame( p, pObj, f );
             assert( !Aig_IsComplement(pObjFraig) );
-            assert( Aig_ObjIsPi(pObjFraig) );
+            assert( Aig_ObjIsCi(pObjFraig) );
             pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
             Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
         }
@@ -393,7 +393,7 @@ p->timeReduce += clock() - clk;
 
     // prepare simulation info
     assert( p->vSimInfo == NULL );
-    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
 
     // sweep internal nodes
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 536316ff..5f467123 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -162,7 +162,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
     }
     assert( iBit == pCex->nBits );
     // check that the output failed as expected -- cannot check because it is not an SRM!
-//    pObj = Aig_ManPo( p->pAig, pCex->iPo );
+//    pObj = Aig_ManCo( p->pAig, pCex->iPo );
 //    if ( pObj->fMarkB != 1 )
 //        printf( "The counter-example does not refine the output.\n" );
     // record the new pattern
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index 3173ec6f..8f54432d 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -85,14 +85,14 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
     // make sure PIs are matched
     Saig_ManForEachPi( p0, pObj0, i )
     {
-        pObj1 = Aig_ManPi( p1, i );
+        pObj1 = Aig_ManCi( p1, i );
         assert( pObj0->pData == pObj1 );
         assert( pObj1->pData == pObj0 );
     }
     // make sure the POs are not matched
     Aig_ManForEachCo( p0, pObj0, i )
     {
-        pObj1 = Aig_ManPo( p1, i );
+        pObj1 = Aig_ManCo( p1, i );
         assert( pObj0->pData == NULL );
         assert( pObj1->pData == NULL );
     }
@@ -135,7 +135,7 @@ void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
     Aig_ManIncrementTravId( p );
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         if ( pObj->pData != NULL )
             continue;
@@ -196,7 +196,7 @@ int Ssw_MatchingCountUnmached( Aig_Man_t * p )
     int i, Counter = 0;
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         if ( pObj->pData != NULL )
             continue;
@@ -230,8 +230,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
         int nUnmached = Ssw_MatchingCountUnmached(p0);
         printf( "Extending islands by %d steps:\n", nDist );
         printf( "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
-            0, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0), 
-            nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
+            0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), 
+            nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
     }
     for ( d = 0; d < nDist; d++ )
     {
@@ -263,8 +263,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose
         {
             int nUnmached = Ssw_MatchingCountUnmached(p0);
             printf( "%2d : Total = %6d. Unmatched = %6d.  Ratio = %6.2f %%\n",
-                d+1, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0), 
-                nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) );
+                d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), 
+                nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
         }
     }
     Vec_PtrFree( vNodes0 );
@@ -335,15 +335,15 @@ Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 )
     Aig_Obj_t * pObj0, * pObj1;
     int i;
     // check correctness
-    assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) );
-    assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) );
+    assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
+    assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
     assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) );
     assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) );
     // create complete pairs
     vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
     Aig_ManForEachObj( p0, pObj0, i )
     {
-        if ( Aig_ObjIsPo(pObj0) )
+        if ( Aig_ObjIsCo(pObj0) )
             continue;
         pObj1 = (Aig_Obj_t *)pObj0->pData;
         Vec_IntPush( vPairsNew, pObj0->Id );
@@ -390,7 +390,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p
         assert( !Aig_IsComplement(pObj0) );
         assert( !Aig_IsComplement(pObj1) );
         assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
-        if ( Aig_ObjIsPo(pObj0) )
+        if ( Aig_ObjIsCo(pObj0) )
             continue;
         assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) );
         assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) );
@@ -519,7 +519,7 @@ Vec_Int_t * Saig_StrSimPerformMatching_hack( Aig_Man_t * p0, Aig_Man_t * p1 )
     vPairs = Vec_IntAlloc( 100 );
     Aig_ManForEachObj( p0, pObj, i )
     {
-        if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
             continue;
         Vec_IntPush( vPairs, i );
         Vec_IntPush( vPairs, i );
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index c41a74ef..ec6087f0 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -58,7 +58,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
             continue;
         }
         assert( !Aig_IsComplement(pObjFraig) );
-        assert( Aig_ObjIsPi(pObjFraig) );
+        assert( Aig_ObjIsCi(pObjFraig) );
         pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
         Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
     }
@@ -160,8 +160,8 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
 {
     Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
     int RetValue, clk;
-    assert( Aig_ObjIsPi(pObj) );
-    assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
+    assert( Aig_ObjIsCi(pObj) );
+    assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
     // check if it makes sense to skip some calls
     if ( p->nCallsCount > 100 && p->nCallsUnsat < p->nCallsSat )
     {
@@ -175,7 +175,7 @@ clk = clock();
     Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
     pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
     // get the fraiged representative
-    if ( Aig_ObjIsPi(pObjRepr) )
+    if ( Aig_ObjIsCi(pObjRepr) )
     {
         pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr ); 
         Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
@@ -264,7 +264,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
 
     // prepare simulation info
     assert( p->vSimInfo == NULL );
-    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
     Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
 
     // go through the registers
diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c
index 0aba942f..e356aa60 100644
--- a/src/proof/ssw/sswPairs.c
+++ b/src/proof/ssw/sswPairs.c
@@ -64,7 +64,7 @@ int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose )
             continue;
         }
         // check if the output is a primary input
-        if ( p->nRegs == 0 && Aig_ObjIsPi(Aig_Regular(pChild)) )
+        if ( p->nRegs == 0 && Aig_ObjIsCi(Aig_Regular(pChild)) )
         {
             CountNonConst0++;
             continue;
diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
index d2f07dc8..5a3aea10 100644
--- a/src/proof/ssw/sswPart.c
+++ b/src/proof/ssw/sswPart.c
@@ -90,7 +90,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_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 );
         }
     }
@@ -110,7 +110,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_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 );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 6e36ae12..445dda84 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -831,7 +831,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
     }
     assert( iBit == pCex->nBits );
     // check that the output failed as expected -- cannot check because it is not an SRM!
-//    pObj = Aig_ManPo( pAig, pCex->iPo );
+//    pObj = Aig_ManCo( pAig, pCex->iPo );
 //    if ( pObj->fMarkB != 1 )
 //        printf( "The counter-example does not refine the output.\n" );
     // record the new pattern
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index dce7ac3e..0851cf3d 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -282,7 +282,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
     }
     assert( iBit == pCex->nBits );
     // check that the output failed as expected -- cannot check because it is not an SRM!
-//    pObj = Aig_ManPo( pAig, pCex->iPo );
+//    pObj = Aig_ManCo( pAig, pCex->iPo );
 //    if ( pObj->fMarkB != 1 )
 //        printf( "The counter-example does not refine the output.\n" );
     // record the new pattern
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index 946224cd..b53e8baf 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -457,13 +457,13 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_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->pAig)+1 );
+    pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pAig)+1 );
     Aig_ManForEachCi( p->pAig, pObjPi, i )
     {
         pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
 //        printf( "%d", pModel[i] );
     }
-    pModel[Aig_ManPiNum(p->pAig)] = pObjPo->Id;
+    pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id;
 //    printf( "\n" );
     return pModel;
 }
@@ -484,7 +484,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
     Aig_Obj_t * pObj;
     int i;
     // make sure the reference simulation pattern does not detect the bug
-    pObj = Aig_ManPo( p->pAig, 0 );
+    pObj = Aig_ManCo( p->pAig, 0 );
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
     Aig_ManForEachCo( p->pAig, pObj, i )
     {
@@ -514,7 +514,7 @@ void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
     int i, f;
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id );
     for ( i = 0; i < p->nWordsTotal; i++ )
         pSims[i] = Ssw_ObjRandomSim();
@@ -540,7 +540,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
     unsigned * pSims;
     int i;
     assert( iFrame < p->nFrames );
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
         pSims[i] = Ssw_ObjRandomSim();
@@ -562,7 +562,7 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
     unsigned * pSims;
     int i;
     assert( iFrame < p->nFrames );
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
         pSims[i] = fConst1? ~(unsigned)0 : 0;
@@ -584,7 +584,7 @@ void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, in
     unsigned * pSims;
     assert( iFrame < p->nFrames );
     assert( iWord < p->nWordsFrame );
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     pSims[iWord] = fConst1? ~(unsigned)0 : 0;
 } 
@@ -604,7 +604,7 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor
 {
     unsigned * pSims;
     assert( iFrame < p->nFrames );
-    assert( Aig_ObjIsPi(pObj) );
+    assert( Aig_ObjIsCi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     pSims[iWord] = Word;
 } 
@@ -631,16 +631,16 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
         Aig_ManForEachCi( p->pAig, pObj, i )
             Ssw_SmlObjAssignConst( 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( Ssw_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
+            Abc_InfoXorBit( Ssw_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++ )
             Saig_ManForEachPi( p->pAig, pObj, i )
                 Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
@@ -648,14 +648,14 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
         k = 0;
         Saig_ManForEachLo( p->pAig, pObj, i )
             Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
-//        assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pFrames) );
+//        assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pFrames) );
 
         // 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( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
+                Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
         }
     }
 }
@@ -684,7 +684,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
     // set distance one PIs for the first frame
     Limit = Abc_MinInt( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
     for ( i = 0; i < Limit; i++ )
-        Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
+        Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ), i+1 );
 
     // create random info for the remaining timeframes
     for ( f = 1; f < p->nFrames; f++ )
@@ -806,7 +806,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
     int fCompl, fCompl0, i;
     assert( iFrame < p->nFrames );
     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  = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
@@ -841,8 +841,8 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
     assert( iFrame < p->nFrames );
     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 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
@@ -869,8 +869,8 @@ void Ssw_SmlNodeTransferFirst( Ssw_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( p->nWordsFrame < p->nWordsTotal );
     // get hold of the simulation information
     pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * (p->nFrames-1);
@@ -899,7 +899,7 @@ void Ssw_SmlInitialize( Ssw_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
         Saig_ManForEachPi( p->pAig, pObj, i )
             Ssw_SmlAssignRandom( p, pObj );
@@ -931,7 +931,7 @@ void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit )
     int Entry, i, nRegs;
     nRegs = Aig_ManRegNum(p->pAig);
     assert( nRegs > 0 );
-    assert( nRegs <= Aig_ManPiNum(p->pAig) );
+    assert( nRegs <= Aig_ManCiNum(p->pAig) );
     assert( Vec_IntSize(vInit) == nRegs * p->nWordsFrame );
     // assign random info for primary inputs
     Saig_ManForEachPi( p->pAig, pObj, i )
@@ -957,7 +957,7 @@ void Ssw_SmlReinitialize( Ssw_Sml_t * p )
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int i;
     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
     Saig_ManForEachPi( p->pAig, pObj, i )
         Ssw_SmlAssignRandom( p, pObj );
@@ -1361,12 +1361,12 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_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;
 
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index a3a8d1c8..550cb4ce 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -48,7 +48,7 @@ int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
     int fUseNoBoundary = 0;
     Aig_Obj_t * pObjFraig;
     int Value;
-//    assert( Aig_ObjIsPi(pObj) );
+//    assert( Aig_ObjIsCi(pObj) );
     pObjFraig = Ssw_ObjFrame( p, pObj, f );
     if ( fUseNoBoundary )
     {
@@ -86,12 +86,12 @@ void Ssw_CheckConstraints( Ssw_Man_t * p )
     Aig_Obj_t * pObj, * pObj2;
     int nConstrPairs, i;
     int Counter = 0;
-    nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
     assert( (nConstrPairs & 1) == 0 );
     for ( i = 0; i < nConstrPairs; i += 2 )
     {
-        pObj  = Aig_ManPo( p->pFrames, i   );
-        pObj2 = Aig_ManPo( p->pFrames, i+1 );
+        pObj  = Aig_ManCo( p->pFrames, i   );
+        pObj2 = Aig_ManCo( p->pFrames, i+1 );
         if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 )
         {
             Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
@@ -162,7 +162,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
     // iterate through the PIs of the frames
     Vec_PtrForEachEntry( Aig_Obj_t *, p->pMSat->vUsedPis, pObj, i )
     {
-        assert( Aig_ObjIsPi(pObj) );
+        assert( Aig_ObjIsCi(pObj) );
         nVarNum = Ssw_ObjSatNum( p->pMSat, pObj );
         assert( nVarNum > 0 );
         if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) )
@@ -373,18 +373,18 @@ clk = clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
     // add constants
-    nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+    nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
     assert( (nConstrPairs & 1) == 0 );
     for ( i = 0; i < nConstrPairs; i += 2 )
     {
-        pObj  = Aig_ManPo( p->pFrames, i   );
-        pObj2 = Aig_ManPo( p->pFrames, i+1 );
+        pObj  = Aig_ManCo( p->pFrames, i   );
+        pObj2 = Aig_ManCo( p->pFrames, i+1 );
         Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
     }
     // build logic cones for register inputs
     for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
     {
-        pObj  = Aig_ManPo( p->pFrames, nConstrPairs + i );
+        pObj  = Aig_ManCo( p->pFrames, nConstrPairs + i );
         Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
     }
     sat_solver_simplify( p->pMSat->pSat );
diff --git a/src/proof/ssw/sswUnique.c b/src/proof/ssw/sswUnique.c
index b5f6a853..8e989531 100644
--- a/src/proof/ssw/sswUnique.c
+++ b/src/proof/ssw/sswUnique.c
@@ -105,7 +105,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
     k = 0;
     Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i )
     {
-        assert( Aig_ObjIsPi(pTemp) );
+        assert( Aig_ObjIsCi(pTemp) );
         if ( !Saig_ObjIsLo(p->pAig, pTemp) )
             continue;
         assert( Aig_ObjPioNum(pTemp) > 0 );