5 files changed, 13 insertions, 13 deletions
diff --git a/src/proof/dch/dchAig.c b/src/proof/dch/dchAig.c
index 59828443..1b6f1539 100644
--- a/src/proof/dch/dchAig.c
+++ b/src/proof/dch/dchAig.c
@@ -73,8 +73,8 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
     pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
     Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i )
     {
-        assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
-        assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
+        assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pAig2) );
+        assert( Aig_ManCoNum(pAig) == Aig_ManCoNum(pAig2) );
         nNodes += Aig_ManNodeNum(pAig2);
         Aig_ManCleanData( pAig2 );
     }
@@ -87,14 +87,14 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
     {
         pObjPi = Aig_ObjCreateCi( pAigTotal );
         Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
-            Aig_ManPi( pAig2, i )->pData = pObjPi;
+            Aig_ManCi( pAig2, i )->pData = pObjPi;
     }
     // construct the AIG in the order of POs
     Aig_ManForEachCo( pAig, pObj, i )
     {
         Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
         {
-            pObjPo = Aig_ManPo( pAig2, i );
+            pObjPo = Aig_ManCo( pAig2, i );
             Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
         }
         Aig_ObjCreateCo( pAigTotal, Aig_ObjChild0Copy(pObj) );
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 1de11509..7a763d84 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -117,7 +117,7 @@ int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
     // check the trivial cases
     if ( pObj == NULL )
         return 0;
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
         return 0;
     if ( pObj->fMarkA )
         return 1;
@@ -289,7 +289,7 @@ int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose )
 {
     Aig_Obj_t * pFanin;
     int fAcyclic;
-    if ( Aig_ObjIsPi(pNode) || Aig_ObjIsConst1(pNode) )
+    if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
         return 1;
     assert( Aig_ObjIsNode(pNode) );
     // make sure the node is not visited
diff --git a/src/proof/dch/dchClass.c b/src/proof/dch/dchClass.c
index 24476309..1f974236 100644
--- a/src/proof/dch/dchClass.c
+++ b/src/proof/dch/dchClass.c
@@ -350,12 +350,12 @@ void Dch_ClassesPrepare( Dch_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 )
@@ -400,7 +400,7 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
     nEntries2 = 0;
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
             continue;
         nNodes = p->pClassSizes[pObj->Id];
         // skip the nodes that are not representatives of non-trivial classes
diff --git a/src/proof/dch/dchCnf.c b/src/proof/dch/dchCnf.c
index 4175a123..b65b096c 100644
--- a/src/proof/dch/dchCnf.c
+++ b/src/proof/dch/dchCnf.c
@@ -217,7 +217,7 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
 void Dch_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)) )
     {
@@ -243,7 +243,7 @@ void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
 void Dch_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 );
     Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
 }
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
index 808e754a..6f69b47e 100644
--- a/src/proof/dch/dchSimSat.c
+++ b/src/proof/dch/dchSimSat.c
@@ -113,7 +113,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
     if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         Aig_Obj_t * pObjFraig;
         int nVarNum;
@@ -151,7 +151,7 @@ void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
     if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
-    if ( Aig_ObjIsPi(pObj) )
+    if ( Aig_ObjIsCi(pObj) )
     {
         // set random value
         pObj->fMarkB = Aig_ManRandom(0) & 1;