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

13 files changed, 51 insertions, 51 deletions

diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c
index 8ab99f83..5cdced62 100644
--- a/src/proof/ssw/sswAig.c
+++ b/src/proof/ssw/sswAig.c
@@ -120,13 +120,13 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
     // add the constraint
     if ( fTwoPos )
     {
-        Aig_ObjCreatePo( pFrames, pObjNew2 );
-        Aig_ObjCreatePo( pFrames, pObjNew );
+        Aig_ObjCreateCo( pFrames, pObjNew2 );
+        Aig_ObjCreateCo( pFrames, pObjNew );
     }
     else
     {
         pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 );
-        Aig_ObjCreatePo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
+        Aig_ObjCreateCo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) );
     }
 }
 
@@ -155,7 +155,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
     // create latches for the first frame
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
     // add timeframes
     iLits = 0;
     for ( f = 0; f < p->pPars->nFramesK; f++ )
@@ -164,7 +164,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePi(pFrames);
+            pObjNew = Aig_ObjCreateCi(pFrames);
             pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
         }
@@ -179,7 +179,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
             Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 );
         }
         // transfer to the primary outputs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) );
         // transfer latch input to the latch outputs 
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -188,7 +188,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) );
     // add the POs for the latch outputs of the last frame
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
+        Aig_ObjCreateCo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
 
     // remove dangling nodes
     Aig_ManCleanup( pFrames );
@@ -225,10 +225,10 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
     // map constants and PIs
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
     // create latches for the first frame
     Saig_ManForEachLo( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
     // set the constraints on the latch outputs
     Saig_ManForEachLo( p->pAig, pObj, i )
         Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 );
@@ -241,7 +241,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p )
     }
     // add the POs for the latch outputs of the last frame
     Saig_ManForEachLi( p->pAig, pObj, i )
-        Aig_ObjCreatePo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
+        Aig_ObjCreateCo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) );
     // remove dangling nodes
     Aig_ManCleanup( pFrames );
     Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) );
diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index 8cb14f4a..0eabaa92 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -50,7 +50,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f )
     if ( Aig_ObjIsConst1(pObj) )
         pRes = Aig_ManConst1( pFrm->pFrames );
     else if ( Saig_ObjIsPi(pFrm->pAig, pObj) )
-        pRes = Aig_ObjCreatePi( pFrm->pFrames );
+        pRes = Aig_ObjCreateCi( pFrm->pFrames );
     else if ( Aig_ObjIsPo(pObj) )
     {
         Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f );
diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c
index 239e35b9..6d8a152d 100644
--- a/src/proof/ssw/sswConstr.c
+++ b/src/proof/ssw/sswConstr.c
@@ -63,19 +63,19 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
         // map constants and PIs
         Aig_ObjSetCopy( Aig_ManConst1(p), Aig_ManConst1(pFrames) );
         Saig_ManForEachPi( p, pObj, i )
-            Aig_ObjSetCopy( pObj, Aig_ObjCreatePi(pFrames) );
+            Aig_ObjSetCopy( pObj, Aig_ObjCreateCi(pFrames) );
         // add internal nodes of this frame
         Aig_ManForEachNode( p, pObj, i )
             Aig_ObjSetCopy( pObj, Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ) );
         // transfer to the primary output
-        Aig_ManForEachPo( p, pObj, i )
+        Aig_ManForEachCo( p, pObj, i )
             Aig_ObjSetCopy( pObj, Aig_ObjChild0Copy(pObj) );
         // create constraint outputs
         Saig_ManForEachPo( p, pObj, i )
         {
             if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
                 continue;
-            Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) );
+            Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) );
         }
         // transfer latch inputs to the latch outputs 
         Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
@@ -125,10 +125,10 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits )
     if ( RetValue == l_True && pvInits )
     {
         *pvInits = Vec_IntAlloc( 1000 );
-        Aig_ManForEachPi( pFrames, pObj, i )
+        Aig_ManForEachCi( pFrames, pObj, i )
             Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) );
 
-//        Aig_ManForEachPi( pFrames, pObj, i )
+//        Aig_ManForEachCi( pFrames, pObj, i )
 //            printf( "%d", Vec_IntEntry(*pvInits, i) );
 //        printf( "\n" );
     }
