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

13 files changed, 43 insertions, 43 deletions

diff --git a/src/proof/llb/llb1Constr.c b/src/proof/llb/llb1Constr.c
index 4ce911db..1ef4ce14 100644
--- a/src/proof/llb/llb1Constr.c
+++ b/src/proof/llb/llb1Constr.c
@@ -150,7 +150,7 @@ void Llb_ManComputeIndCase( Aig_Man_t * p, DdManager * dd, Vec_Int_t * vNodes )
     Vec_PtrWriteEntry( vBdds, Aig_ObjId(Aig_ManConst1(p)), bFunc );
     Saig_ManForEachPi( p, pObj, i )
     {
-        bFunc = Cudd_bddIthVar( dd, Aig_ManPiNum(p) + i );  Cudd_Ref( bFunc );
+        bFunc = Cudd_bddIthVar( dd, Aig_ManCiNum(p) + i );  Cudd_Ref( bFunc );
         Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc );
     }
     Saig_ManForEachLi( p, pObj, i )
@@ -201,11 +201,11 @@ Vec_Int_t * Llb_ManComputeBaseCase( Aig_Man_t * p, DdManager * dd )
     Vec_Int_t * vNodes;
     Aig_Obj_t * pObj, * pRoot;
     int i;
-    pRoot = Aig_ManPo( p, 0 );
+    pRoot = Aig_ManCo( p, 0 );
     vNodes = Vec_IntStartFull( Aig_ManObjNumMax(p) );
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         if ( Cudd_bddLeq( dd, (DdNode *)pObj->pData, Cudd_Not(pRoot->pData) ) )
             Vec_IntWriteEntry( vNodes, i, 1 );
@@ -232,7 +232,7 @@ DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p )
     DdNode * bBdd0, * bBdd1;
     Aig_Obj_t * pObj;
     int i;
-    dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    dd = Cudd_Init( Aig_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
     pObj = Aig_ManConst1(p);
     pObj->pData = Cudd_ReadOne(dd);  Cudd_Ref( (DdNode *)pObj->pData );
diff --git a/src/proof/llb/llb1Core.c b/src/proof/llb/llb1Core.c
index ee697748..56e0cc6b 100644
--- a/src/proof/llb/llb1Core.c
+++ b/src/proof/llb/llb1Core.c
@@ -89,7 +89,7 @@ void Llb_ManPrintAig( Llb_Man_t * p )
     Abc_Print( 1, "pi =%3d  ",    Saig_ManPiNum(p->pAig) );
     Abc_Print( 1, "po =%3d  ",    Saig_ManPoNum(p->pAig) );
     Abc_Print( 1, "ff =%3d  ",    Saig_ManRegNum(p->pAig) );
-    Abc_Print( 1, "int =%5d  ",   Vec_IntSize(p->vVar2Obj)-Aig_ManPiNum(p->pAig)-Saig_ManRegNum(p->pAig) );
+    Abc_Print( 1, "int =%5d  ",   Vec_IntSize(p->vVar2Obj)-Aig_ManCiNum(p->pAig)-Saig_ManRegNum(p->pAig) );
     Abc_Print( 1, "var =%5d  ",   Vec_IntSize(p->vVar2Obj) );
     Abc_Print( 1, "part =%5d  ",  Vec_PtrSize(p->vGroups)-2 );
     Abc_Print( 1, "and =%5d  ",   Aig_ManNodeNum(p->pAig) );
diff --git a/src/proof/llb/llb1Group.c b/src/proof/llb/llb1Group.c
index c61f3a30..1099b2cd 100644
--- a/src/proof/llb/llb1Group.c
+++ b/src/proof/llb/llb1Group.c
@@ -95,7 +95,7 @@ void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vN
     Aig_ObjSetTravIdCurrent(pAig, pObj);
     if ( Aig_ObjIsConst1(pObj) )
         return;
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes );
         return;
