summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bsat/satInterA.c4
-rw-r--r--src/sat/bsat/satInterB.c4
-rw-r--r--src/sat/bsat/satProof.c6
-rw-r--r--src/sat/cnf/cnfFast.c12
-rw-r--r--src/sat/cnf/cnfMan.c8
-rw-r--r--src/sat/cnf/cnfMap.c2
-rw-r--r--src/sat/cnf/cnfUtil.c8
-rw-r--r--src/sat/cnf/cnfWrite.c26
8 files changed, 35 insertions, 35 deletions
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 01a5ca31..4057ce7e 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -1017,7 +1017,7 @@ p->timeTotal += clock() - clkTotal;
}
pObj = *Inta_ManAigRead( p, p->pCnf->pTail );
- Aig_ObjCreatePo( pRes, pObj );
+ Aig_ObjCreateCo( pRes, pObj );
Aig_ManCleanup( pRes );
p->pAig = NULL;
@@ -1066,7 +1066,7 @@ Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fCla
}
pMiter = Aig_And( p, pMiter, pSum );
}
- Aig_ObjCreatePo( p, pMiter );
+ Aig_ObjCreateCo( p, pMiter );
return p;
}
diff --git a/src/sat/bsat/satInterB.c b/src/sat/bsat/satInterB.c
index 5d348f62..a9b18fd5 100644
--- a/src/sat/bsat/satInterB.c
+++ b/src/sat/bsat/satInterB.c
@@ -1053,7 +1053,7 @@ p->timeTotal += clock() - clkTotal;
}
pObj = *Intb_ManAigRead( p, p->pCnf->pTail );
- Aig_ObjCreatePo( pRes, pObj );
+ Aig_ObjCreateCo( pRes, pObj );
Aig_ManCleanup( pRes );
p->pAig = NULL;
@@ -1102,7 +1102,7 @@ Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fCla
}
pMiter = Aig_And( p, pMiter, pSum );
}
- Aig_ObjCreatePo( p, pMiter );
+ Aig_ObjCreateCo( p, pMiter );
return p;
}
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index d61dea4f..81a6a67a 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -695,7 +695,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
pAig = Aig_ManStart( 10000 );
pAig->pName = Abc_UtilStrsav( "interpol" );
for ( i = 0; i < Vec_IntSize(vGlobVars); i++ )
- Aig_ObjCreatePi( pAig );
+ Aig_ObjCreateCi( pAig );
// copy the numbers out and derive interpol for clause
vCoreNums = Vec_IntAlloc( Vec_IntSize(vCore) );
@@ -736,7 +736,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars )
}
// save the result
// assert( Proof_NodeHandle(vProof, pNode) == hRoot );
- Aig_ObjCreatePo( pAig, pObj );
+ Aig_ObjCreateCo( pAig, pObj );
Aig_ManCleanup( pAig );
// move the results back
@@ -844,7 +844,7 @@ word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars )
}
// save the result
// assert( Proof_NodeHandle(vProof, pNode) == hRoot );
-// Aig_ObjCreatePo( pAig, pObj );
+// Aig_ObjCreateCo( pAig, pObj );
// Aig_ManCleanup( pAig );
// move the results back
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 ];
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 20:36:09 +0000