diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-09 19:32:44 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-09 19:32:44 -0800 |
commit | 2c8f1a67ec9295450a72fc27cbb3ed1177945734 (patch) | |
tree | 5386dd978ded397a75b6a9c06fe46b3789468beb /src/sat/cnf | |
parent | 34078de8d6414bb832d26c33578a1fcdfa21b750 (diff) | |
download | abc-2c8f1a67ec9295450a72fc27cbb3ed1177945734.tar.gz abc-2c8f1a67ec9295450a72fc27cbb3ed1177945734.tar.bz2 abc-2c8f1a67ec9295450a72fc27cbb3ed1177945734.zip |
Renamed Aig_ManForEachPi/Po to be ...Ci/Co and Aig_ObjCreatePi/Po to be ...Ci/Co.
Diffstat (limited to 'src/sat/cnf')
-rw-r--r-- | src/sat/cnf/cnfFast.c | 12 | ||||
-rw-r--r-- | src/sat/cnf/cnfMan.c | 8 | ||||
-rw-r--r-- | src/sat/cnf/cnfMap.c | 2 | ||||
-rw-r--r-- | src/sat/cnf/cnfUtil.c | 8 | ||||
-rw-r--r-- | src/sat/cnf/cnfWrite.c | 26 |
5 files changed, 28 insertions, 28 deletions
diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c index 840c923e..ea831844 100644 --- a/src/sat/cnf/cnfFast.c +++ b/src/sat/cnf/cnfFast.c @@ -306,11 +306,11 @@ void Cnf_DeriveFastMark( Aig_Man_t * p ) vSupps = Vec_IntStart( Aig_ManObjNumMax(p) ); // mark CIs - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) pObj->fMarkA = 1; // mark CO drivers - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) Aig_ObjFanin0(pObj)->fMarkA = 1; // mark MUX/XOR nodes @@ -403,7 +403,7 @@ void Cnf_DeriveFastMark( Aig_Man_t * p ) // check CO drivers Counter = 0; - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) Counter += !Aig_ObjFanin0(pObj)->fMarkA; if ( Counter ) printf( "PO-driver rule is violated %d times.\n", Counter ); @@ -562,7 +562,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) if ( Aig_ManRegNum(p) == 0 ) { assert( nOutputs == Aig_ManPoNum(p) ); - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ ); } else @@ -577,7 +577,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) if ( pObj->fMarkA ) Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ ); // assign variables to the PIs and constant node - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) Vec_IntWriteEntry( vMap, Aig_ObjId(pObj), nVars++ ); Vec_IntWriteEntry( vMap, Aig_ObjId(Aig_ManConst1(p)), nVars++ ); @@ -605,7 +605,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) Vec_IntFree( vTemp ); // create clauses for the outputs - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { DriLit = Cnf_ObjGetLit( vMap, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj) ); if ( i < Aig_ManPoNum(p) - nOutputs ) diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index a670a69d..1a28bd2a 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -107,7 +107,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) Aig_Obj_t * pObj; int i; vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); return vCiIds; } @@ -541,7 +541,7 @@ int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf ) Aig_Obj_t * pObj; int i, * pLits; pLits = ABC_ALLOC( int, Aig_ManPoNum(pCnf->pMan) ); - Aig_ManForEachPo( pCnf->pMan, pObj, i ) + 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) ) ) { @@ -569,7 +569,7 @@ int Cnf_DataWriteOrClause2( void * p, Cnf_Dat_t * pCnf ) Aig_Obj_t * pObj; int i, * pLits; pLits = ABC_ALLOC( int, Aig_ManPoNum(pCnf->pMan) ); - Aig_ManForEachPo( pCnf->pMan, pObj, i ) + 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) ) ) { @@ -596,7 +596,7 @@ int Cnf_DataWriteAndClauses( void * p, Cnf_Dat_t * pCnf ) sat_solver * pSat = (sat_solver *)p; Aig_Obj_t * pObj; int i, Lit; - Aig_ManForEachPo( pCnf->pMan, pObj, i ) + Aig_ManForEachCo( pCnf->pMan, pObj, i ) { Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) ) diff --git a/src/sat/cnf/cnfMap.c b/src/sat/cnf/cnfMap.c index 8907485e..a6345471 100644 --- a/src/sat/cnf/cnfMap.c +++ b/src/sat/cnf/cnfMap.c @@ -144,7 +144,7 @@ void Cnf_DeriveMapping( Cnf_Man_t * p ) /* // compute the area of mapping AreaFlow = 0; - Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ManForEachCo( p->pManAig, pObj, i ) AreaFlow += Dar_ObjBestCut(Aig_ObjFanin0(pObj))->uSign / 100 / Aig_ObjFanin0(pObj)->nRefs; printf( "Area of the network = %d.\n", AreaFlow ); */ diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index 236b6bfa..dd495d89 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -99,7 +99,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ) vMapped = Vec_PtrAlloc( 1000 ); // collect nodes reachable from POs in the DFS order through the best cuts p->aArea = 0; - Aig_ManForEachPo( p->pManAig, pObj, i ) + 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 ); return vMapped; @@ -179,7 +179,7 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ) vMapped = Vec_PtrAlloc( 1000 ); // collect nodes reachable from POs in the DFS order through the best cuts p->aArea = 0; - Aig_ManForEachPo( p->pManAig, pObj, i ) + 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 ); return vMapped; @@ -202,7 +202,7 @@ Vec_Int_t * Cnf_DataCollectCiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) Aig_Obj_t * pObj; int i; vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); return vCiIds; } @@ -224,7 +224,7 @@ Vec_Int_t * Cnf_DataCollectCoSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ) Aig_Obj_t * pObj; int i; vCoIds = Vec_IntAlloc( Aig_ManPoNum(p) ); - Aig_ManForEachPo( p, pObj, i ) + 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 54c28967..42809299 100644 --- a/src/sat/cnf/cnfWrite.c +++ b/src/sat/cnf/cnfWrite.c @@ -268,7 +268,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) ); - Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ManForEachCo( p->pManAig, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; } else @@ -282,7 +282,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; // assign variables to the PIs and constant node - Aig_ManForEachPi( p->pManAig, pObj, i ) + Aig_ManForEachCi( p->pManAig, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++; pCnf->nVars = Number; @@ -297,7 +297,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) ); - Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ManForEachCo( p->pManAig, pObj, i ) pCnf->pVarNums[pObj->Id] = Number--; } else @@ -311,7 +311,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i ) pCnf->pVarNums[pObj->Id] = Number--; // assign variables to the PIs and constant node - Aig_ManForEachPi( p->pManAig, pObj, i ) + Aig_ManForEachCi( p->pManAig, pObj, i ) pCnf->pVarNums[pObj->Id] = Number--; pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number--; assert( Number >= 0 ); @@ -374,7 +374,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) *pLits++ = 2 * OutVar; // write the output literals - Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ManForEachCo( p->pManAig, pObj, i ) { OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; if ( i < Aig_ManPoNum(p->pManAig) - nOutputs ) @@ -477,7 +477,7 @@ Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) pCnf->nVars = Aig_ManObjNumMax(p->pManAig); // clear the PI counters - Aig_ManForEachPi( p->pManAig, pObj, i ) + Aig_ManForEachCi( p->pManAig, pObj, i ) pCnf->pObj2Count[pObj->Id] = 0; // assign the clauses @@ -537,7 +537,7 @@ Cnf_Dat_t * Cnf_ManWriteCnfOther( Cnf_Man_t * p, Vec_Ptr_t * vMapped ) Vec_IntFree( vSopTemp ); // write the output literals - Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ManForEachCo( p->pManAig, pObj, i ) { // remember the starting clause pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses; @@ -617,14 +617,14 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) // assert( nOutputs == Aig_ManRegNum(p) ); // Aig_ManForEachLiSeq( p, pObj, i ) // pCnf->pVarNums[pObj->Id] = Number++; - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; } // assign variables to the internal nodes Aig_ManForEachNode( p, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; // assign variables to the PIs and constant node - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++; pCnf->nVars = Number; @@ -665,7 +665,7 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) *pLits++ = 2 * OutVar; // write the output literals - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; if ( i < Aig_ManPoNum(p) - nOutputs ) @@ -734,13 +734,13 @@ Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p ) pCnf->pVarNums[i] = -1; // assign variables to the last (nOutputs) POs Number = 1; - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; // assign variables to the internal nodes Aig_ManForEachNode( p, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; // assign variables to the PIs and constant node - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) pCnf->pVarNums[pObj->Id] = Number++; pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++; pCnf->nVars = Number; @@ -774,7 +774,7 @@ Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p ) *pLits++ = 2 * OutVar; // write the output literals - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ]; PoVar = pCnf->pVarNums[ pObj->Id ]; |