@@ -180,7 +180,7 @@ Llb_Grp_t * Llb_ManGroupCreate( Llb_Man_t * pMan, Aig_Obj_t * pObj )
     p = Llb_ManGroupAlloc( pMan );
     Vec_PtrPush( p->vOuts, pObj );
     Aig_ManIncrementTravId( pMan->pAig );
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
         Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns );
     else
     {
diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c
index 6e705a38..51d3a9fc 100644
--- a/src/proof/llb/llb1Hint.c
+++ b/src/proof/llb/llb1Hint.c
@@ -103,7 +103,7 @@ Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int
     vFanouts = Vec_IntAlloc( 100 );
     Aig_ManForEachObj( pAig, pObj, i )
     {
-//        if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
+//        if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
         if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
             continue;
         Vec_IntPush( vFanouts, Aig_ObjRefs(pObj) );
@@ -117,7 +117,7 @@ Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int
     vResult = Vec_IntAlloc( 100 );
     Aig_ManForEachObj( pAig, pObj, i )
     {
-//        if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
+//        if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
         if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) )
             continue;
         if ( Aig_ObjRefs(pObj) < PivotValue )
diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c
index d8c667ae..60124378 100644
--- a/src/proof/llb/llb1Reach.c
+++ b/src/proof/llb/llb1Reach.c
@@ -69,7 +69,7 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager
         Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
     }
     Vec_PtrFree( vNodes );
-    if ( Aig_ObjIsPo(pNode) )
+    if ( Aig_ObjIsCo(pNode) )
         bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) );
     Cudd_Deref( bFunc );
     dd->TimeStop = TimeStop;
@@ -113,7 +113,7 @@ DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
     bRes = Cudd_ReadOne( p->dd );   Cudd_Ref( bRes );
     Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
     {
-        if ( Aig_ObjIsPo(pObj) )
+        if ( Aig_ObjIsCo(pObj) )
             bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
         else
             bBdd0 = (DdNode *)pObj->pData;
@@ -413,7 +413,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
     if ( vHints == NULL )
         return Cudd_ReadOne( p->dd );
     TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
-    assert( Aig_ManPiNum(p->pAig) == Aig_ManPiNum(p->pAigGlo) );
+    assert( Aig_ManCiNum(p->pAig) == Aig_ManCiNum(p->pAigGlo) );
     // assign const and PI nodes to the original AIG
     Aig_ManCleanData( p->pAig );
     Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd );
@@ -431,7 +431,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
     Aig_ManCleanData( p->pAigGlo );
     Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
     Aig_ManForEachCi( p->pAigGlo, pObj, i )
-        pObj->pData = Aig_ManPi(p->pAig, i)->pData;
+        pObj->pData = Aig_ManCi(p->pAig, i)->pData;
     // derive consraints
     bConstr = Cudd_ReadOne( p->dd );   Cudd_Ref( bConstr );
     Vec_IntForEachEntry( vHints, Entry, i )
@@ -595,7 +595,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
     assert( p->ddG == NULL );
     assert( p->ddR == NULL );
     p->dd  = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    p->ddR = Cudd_Init( Aig_ManPiNum(p->pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    p->ddR = Cudd_Init( Aig_ManCiNum(p->pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     if ( pddGlo && *pddGlo )
         p->ddG = *pddGlo, *pddGlo = NULL; 
     else
diff --git a/src/proof/llb/llb2Bad.c b/src/proof/llb/llb2Bad.c
index 9aecb9ff..f4359493 100644
--- a/src/proof/llb/llb2Bad.c
+++ b/src/proof/llb/llb2Bad.c
@@ -48,7 +48,7 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
     DdNode * bBdd0, * bBdd1, * bTemp, * bResult;
     Aig_Obj_t * pObj;
     int i, k;
-    assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
+    assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
     // initialize elementary variables
     Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd );
     Saig_ManForEachLo( pInit, pObj, i )
@@ -56,7 +56,7 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
     Saig_ManForEachPi( pInit, pObj, i )
         pObj->pData = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i );
     // compute internal nodes
-    vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vPos), Saig_ManPoNum(pInit) );
+    vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vCos), Saig_ManPoNum(pInit) );
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         if ( !Aig_ObjIsNode(pObj) )
@@ -111,7 +111,7 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc )
     DdNode * bVar, * bCube, * bTemp;
     Aig_Obj_t * pObj;
     int i, TimeStop;
-    assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) );
+    assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) );
     TimeStop = dd->TimeStop; dd->TimeStop = 0;
     // create PI cube
     bCube = Cudd_ReadOne( dd );  Cudd_Ref( bCube );
diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c
index 626acbd2..3b98c32a 100644
--- a/src/proof/llb/llb2Core.c
+++ b/src/proof/llb/llb2Core.c
@@ -622,7 +622,7 @@ Llb_Img_t * Llb_CoreStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t *
     p->pPars = pPars;
     p->dd    = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     p->ddG   = Cudd_Init( Aig_ManRegNum(pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    p->ddR   = Cudd_Init( Aig_ManPiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    p->ddR   = Cudd_Init( Aig_ManCiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
     Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
     Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c
index 295f0bfe..a1db70d3 100644
--- a/src/proof/llb/llb2Flow.c
+++ b/src/proof/llb/llb2Flow.c
@@ -194,7 +194,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
     if ( fShowMatrix )
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
             continue;
         Vec_PtrForEachEntry( Vec_Int_t *, vMaps, vMap, k )
             if ( Vec_IntEntry(vMap, i) )
@@ -276,7 +276,7 @@ int Llb_ManCutLiNum( Aig_Man_t * p, Vec_Ptr_t * vMinCut )
     int i, k, iFanout = -1, Counter = 0;
     Vec_PtrForEachEntry( Aig_Obj_t *, vMinCut, pObj, i )
     {
-        if ( Aig_ObjIsPi(pObj) )
+        if ( Aig_ObjIsCi(pObj) )
             continue;
         Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k )
         {
@@ -547,7 +547,7 @@ void Llb_ManResultPrint( Aig_Man_t * p, Vec_Ptr_t * vResult )
 int Llb_ManFlowBwdPath2_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pFanout;
-    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) );
+    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) );
     // skip visited nodes
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return 0;
@@ -607,7 +607,7 @@ void Llb_ManFlowLabelTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
+    if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
         return;
     assert( Aig_ObjIsNode(pObj) );
     Llb_ManFlowLabelTfi_rec( p, Aig_ObjFanin0(pObj) );
@@ -638,7 +638,7 @@ void Llb_ManFlowUpdateCut( Aig_Man_t * p, Vec_Ptr_t * vMinCut )
     Aig_ManIncrementTravId(p);
     Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Aig_ObjIsPo(pObj) && !Aig_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsCo(pObj) && !Aig_ObjIsNode(pObj) )
             continue;
         if ( Aig_ObjIsTravIdCurrent(p, pObj) || Aig_ObjIsTravIdPrevious(p, pObj) )
             continue;
@@ -708,7 +708,7 @@ int Llb_ManFlowVerifyCut_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
     // visit the node
     if ( Aig_ObjIsConst1(pObj) )
         return 1;
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return 0;
     // explore the fanins
     assert( Aig_ObjIsNode(pObj) );
@@ -930,7 +930,7 @@ void Llb_ManFlowSetMarkA_rec( Aig_Obj_t * pObj )
     if ( pObj->fMarkA )
         return;
     pObj->fMarkA = 1;
-    if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
+    if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
         return;
     assert( Aig_ObjIsNode(pObj) );
     Llb_ManFlowSetMarkA_rec( Aig_ObjFanin0(pObj) );
diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c
index 678a6fff..38d9b8ae 100644
--- a/src/proof/llb/llb3Nonlin.c
+++ b/src/proof/llb/llb3Nonlin.c
@@ -705,17 +705,17 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t *  p
     p->pPars = pPars;
     p->dd    = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     p->ddG   = Cudd_Init( Aig_ManRegNum(pAig),    0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    p->ddR   = Cudd_Init( Aig_ManPiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    p->ddR   = Cudd_Init( Aig_ManCiNum(pAig),     0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
     Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
     Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
     p->vRings = Vec_PtrAlloc( 100 );
     // create leaves
-    p->vLeaves = Vec_PtrAlloc( Aig_ManPiNum(pAig) );
+    p->vLeaves = Vec_PtrAlloc( Aig_ManCiNum(pAig) );
     Aig_ManForEachCi( pAig, pObj, i )
         Vec_PtrPush( p->vLeaves, pObj );
     // create roots
-    p->vRoots = Vec_PtrAlloc( Aig_ManPoNum(pAig) );
+    p->vRoots = Vec_PtrAlloc( Aig_ManCoNum(pAig) );
     Saig_ManForEachLi( pAig, pObj, i )
         Vec_PtrPush( p->vRoots, pObj );
     // variables to quantify
diff --git a/src/proof/llb/llb4Cex.c b/src/proof/llb/llb4Cex.c
index 69ba6ab1..b5bdb36e 100644
--- a/src/proof/llb/llb4Cex.c
+++ b/src/proof/llb/llb4Cex.c
@@ -63,7 +63,7 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int
 */
     // derive SAT solver
     nRegs = Aig_ManRegNum(pAig); pAig->nRegs = 0;
-    pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) );
+    pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
     pAig->nRegs = nRegs;
 //    Cnf_DataTranformPolarity( pCnf, 0 );
     // convert into SAT solver
@@ -249,11 +249,11 @@ Vec_Ptr_t * Llb4_Nonlin4VerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
     }
 */
     assert( iBit == p->nBits );
