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

4 files changed, 30 insertions, 30 deletions

diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c
index ea831844..492ddb61 100644
--- a/src/sat/cnf/cnfFast.c
+++ b/src/sat/cnf/cnfFast.c
@@ -367,12 +367,12 @@ void Cnf_DeriveFastMark( Aig_Man_t * p )
 //            if ( pObj0 == pObj1 )
 //                continue;
             nFans = 1 + (pObj0 == pObj1);
-            if ( !pObj0->fMarkB && !Aig_ObjIsPi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 )
+            if ( !pObj0->fMarkB && !Aig_ObjIsCi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 )
             {
                 pObj0->fMarkA = 0;
                 continue;
             }
-            if ( !pObj1->fMarkB && !Aig_ObjIsPi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 )
+            if ( !pObj1->fMarkB && !Aig_ObjIsCi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 )
             {
                 pObj1->fMarkA = 0;
                 continue;
@@ -388,7 +388,7 @@ void Cnf_DeriveFastMark( Aig_Man_t * p )
         {
             pTemp = Aig_Regular(pTemp);
             assert( pTemp->fMarkA );
-            if ( pTemp->fMarkB || Aig_ObjIsPi(pTemp) || Aig_ObjRefs(pTemp) > 1 )
+            if ( pTemp->fMarkB || Aig_ObjIsCi(pTemp) || Aig_ObjRefs(pTemp) > 1 )
                 continue;
             assert( Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 0 );
             if ( Vec_PtrSize(vLeaves) - 1 + Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 6 )
@@ -561,7 +561,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
     {
         if ( Aig_ManRegNum(p) == 0 )
         {
-            assert( nOutputs == Aig_ManPoNum(p) );
+            assert( nOutputs == Aig_ManCoNum(p) );
             Aig_ManForEachCo( p, pObj, i )
                 Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ );
         }
@@ -608,7 +608,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs )
     Aig_ManForEachCo( p, pObj, i )
     {
         DriLit = Cnf_ObjGetLit( vMap, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj) );
-        if ( i < Aig_ManPoNum(p) - nOutputs )
+        if ( i < Aig_ManCoNum(p) - nOutputs )
         {
             Vec_IntPush( vClas, Vec_IntSize(vLits) );
             Vec_IntPush( vLits, DriLit );
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index 1a28bd2a..a4081f86 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -106,7 +106,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
     Vec_Int_t * vCiIds;
     Aig_Obj_t * pObj;
     int i;
-    vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
+    vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
     Aig_ManForEachCi( p, pObj, i )
         Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
     return vCiIds;
@@ -540,10 +540,10 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
     sat_solver * pSat = (sat_solver *)p;
     Aig_Obj_t * pObj;
     int i, * pLits;
-    pLits = ABC_ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
+    pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) );
     Aig_ManForEachCo( pCnf->pMan, pObj, i )
         pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-    if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
+    if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) )
     {
         ABC_FREE( pLits );
         return 0;
@@ -568,10 +568,10 @@ int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf )
     sat_solver2 * pSat = (sat_solver2 *)p;
     Aig_Obj_t * pObj;
     int i, * pLits;
-    pLits = ABC_ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
+    pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) );
     Aig_ManForEachCo( pCnf->pMan, pObj, i )
         pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-    if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
+    if ( !sat_solver2_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) )
     {
         ABC_FREE( pLits );
         return 0;
@@ -625,7 +625,7 @@ void Cnf_DataTranformPolarity( Cnf_Dat_t * pCnf, int fTransformPos )
     pVarToPol = ABC_CALLOC( int, pCnf->nVars );
     Aig_ManForEachObj( pCnf->pMan, pObj, i )
     {
-        if ( !fTransformPos && Aig_ObjIsPo(pObj) )
+        if ( !fTransformPos && Aig_ObjIsCo(pObj) )
             continue;
         if ( pCnf->pVarNums[pObj->Id] >= 0 )
             pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase;
diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c
index dd495d89..e3828863 100644
--- a/src/sat/cnf/cnfUtil.c
+++ b/src/sat/cnf/cnfUtil.c
@@ -47,7 +47,7 @@ int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
     Aig_Obj_t * pLeaf;
     Dar_Cut_t * pCutBest;
     int aArea, i;
-    if ( pObj->nRefs++ || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
+    if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
         return 0;
     assert( Aig_ObjIsAnd(pObj) );
     // collect the node first to derive pre-order
@@ -101,7 +101,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
     p->aArea = 0;
     Aig_ManForEachCo( p->pManAig, pObj, i )
         p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
-//    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
+//    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
     return vMapped;
 }
 
@@ -121,7 +121,7 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped
     Aig_Obj_t * pLeaf;
     Cnf_Cut_t * pCutBest;
     int aArea, i;
-    if ( pObj->nRefs++ || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
+    if ( pObj->nRefs++ || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) )
         return 0;
     assert( Aig_ObjIsAnd(pObj) );
     assert( pObj->pData != NULL );
@@ -181,7 +181,7 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
     p->aArea = 0;
     Aig_ManForEachCo( p->pManAig, pObj, i )
         p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
-//    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
+//    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
     return vMapped;
 }
 
@@ -201,7 +201,7 @@ Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
     Vec_Int_t * vCiIds;
     Aig_Obj_t * pObj;
     int i;
-    vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
+    vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
     Aig_ManForEachCi( p, pObj, i )
         Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
     return vCiIds;
@@ -223,7 +223,7 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
     Vec_Int_t * vCoIds;
     Aig_Obj_t * pObj;
     int i;
-    vCoIds = Vec_IntAlloc( Aig_ManPoNum(p) );
+    vCoIds = Vec_IntAlloc( Aig_ManCoNum(p) );
     Aig_ManForEachCo( p, pObj, i )
         Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] );
     return vCoIds;
