summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/pdr')
-rw-r--r--src/proof/pdr/pdrClass.c2
-rw-r--r--src/proof/pdr/pdrCnf.c6
-rw-r--r--src/proof/pdr/pdrSat.c6
-rw-r--r--src/proof/pdr/pdrTsim.c14
-rw-r--r--src/proof/pdr/pdrUtil.c2
5 files changed, 15 insertions, 15 deletions
diff --git a/src/proof/pdr/pdrClass.c b/src/proof/pdr/pdrClass.c
index cbe5e1c2..5dd4c4a9 100644
--- a/src/proof/pdr/pdrClass.c
+++ b/src/proof/pdr/pdrClass.c
@@ -202,7 +202,7 @@ void Pdr_ManEquivClasses( Aig_Man_t * pAig )
// report the result
Abc_Print( 1, "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n",
f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap),
- Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
+ Aig_ObjChild0(Aig_ManCo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
// recreate the map
Pdr_ManPrintMap( vMap );
Vec_IntFree( vMap );
diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c
index fddd292b..fcad15e0 100644
--- a/src/proof/pdr/pdrCnf.c
+++ b/src/proof/pdr/pdrCnf.c
@@ -114,7 +114,7 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
if ( nVarCount == Vec_IntSize(vVar2Ids) )
return iVarThis;
assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
- if ( Aig_ObjIsPi(pObj) )
+ if ( Aig_ObjIsCi(pObj) )
return iVarThis;
nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
@@ -269,8 +269,8 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p,
if ( p->pCnf1 == NULL )
{
int nRegs = p->pAig->nRegs;
- p->pAig->nRegs = Aig_ManPoNum(p->pAig);
- p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManPoNum(p->pAig) );
+ p->pAig->nRegs = Aig_ManCoNum(p->pAig);
+ p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManCoNum(p->pAig) );
p->pAig->nRegs = nRegs;
assert( p->vVar2Reg == NULL );
p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index c191654a..de661905 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -55,7 +55,7 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
Vec_VecExpand( p->vClauses, k );
Vec_IntPush( p->vActVars, 0 );
// add property cone
- Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
+ Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
return pSat;
}
@@ -175,7 +175,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
sat_solver * pSat;
int Lit, RetValue;
pSat = Pdr_ManSolver(p, k);
- Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
+ Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );
sat_solver_compress( pSat );
@@ -278,7 +278,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
if ( pCube == NULL ) // solve the property
{
clk = clock();
- Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
+ Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
if ( RetValue == l_Undef )
return -1;
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 428c20c7..0547c308 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -81,13 +81,13 @@ void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCi
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
return;
Aig_ObjSetTravIdCurrent(pAig, pObj);
- if ( Aig_ObjIsPi(pObj) )
+ if ( Aig_ObjIsCi(pObj) )
{
Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
return;
}
Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
- if ( Aig_ObjIsPo(pObj) )
+ if ( Aig_ObjIsCo(pObj) )
return;
Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
Vec_IntPush( vNodes, Aig_ObjId(pObj) );
@@ -133,7 +133,7 @@ int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
if ( Aig_ObjFaninC0(pObj) )
Value0 = Pdr_ManSimInfoNot( Value0 );
- if ( Aig_ObjIsPo(pObj) )
+ if ( Aig_ObjIsCo(pObj) )
{
Pdr_ManSimInfoSet( pAig, pObj, Value0 );
return Value0;
@@ -228,7 +228,7 @@ int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec
assert( Value2 == PDR_UND );
Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
Vec_IntPush( vUndo, Value );
- if ( Aig_ObjIsPo(pFanout) )
+ if ( Aig_ObjIsCo(pFanout) )
return 0;
assert( Aig_ObjIsNode(pFanout) );
Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
@@ -318,8 +318,8 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
{
Aig_Obj_t * pObj;
int i;
- char * pBuff = ABC_ALLOC( char, Aig_ManPiNum(pAig)+1 );
- for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
+ char * pBuff = ABC_ALLOC( char, Aig_ManCiNum(pAig)+1 );
+ for ( i = 0; i < Aig_ManCiNum(pAig); i++ )
pBuff[i] = '-';
pBuff[i] = 0;
Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
@@ -368,7 +368,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
// collect CO objects
Vec_IntClear( vCoObjs );
if ( pCube == NULL ) // the target is the property output
- Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
+ Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
else // the target is the cube
{
for ( i = 0; i < pCube->nLits; i++ )
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 97261a7f..9a2cffb2 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -613,7 +613,7 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd
return ((int)pNode->fMarkA == Value);
Aig_ObjSetTravIdCurrent(pAig, pNode);
pNode->fMarkA = Value;
- if ( Aig_ObjIsPi(pNode) )
+ if ( Aig_ObjIsCi(pNode) )
{
// if ( vSuppLits )
// Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 21:59:14 +0000