-//    if ( Aig_ManPo(pAig, p->iPo)->fMarkB == 0 )
+//    if ( Aig_ManCo(pAig, p->iPo)->fMarkB == 0 )
 //        Vec_PtrFreeP( &vStates );
     for ( i = Saig_ManPoNum(pAig) - 1; i >= 0; i-- )
     {
-        if ( Aig_ManPo(pAig, i)->fMarkB )
+        if ( Aig_ManCo(pAig, i)->fMarkB )
         {
             p->iPo = i;
             break;
diff --git a/src/proof/llb/llb4Cluster.c b/src/proof/llb/llb4Cluster.c
index c151a618..7e325597 100644
--- a/src/proof/llb/llb4Cluster.c
+++ b/src/proof/llb/llb4Cluster.c
@@ -49,7 +49,7 @@ void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v
         return;
     Aig_ObjSetTravIdCurrent( pAig, pObj );
     assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
         return;
@@ -152,11 +152,11 @@ DdNode * Llb_Nonlin4FindPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_In
     DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
     if ( Aig_ObjIsConst1(pObj) )
         return Cudd_ReadOne(dd); 
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
     if ( pObj->pData )
         return (DdNode *)pObj->pData;
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
         bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 );  Cudd_Ref( bPart );
diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c
index 31f94acf..af8dad75 100644
--- a/src/proof/llb/llb4Nonlin.c
+++ b/src/proof/llb/llb4Nonlin.c
@@ -84,7 +84,7 @@ DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vO
     Aig_ManForEachCi( pAig, pObj, i )
         pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
     // compute internal nodes
-    vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vPos), Saig_ManPoNum(pAig) );
+    vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vCos), Saig_ManPoNum(pAig) );
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         if ( !Aig_ObjIsNode(pObj) )
@@ -273,7 +273,7 @@ void Llb_Nonlin4CreateOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t *
         return;
     Aig_ObjSetTravIdCurrent( pAig, pObj );
     assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
 //        if ( Saig_ObjIsLo(pAig, pObj) )
 //            Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ );
@@ -371,7 +371,7 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
 //                Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ );
             Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
         }
-    assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
+    assert( Counter <= Aig_ManCiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
     Aig_ManCleanMarkA( pAig );
     Vec_IntFreeP( &vNodes );
     return vOrder;
diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c
index 292fb176..6b223ab9 100644
--- a/src/proof/llb/llb4Sweep.c
+++ b/src/proof/llb/llb4Sweep.c
@@ -49,7 +49,7 @@ void Llb_Nonlin4SweepOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t *
         return;
     Aig_ObjSetTravIdCurrent( pAig, pObj );
     assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
         return;
@@ -102,7 +102,7 @@ Vec_Int_t * Llb_Nonlin4SweepOrder( Aig_Man_t * pAig, int * pCounter, int fSaveAl
             Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
 //    assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes
     if ( pCounter )
-        *pCounter = Counter - Aig_ManPiNum(pAig) - Aig_ManPoNum(pAig);
+        *pCounter = Counter - Aig_ManCiNum(pAig) - Aig_ManCoNum(pAig);
     return vOrder;
 }
 
@@ -211,11 +211,11 @@ DdNode * Llb_Nonlin4SweepPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_I
     DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
     if ( Aig_ObjIsConst1(pObj) )
         return Cudd_ReadOne(dd); 
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
     if ( pObj->pData )
         return (DdNode *)pObj->pData;
-    if ( Aig_ObjIsPo(pObj) )
+    if ( Aig_ObjIsCo(pObj) )
     {
         bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
         bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 );  Cudd_Ref( bPart );
@@ -535,9 +535,9 @@ void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdMana
     assert( Counter == nCutPoints );
     Aig_ManCleanMarkA( pAig );
     // compute the BAD states
-    ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManPiNum(pAig) + Aig_ManPoNum(pAig) );
+    ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig) );
     // compute the clusters
-    ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManPiNum(pAig) + Aig_ManPoNum(pAig), &vGroups, nClusterMax, fVerbose );
+    ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig), &vGroups, nClusterMax, fVerbose );
     // transfer the result from the Bad manager
 //printf( "Bad before = %d.\n", Cudd_DagSize(ddBad->bFunc) );
     ddWork->bFunc = Cudd_bddTransfer( ddBad, ddWork, ddBad->bFunc );   Cudd_Ref( ddWork->bFunc );