diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-09 19:50:18 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-09 19:50:18 -0800 |
commit | c46c957a0721004eb21c5f3d3f316ba1c8ab8df1 (patch) | |
tree | ede7a13119d06c192e7da95992d503107d2f1651 /src/proof/dch | |
parent | 2c8f1a67ec9295450a72fc27cbb3ed1177945734 (diff) | |
download | abc-c46c957a0721004eb21c5f3d3f316ba1c8ab8df1.tar.gz abc-c46c957a0721004eb21c5f3d3f316ba1c8ab8df1.tar.bz2 abc-c46c957a0721004eb21c5f3d3f316ba1c8ab8df1.zip |
Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)...
Diffstat (limited to 'src/proof/dch')
-rw-r--r-- | src/proof/dch/dchAig.c | 8 | ||||
-rw-r--r-- | src/proof/dch/dchChoice.c | 4 | ||||
-rw-r--r-- | src/proof/dch/dchClass.c | 6 | ||||
-rw-r--r-- | src/proof/dch/dchCnf.c | 4 | ||||
-rw-r--r-- | src/proof/dch/dchSimSat.c | 4 |
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; |