@@ -268,7 +268,7 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
         // check the outputs
         Saig_ManForEachPo( p->pAig, pObj, i )
@@ -424,7 +424,7 @@ clk = clock();
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePi(p->pFrames);
+            pObjNew = Aig_ObjCreateCi(p->pFrames);
             pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
         }
@@ -464,7 +464,7 @@ clk = clock();
         if ( f == p->pPars->nFramesK - 1 )
             break;
         // transfer latch input to the latch outputs 
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
         // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -514,7 +514,7 @@ clk = clock();
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePi(p->pFrames);
+            pObjNew = Aig_ObjCreateCi(p->pFrames);
             pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
         }
@@ -544,7 +544,7 @@ clk = clock();
         if ( f == p->pPars->nFramesK - 1 )
             break;
         // transfer latch input to the latch outputs 
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
         // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -648,7 +648,7 @@ clk = clock();
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
     {
-        pObjNew = Aig_ObjCreatePi(p->pFrames);
+        pObjNew = Aig_ObjCreateCi(p->pFrames);
         pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++);
         Ssw_ObjSetFrame( p, pObj, f, pObjNew );
     }
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index d9a16e22..0f6002fa 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -215,7 +215,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
     int i, f, nFrames;
 
     // transfer simulation information
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
     {
         pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
         if ( pObjFraig == Aig_ManConst0(p->pFrames) )
@@ -385,7 +385,7 @@ clk = clock();
     f = p->pPars->nFramesK;
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
     Aig_ManSetPioNumbers( p->pFrames );
     // label nodes corresponding to primary inputs
     Ssw_ManLabelPiNodes( p );
diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c
index 4f6fb26e..536316ff 100644
--- a/src/proof/ssw/sswFilter.c
+++ b/src/proof/ssw/sswFilter.c
@@ -65,7 +65,7 @@ void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
         // transfer
         if ( f == 0 )
@@ -115,7 +115,7 @@ void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
     }
     // record the new pattern
@@ -157,7 +157,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
     }
     assert( iBit == pCex->nBits );
@@ -317,7 +317,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePi(p->pFrames);
+            pObjNew = Aig_ObjCreateCi(p->pFrames);
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
         }
         // sweep internal nodes
@@ -351,7 +351,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit )
         if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
             break;
         // transfer latch input to the latch outputs 
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
         // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c
index ca95cf23..3173ec6f 100644
--- a/src/proof/ssw/sswIslands.c
+++ b/src/proof/ssw/sswIslands.c
@@ -90,7 +90,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs )
         assert( pObj1->pData == pObj0 );
     }
     // make sure the POs are not matched
-    Aig_ManForEachPo( p0, pObj0, i )
+    Aig_ManForEachCo( p0, pObj0, i )
     {
         pObj1 = Aig_ManPo( p1, i );
         assert( pObj0->pData == NULL );
@@ -295,7 +295,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
     {
         if ( pObj0->pData != NULL )
             continue;
-        pObj1 = Aig_ObjCreatePi( p1 );
+        pObj1 = Aig_ObjCreateCi( p1 );
         pObj0->pData = pObj1;
         pObj1->pData = pObj0;
         Vec_PtrPush( vNewLis, pObj0Li );
@@ -311,7 +311,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 )
     }
     // create register outputs in p0 that are absent in p1
     Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i )
-        Aig_ObjCreatePo( p1, Aig_ObjChild0Copy(pObj0Li) );
+        Aig_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) );
     // increment the number of registers
     Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
     Vec_PtrFree( vNewLis );
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index ce9c2563..c41a74ef 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -49,7 +49,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
     unsigned * pInfo;
     int i;
     // transfer simulation information
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
     {
         pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
         if ( pObjFraig == Aig_ManConst0(p->pFrames) )
@@ -245,7 +245,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
     // map constants and PIs
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(p->pFrames) );
 
     // implement equivalence classes
     Saig_ManForEachLo( p->pAig, pObj, i )
@@ -253,7 +253,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
         pRepr = Aig_ObjRepr( p->pAig, pObj );
         if ( pRepr == NULL )
         {
-            pTemp = Aig_ObjCreatePi(p->pFrames);
+            pTemp = Aig_ObjCreateCi(p->pFrames);
             pTemp->pData = pObj;
         }
         else
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 25a80be7..6e36ae12 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -587,7 +587,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
     Aig_ManIncrementTravId( p->pAig );
     // check comb inputs
     if ( fUpdate )
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
     {
         pRepr = Aig_ObjRepr(p->pAig, pObj);
         if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
@@ -631,7 +631,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
         }
     }
     // transfer to POs
