Renamed Aig_ObjPioNum to be Aig_ObjCioId.

3 files changed, 10 insertions, 10 deletions

diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
index fcad15e0..2b039c01 100644
--- a/src/proof/pdr/pdrCnf.c
+++ b/src/proof/pdr/pdrCnf.c
@@ -202,7 +202,7 @@ static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar )
         return -1;
     pObj = Aig_ManObj( p->pAig, ObjId );
     if ( Saig_ObjIsLi( p->pAig, pObj ) )
-        return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig);
+        return Aig_ObjCioId(pObj)-Saig_ManPoNum(p->pAig);
     assert( 0 ); // should be called for register inputs only
     return -1;
 }
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 0547c308..cf4756d1 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -289,14 +289,14 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi
     {
         if ( Saig_ObjIsPi(pAig, pObj) )
         {
-            Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
+            Lit = toLitCond( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
             Vec_IntPush( vPiLits, Lit );
             continue;
         }
         assert( Saig_ObjIsLo(pAig, pObj) );
         if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
             continue;
-        Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
+        Lit = toLitCond( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
         Vec_IntPush( vRes, Lit );
     }
     if ( Vec_IntSize(vRes) == 0 )
@@ -323,10 +323,10 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
         pBuff[i] = '-';
     pBuff[i] = 0;
     Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
-        pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
+        pBuff[Aig_ObjCioId(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
     if ( vCi2Rem )
     Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
-        pBuff[Aig_ObjPioNum(pObj)] = 'x';
+        pBuff[Aig_ObjCioId(pObj)] = 'x';
     Abc_Print( 1, "%s\n", pBuff );
     ABC_FREE( pBuff );
 }
@@ -406,7 +406,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
     {
         if ( !Saig_ObjIsLo( p->pAig, pObj ) )
             continue;
-        Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig);
+        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
         if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
             continue;
         Vec_IntClear( vUndo );
@@ -420,7 +420,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
     {
         if ( !Saig_ObjIsLo( p->pAig, pObj ) )
             continue;
-        Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig);
+        Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
         if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
             continue;
         Vec_IntClear( vUndo );
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 9a2cffb2..a47bc9f0 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -616,11 +616,11 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd
     if ( Aig_ObjIsCi(pNode) )
     {
 //        if ( vSuppLits )
-//            Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
+//            Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) );
         if ( Saig_ObjIsLo(pAig, pNode) )
         {
-//            pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value );
-            pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value );
+//            pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), !Value );
+            pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), Value );
             pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63));
         }
         return 1;