summaryrefslogtreecommitdiffstats
path: root/src/proof/dch
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/dch')
-rw-r--r--src/proof/dch/dchAig.c8
-rw-r--r--src/proof/dch/dchChoice.c4
-rw-r--r--src/proof/dch/dchClass.c6
-rw-r--r--src/proof/dch/dchCnf.c4
-rw-r--r--src/proof/dch/dchSimSat.c4
5 files changed, 13 insertions, 13 deletions
diff --git a/src/proof/dch/dchAig.c b/src/proof/dch/dchAig.c
index 59828443..1b6f1539 100644
--- a/src/proof/dch/dchAig.c
+++ b/src/proof/dch/dchAig.c
@@ -73,8 +73,8 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i )
{
- assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
- assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
+ assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pAig2) );
+ assert( Aig_ManCoNum(pAig) == Aig_ManCoNum(pAig2) );
nNodes += Aig_ManNodeNum(pAig2);
Aig_ManCleanData( pAig2 );
}
@@ -87,14 +87,14 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
{
pObjPi = Aig_ObjCreateCi( pAigTotal );
Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
- Aig_ManPi( pAig2, i )->pData = pObjPi;
+ Aig_ManCi( pAig2, i )->pData = pObjPi;
}
// construct the AIG in the order of POs
Aig_ManForEachCo( pAig, pObj, i )
{
Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k )
{
- pObjPo = Aig_ManPo( pAig2, i );
+ pObjPo = Aig_ManCo( pAig2, i );
Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) );
}
Aig_ObjCreateCo( pAigTotal, Aig_ObjChild0Copy(pObj) );
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 1de11509..7a763d84 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -117,7 +117,7 @@ int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
// check the trivial cases
if ( pObj == NULL )
return 0;
- if ( Aig_ObjIsPi(pObj) )
+ if ( Aig_ObjIsCi(pObj) )
return 0;
if ( pObj->fMarkA )
return 1;
@@ -289,7 +289,7 @@ int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose )
{
Aig_Obj_t * pFanin;
int fAcyclic;
- if ( Aig_ObjIsPi(pNode) || Aig_ObjIsConst1(pNode) )
+ if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
return 1;
assert( Aig_ObjIsNode(pNode) );
// make sure the node is not visited
diff --git a/src/proof/dch/dchClass.c b/src/proof/dch/dchClass.c
index 24476309..1f974236 100644
--- a/src/proof/dch/dchClass.c
+++ b/src/proof/dch/dchClass.c
@@ -350,12 +350,12 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
{
if ( fLatchCorr )
{
- if ( !Aig_ObjIsPi(pObj) )
+ if ( !Aig_ObjIsCi(pObj) )
continue;
}
else
{
- if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
continue;
// skip the node with more that the given number of levels
if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
@@ -400,7 +400,7 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
nEntries2 = 0;
Aig_ManForEachObj( p->pAig, pObj, i )
{
- if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
continue;
nNodes = p->pClassSizes[pObj->Id];
// skip the nodes that are not representatives of non-trivial classes
diff --git a/src/proof/dch/dchCnf.c b/src/proof/dch/dchCnf.c
index 4175a123..b65b096c 100644
--- a/src/proof/dch/dchCnf.c
+++ b/src/proof/dch/dchCnf.c
@@ -217,7 +217,7 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
// if the new node is complemented or a PI, another gate begins
- if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) ||
+ if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ||
(!fFirst && Aig_ObjRefs(pObj) > 1) ||
(fUseMuxes && Aig_ObjIsMuxType(pObj)) )
{
@@ -243,7 +243,7 @@ void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
void Dch_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
{
assert( !Aig_IsComplement(pObj) );
- assert( !Aig_ObjIsPi(pObj) );
+ assert( !Aig_ObjIsCi(pObj) );
Vec_PtrClear( vSuper );
Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
}
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
index 808e754a..6f69b47e 100644
--- a/src/proof/dch/dchSimSat.c
+++ b/src/proof/dch/dchSimSat.c
@@ -113,7 +113,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
return;
Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
- if ( Aig_ObjIsPi(pObj) )
+ if ( Aig_ObjIsCi(pObj) )
{
Aig_Obj_t * pObjFraig;
int nVarNum;
@@ -151,7 +151,7 @@ void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) )
return;
Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
- if ( Aig_ObjIsPi(pObj) )
+ if ( Aig_ObjIsCi(pObj) )
{
// set random value
pObj->fMarkB = Aig_ManRandom(0) & 1;