-    Aig_ManForEachPo( p->pAig, pObj, i )
+    Aig_ManForEachCo( p->pAig, pObj, i )
     {
         pSim  = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
         pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
@@ -826,7 +826,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ManForEachCo( pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
     }
     assert( iBit == pCex->nBits );
diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c
index ac22b0d5..dce7ac3e 100644
--- a/src/proof/ssw/sswRarity2.c
+++ b/src/proof/ssw/sswRarity2.c
@@ -277,7 +277,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
                          & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
         // assign the COs
-        Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ManForEachCo( pAig, pObj, i )
             pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
     }
     assert( iBit == pCex->nBits );
diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c
index ec50ab50..a04f6f54 100644
--- a/src/proof/ssw/sswSemi.c
+++ b/src/proof/ssw/sswSemi.c
@@ -198,7 +198,7 @@ clk = clock();
         // map constants and PIs
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
-            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c
index 9ce89a71..946224cd 100644
--- a/src/proof/ssw/sswSim.c
+++ b/src/proof/ssw/sswSim.c
@@ -458,7 +458,7 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo )
     BestPat = i * 32 + k;
     // fill in the counter-example data
     pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pAig)+1 );
-    Aig_ManForEachPi( p->pAig, pObjPi, i )
+    Aig_ManForEachCi( p->pAig, pObjPi, i )
     {
         pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
 //        printf( "%d", pModel[i] );
@@ -486,7 +486,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
     // make sure the reference simulation pattern does not detect the bug
     pObj = Aig_ManPo( p->pAig, 0 );
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
-    Aig_ManForEachPo( p->pAig, pObj, i )
+    Aig_ManForEachCo( p->pAig, pObj, i )
     {
         if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
         {
@@ -628,7 +628,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
     if ( p->nFrames == 1 )
     {
         // copy the PI info 
-        Aig_ManForEachPi( p->pAig, pObj, i )
+        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 );
@@ -678,7 +678,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
     assert( p->nFrames > 0 );
 
     // copy the pattern into the primary inputs
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
 
     // set distance one PIs for the first frame
@@ -909,7 +909,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
     }
     else
     {
-        Aig_ManForEachPi( p->pAig, pObj, i )
+        Aig_ManForEachCi( p->pAig, pObj, i )
             Ssw_SmlAssignRandom( p, pObj );
     }
 }
diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c
index 4c094a2d..098b1e0f 100644
--- a/src/proof/ssw/sswSimSat.c
+++ b/src/proof/ssw/sswSimSat.c
@@ -48,7 +48,7 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
     int i, RetValue1, RetValue2, clk = clock();
     // set the PI simulation information
     Aig_ManConst1(p->pAig)->fMarkB = 1;
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         pObj->fMarkB = Abc_InfoHasBit( p->pPatWords, i );
     // simulate internal nodes
     Aig_ManForEachNode( p->pAig, pObj, i )
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index e2a4f65d..a3a8d1c8 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -117,7 +117,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
     Aig_Obj_t * pObj;
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
             Abc_InfoSetBit( p->pPatWords, i );
 }
@@ -138,7 +138,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
     Aig_Obj_t * pObj;
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pAig, pObj, i )
+    Aig_ManForEachCi( p->pAig, pObj, i )
         if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
             Abc_InfoSetBit( p->pPatWords, i );
 }
@@ -284,7 +284,7 @@ clk = clock();
         // map constants and PIs
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
-            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+            Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
@@ -298,7 +298,7 @@ clk = clock();
         if ( f == p->pPars->nFramesK - 1 )
             break;
         // transfer latch input to the latch outputs 
-        Aig_ManForEachPo( p->pAig, pObj, i )
+        Aig_ManForEachCo( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) );
         // build logic cones for register outputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
@@ -393,7 +393,7 @@ clk = clock();
     f = p->pPars->nFramesK;
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
-        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
 p->timeReduce += clock() - clk;
 
     // sweep internal nodes