diff --git a/src/sat/cnf/cnfWrite.c b/src/sat/cnf/cnfWrite.c
index 42809299..08407e39 100644
--- a/src/sat/cnf/cnfWrite.c
+++ b/src/sat/cnf/cnfWrite.c
@@ -208,8 +208,8 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     int i, k, nLiterals, nClauses, Cube, Number;
 
     // count the number of literals and clauses
-    nLiterals = 1 + Aig_ManPoNum( p->pManAig ) + 3 * nOutputs;
-    nClauses = 1 + Aig_ManPoNum( p->pManAig ) + nOutputs;
+    nLiterals = 1 + Aig_ManCoNum( p->pManAig ) + 3 * nOutputs;
+    nClauses = 1 + Aig_ManCoNum( p->pManAig ) + nOutputs;
     Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
     {
         assert( Aig_ObjIsNode(pObj) );
@@ -241,7 +241,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
             nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
             nClauses += Vec_IntSize(pCut->vIsop[0]);
         }
-//printf( "%d ", nClauses-(1 + Aig_ManPoNum( p->pManAig )) );
+//printf( "%d ", nClauses-(1 + Aig_ManCoNum( p->pManAig )) );
     }
 //printf( "\n" );
 
@@ -267,7 +267,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
         {
             if ( Aig_ManRegNum(p->pManAig) == 0 )
             {
-                assert( nOutputs == Aig_ManPoNum(p->pManAig) );
+                assert( nOutputs == Aig_ManCoNum(p->pManAig) );
                 Aig_ManForEachCo( p->pManAig, pObj, i )
                     pCnf->pVarNums[pObj->Id] = Number++;
             }
@@ -296,7 +296,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
         {
             if ( Aig_ManRegNum(p->pManAig) == 0 )
             {
-                assert( nOutputs == Aig_ManPoNum(p->pManAig) );
+                assert( nOutputs == Aig_ManCoNum(p->pManAig) );
                 Aig_ManForEachCo( p->pManAig, pObj, i )
                     pCnf->pVarNums[pObj->Id] = Number--;
             }
@@ -377,7 +377,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
     Aig_ManForEachCo( p->pManAig, pObj, i )
     {
         OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
-        if ( i < Aig_ManPoNum(p->pManAig) - nOutputs )
+        if ( i < Aig_ManCoNum(p->pManAig) - nOutputs )
         {
             *pClas++ = pLits;
             *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
@@ -427,8 +427,8 @@ Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
     int i, k, nLiterals, nClauses, Cube;
 
     // count the number of literals and clauses
-    nLiterals = 1 + 4 * Aig_ManPoNum( p->pManAig );
-    nClauses  = 1 + 2 * Aig_ManPoNum( p->pManAig );
+    nLiterals = 1 + 4 * Aig_ManCoNum( p->pManAig );
+    nClauses  = 1 + 2 * Aig_ManCoNum( p->pManAig );
     Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
     {
         assert( Aig_ObjIsNode(pObj) );
@@ -592,8 +592,8 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
     int i, nLiterals, nClauses, Number;
 
     // count the number of literals and clauses
-    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + 3 * nOutputs;
-    nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + nOutputs;
+    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + 3 * nOutputs;
+    nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + nOutputs;
 
     // allocate CNF
     pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
@@ -668,7 +668,7 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
     Aig_ManForEachCo( p, pObj, i )
     {
         OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
-        if ( i < Aig_ManPoNum(p) - nOutputs )
+        if ( i < Aig_ManCoNum(p) - nOutputs )
         {
             *pClas++ = pLits;
             *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
@@ -714,8 +714,8 @@ Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p )
     int i, nLiterals, nClauses, Number;
 
     // count the number of literals and clauses
-    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManPoNum(p);
-    nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManPoNum(p);
+    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManCoNum(p);
+    nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManCoNum(p);
 
     // allocate CNF
     pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );