diff options
Diffstat (limited to 'src/proof')
50 files changed, 263 insertions, 263 deletions
diff --git a/src/proof/bbr/bbrNtbdd.c b/src/proof/bbr/bbrNtbdd.c index 09456df0..49c2873b 100644 --- a/src/proof/bbr/bbrNtbdd.c +++ b/src/proof/bbr/bbrNtbdd.c @@ -136,7 +136,7 @@ int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ) int RetValue, i; // complement the global functions vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) ); - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) ); RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) ); Vec_PtrFree( vFuncsGlob ); @@ -171,7 +171,7 @@ DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropI // assign the constant node BDD Aig_ObjSetGlobalBdd( Aig_ManConst1(p), dd->one ); Cudd_Ref( dd->one ); // set the elementary variables - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) { Aig_ObjSetGlobalBdd( pObj, dd->vars[i] ); Cudd_Ref( dd->vars[i] ); } @@ -180,7 +180,7 @@ DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropI Counter = 0; // construct the BDDs // pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) ); - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose ); if ( bFunc == NULL ) diff --git a/src/proof/dch/dchAig.c b/src/proof/dch/dchAig.c index 91a00c63..59828443 100644 --- a/src/proof/dch/dchAig.c +++ b/src/proof/dch/dchAig.c @@ -83,21 +83,21 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAigTotal); // map primary inputs - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) { - pObjPi = Aig_ObjCreatePi( pAigTotal ); + pObjPi = Aig_ObjCreateCi( pAigTotal ); Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) Aig_ManPi( pAig2, i )->pData = pObjPi; } // construct the AIG in the order of POs - Aig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachCo( pAig, pObj, i ) { Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) { pObjPo = Aig_ManPo( pAig2, i ); Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) ); } - Aig_ObjCreatePo( pAigTotal, Aig_ObjChild0Copy(pObj) ); + Aig_ObjCreateCo( pAigTotal, Aig_ObjChild0Copy(pObj) ); } /* // mark the cone of the first AIG diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c index 1772f8aa..1de11509 100644 --- a/src/proof/dch/dchChoice.c +++ b/src/proof/dch/dchChoice.c @@ -255,14 +255,14 @@ Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig ) // map constants and PIs Aig_ManCleanData( pAig ); Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices); - Aig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pChoices ); + Aig_ManForEachCi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreateCi( pChoices ); // construct choices for the internal nodes assert( pAig->pReprs != NULL ); Aig_ManForEachNode( pAig, pObj, i ) Dch_DeriveChoiceAigNode( pChoices, pAig, pObj ); - Aig_ManForEachPo( pAig, pObj, i ) - Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); + Aig_ManForEachCo( pAig, pObj, i ) + Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); Dch_DeriveChoiceCountEquivs( pChoices ); // there is no need for cleanup ABC_FREE( pChoices->pReprs ); @@ -384,7 +384,7 @@ int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose ) // pNode->TravId < pNet->nTravIds - 1 means "pNode is not visited" // traverse the network to detect cycles fAcyclic = 1; - Aig_ManForEachPo( p, pNode, i ) + Aig_ManForEachCo( p, pNode, i ) { pNode = Aig_ObjFanin0(pNode); if ( Aig_ObjIsTravIdPrevious(p, pNode) ) @@ -454,14 +454,14 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig ) // map constants and PIs Aig_ManCleanData( pAig ); Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices); - Aig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pChoices ); + Aig_ManForEachCi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreateCi( pChoices ); // construct choices for the internal nodes assert( pAig->pReprs != NULL ); Aig_ManForEachNode( pAig, pObj, i ) Dch_DeriveChoiceAigNode( pChoices, pAig, pObj ); - Aig_ManForEachPo( pAig, pObj, i ) - Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); + Aig_ManForEachCo( pAig, pObj, i ) + Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) ); Dch_DeriveChoiceCountEquivs( pChoices ); Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) ); return pChoices; diff --git a/src/proof/dch/dchSim.c b/src/proof/dch/dchSim.c index b2d24761..3e7c575b 100644 --- a/src/proof/dch/dchSim.c +++ b/src/proof/dch/dchSim.c @@ -211,7 +211,7 @@ void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims ) memset( pSim, 0xff, sizeof(unsigned) * nWords ); // assign primary input random sim info - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) { pSim = Dch_ObjSim( vSims, pObj ); for ( k = 0; k < nWords; k++ ) diff --git a/src/proof/dch/dchSweep.c b/src/proof/dch/dchSweep.c index a1c4f79b..dafab06e 100644 --- a/src/proof/dch/dchSweep.c +++ b/src/proof/dch/dchSweep.c @@ -112,8 +112,8 @@ void Dch_ManSweep( Dch_Man_t * p ) p->pAigFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAigTotal) ); Aig_ManCleanData( p->pAigTotal ); Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig); - Aig_ManForEachPi( p->pAigTotal, pObj, i ) - pObj->pData = Aig_ObjCreatePi( p->pAigFraig ); + Aig_ManForEachCi( p->pAigTotal, pObj, i ) + pObj->pData = Aig_ObjCreateCi( p->pAigFraig ); // sweep internal nodes pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) ); Aig_ManForEachNode( p->pAigTotal, pObj, i ) diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c index 7b4db3de..b0dd3c86 100644 --- a/src/proof/fra/fraBmc.c +++ b/src/proof/fra/fraBmc.c @@ -250,7 +250,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos ) Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) ); for ( f = 0; f < p->nFramesAll; f++ ) Aig_ManForEachPiSeq( p->pAig, pObj, i ) - Bmc_ObjSetFrames( pObj, f, Aig_ObjCreatePi(pAigFrames) ); + Bmc_ObjSetFrames( pObj, f, Aig_ObjCreateCi(pAigFrames) ); // set initial state for the latches Aig_ManForEachLoSeq( p->pAig, pObj, i ) Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) ); @@ -283,7 +283,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos ) { for ( f = 0; f < p->nFramesAll; f++ ) Aig_ManForEachPoSeq( p->pAig, pObj, i ) - Aig_ObjCreatePo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) ); + Aig_ObjCreateCo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) ); Aig_ManCleanup( pAigFrames ); } else @@ -291,7 +291,7 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos ) // add POs to all the dangling nodes Aig_ManForEachObj( pAigFrames, pObjNew, i ) if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 ) - Aig_ObjCreatePo( pAigFrames, pObjNew ); + Aig_ObjCreateCo( pAigFrames, pObjNew ); } // return the new manager return pAigFrames; diff --git a/src/proof/fra/fraClass.c b/src/proof/fra/fraClass.c index 67351f6d..f7850241 100644 --- a/src/proof/fra/fraClass.c +++ b/src/proof/fra/fraClass.c @@ -779,7 +779,7 @@ static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pOb pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) ); pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); pMiter = Aig_Not( pMiter ); - Aig_ObjCreatePo( pManFraig, pMiter ); + Aig_ObjCreateCo( pManFraig, pMiter ); } /**Function************************************************************* @@ -811,14 +811,14 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) ); // create latches for the first frame Aig_ManForEachLoSeq( p->pAig, pObj, i ) - Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); + Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) ); // add timeframes pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) ); for ( f = 0; f < nFramesAll; f++ ) { // create PIs for this frame Aig_ManForEachPiSeq( p->pAig, pObj, i ) - Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) ); + Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreateCi(pManFraig) ); // set the constraints on the latch outputs Aig_ManForEachLoSeq( p->pAig, pObj, i ) Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs ); diff --git a/src/proof/fra/fraClau.c b/src/proof/fra/fraClau.c index 48640d1d..28e9e9b9 100644 --- a/src/proof/fra/fraClau.c +++ b/src/proof/fra/fraClau.c @@ -109,7 +109,7 @@ Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf ) Aig_Obj_t * pObj; int i; vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) ); - Aig_ManForEachPo( pMan, pObj, i ) + Aig_ManForEachCo( pMan, pObj, i ) Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] ); return vVars; } @@ -131,7 +131,7 @@ Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStar Aig_Obj_t * pObj; int i; vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting ); - Aig_ManForEachPi( pMan, pObj, i ) + Aig_ManForEachCi( pMan, pObj, i ) { if ( i < nStarting ) continue; diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c index e71219b5..f27c63ce 100644 --- a/src/proof/fra/fraClaus.c +++ b/src/proof/fra/fraClaus.c @@ -1565,7 +1565,7 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p ) pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] ); pClause = Aig_Or( pNew, pClause, pLiteral ); } - Aig_ObjCreatePo( pNew, pClause ); + Aig_ObjCreateCo( pNew, pClause ); Beg = End; } ABC_FREE( pVar2Id ); diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c index d3b60ab7..1969b36d 100644 --- a/src/proof/fra/fraCore.c +++ b/src/proof/fra/fraCore.c @@ -193,12 +193,12 @@ void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex ) assert( !pObj->fMarkB ); // simulate the cex through the AIG Aig_ManConst1(p->pManAig)->fMarkB = 1; - Aig_ManForEachPi( p->pManAig, pObj, i ) + Aig_ManForEachCi( p->pManAig, pObj, i ) pObj->fMarkB = Vec_IntEntry(vCex, i); Aig_ManForEachNode( p->pManAig, pObj, i ) pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); - Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ManForEachCo( p->pManAig, pObj, i ) pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); // check if the classes hold Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i ) diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c index 29c9c33d..03dd468a 100644 --- a/src/proof/fra/fraHot.c +++ b/src/proof/fra/fraHot.c @@ -402,9 +402,9 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots ) int i, Out1, Out2, nTruePis; pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 ); // for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ ) -// Aig_ObjCreatePi(pNew); - Aig_ManForEachPi( p->pManAig, pObj, i ) - Aig_ObjCreatePi(pNew); +// Aig_ObjCreateCi(pNew); + Aig_ManForEachCi( p->pManAig, pObj, i ) + Aig_ObjCreateCi(pNew); nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) { @@ -417,7 +417,7 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots ) pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) ); pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) ); pObj = Aig_Or( pNew, pObj1, pObj2 ); - Aig_ObjCreatePo( pNew, pObj ); + Aig_ObjCreateCo( pNew, pObj ); } Aig_ManCleanup(pNew); // printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) ); diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c index 9877ceaa..de24f179 100644 --- a/src/proof/fra/fraImp.c +++ b/src/proof/fra/fraImp.c @@ -717,7 +717,7 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ) pMiter = Aig_Or( pNew, Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase), Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); - Aig_ObjCreatePo( pNew, pMiter ); + Aig_ObjCreateCo( pNew, pMiter ); } pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld; } diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c index 1224bab3..b8a1e6bf 100644 --- a/src/proof/fra/fraInd.c +++ b/src/proof/fra/fraInd.c @@ -112,7 +112,7 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew ); pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) ); assert( Aig_ObjPhaseReal(pMiter) == 1 ); - Aig_ObjCreatePo( pManFraig, pMiter ); + Aig_ObjCreateCo( pManFraig, pMiter ); } /**Function************************************************************* @@ -145,10 +145,10 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) ); for ( f = 0; f < p->nFramesAll; f++ ) Aig_ManForEachPiSeq( p->pManAig, pObj, i ) - Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) ); + Fra_ObjSetFraig( pObj, f, Aig_ObjCreateCi(pManFraig) ); // create latches for the first frame Aig_ManForEachLoSeq( p->pManAig, pObj, i ) - Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); + Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) ); // add timeframes // pManFraig->fAddStrash = 1; @@ -173,7 +173,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) pManFraig->nAsserts = Aig_ManPoNum(pManFraig); // add the POs for the latch outputs of the last frame Aig_ManForEachLoSeq( p->pManAig, pObj, i ) - Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) ); + Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) ); // remove dangling nodes Aig_ManCleanup( pManFraig ); diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c index 238e3096..d24b37f6 100644 --- a/src/proof/fra/fraLcr.c +++ b/src/proof/fra/fraLcr.c @@ -134,7 +134,7 @@ void Lcr_ManFree( Fra_Lcr_t * p ) int i; if ( p->fVerbose ) Lcr_ManPrint( p ); - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) pObj->pNext = NULL; Vec_PtrFree( p->vFraigs ); if ( p->pCla ) Fra_ClassesStop( p->pCla ); @@ -162,7 +162,7 @@ Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig ) int i; p = ABC_ALLOC( Fra_Man_t, 1 ); memset( p, 0, sizeof(Fra_Man_t) ); -// Aig_ManForEachPi( pAig, pObj, i ) +// Aig_ManForEachCi( pAig, pObj, i ) Aig_ManForEachObj( pAig, pObj, i ) pObj->pData = p; return p; @@ -183,7 +183,7 @@ void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p ) { Aig_Obj_t * pObj; int i; - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) pObj->pData = p; } @@ -300,7 +300,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter; int i, c, Offset; // remember the numbers of the inputs of the original AIG - Aig_ManForEachPi( pLcr->pAig, pObj, i ) + Aig_ManForEachCi( pLcr->pAig, pObj, i ) { pObj->pData = pLcr; pObj->pNext = (Aig_Obj_t *)(long)i; @@ -321,7 +321,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) ); pMiter = Aig_Exor( pNew, pMiter, pObjNew ); } - Aig_ObjCreatePo( pNew, pMiter ); + Aig_ObjCreateCo( pNew, pMiter ); } // go over the constant candidates Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i ) @@ -329,7 +329,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) assert( Aig_ObjIsPi(pObj) ); pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext ); pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) ); - Aig_ObjCreatePo( pNew, pMiter ); + Aig_ObjCreateCo( pNew, pMiter ); } return pNew; } @@ -403,7 +403,7 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t // Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj); Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id]; if ( pRepr == NULL ) - pObj->pData = Aig_ObjCreatePi( pNew ); + pObj->pData = Aig_ObjCreateCi( pNew ); else { pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr ); @@ -447,7 +447,7 @@ Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart ) } else pObjNew = Aig_ManConst1( pNew ); - Aig_ObjCreatePo( pNew, pObjNew ); + Aig_ObjCreateCo( pNew, pObjNew ); } return pNew; } diff --git a/src/proof/fra/fraMan.c b/src/proof/fra/fraMan.c index 90e8b762..67832f83 100644 --- a/src/proof/fra/fraMan.c +++ b/src/proof/fra/fraMan.c @@ -187,8 +187,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) pManFraig->nAsserts = p->pManAig->nAsserts; // set the pointers to the available fraig nodes Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) ); - Aig_ManForEachPi( p->pManAig, pObj, i ) - Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); + Aig_ManForEachCi( p->pManAig, pObj, i ) + Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) ); // set the pointers to the manager Aig_ManForEachObj( pManFraig, pObj, i ) pObj->pData = p; @@ -219,8 +219,8 @@ void Fra_ManFinalizeComb( Fra_Man_t * p ) Aig_Obj_t * pObj; int i; // add the POs - Aig_ManForEachPo( p->pManAig, pObj, i ) - Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) ); + Aig_ManForEachCo( p->pManAig, pObj, i ) + Aig_ObjCreateCo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) ); // postprocess Aig_ManCleanMarkB( p->pManFraig ); } diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c index e9739f97..6594ac0b 100644 --- a/src/proof/fra/fraPart.c +++ b/src/proof/fra/fraPart.c @@ -64,7 +64,7 @@ clk = clock(); vSupps = (Vec_Vec_t *)Aig_ManSupports( p ); ABC_PRT( "Supports", clock() - clk ); // remove last entry - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { vSup = Vec_VecEntryInt( vSupps, i ); Vec_IntPop( vSup ); @@ -75,7 +75,7 @@ ABC_PRT( "Supports", clock() - clk ); // create reverse supports clk = clock(); vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) ); - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { vSup = Vec_VecEntryInt( vSupps, i ); Vec_IntForEachEntry( vSup, Entry, k ) @@ -90,7 +90,7 @@ clk = clock(); vOverNew = Vec_IntAlloc( Aig_ManPoNum(p) ); vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) ); // pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) ); - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { // Bar_ProgressUpdate( pProgress, i, NULL ); // get old supports @@ -101,7 +101,7 @@ clk = clock(); CountOver = CountQuant = 0; vSupNew = Vec_IntDup( vSup ); // go through the nodes where the first var appears - Aig_ManForEachPo( p, pObj, k ) + Aig_ManForEachCo( p, pObj, k ) // iVar = Vec_IntEntry( vSup, 0 ); // vSupIn = Vec_VecEntry( vSuppsIn, iVar ); // Vec_IntForEachEntry( vSupIn, Entry, k ) @@ -198,7 +198,7 @@ clk = clock(); vSupps = (Vec_Vec_t *)Aig_ManSupports( p ); ABC_PRT( "Supports", clock() - clk ); // remove last entry - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { vSup = Vec_VecEntryInt( vSupps, i ); Vec_IntPop( vSup ); @@ -209,7 +209,7 @@ ABC_PRT( "Supports", clock() - clk ); // create reverse supports clk = clock(); vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) ); - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { if ( i == p->nAsserts ) break; @@ -222,7 +222,7 @@ ABC_PRT( "Inverse ", clock() - clk ); // create affective supports clk = clock(); pSupp = ABC_ALLOC( char, Aig_ManPiNum(p) ); - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { if ( i % 50 != 0 ) continue; diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c index eb42c665..e54846bc 100644 --- a/src/proof/fra/fraSim.c +++ b/src/proof/fra/fraSim.c @@ -243,7 +243,7 @@ void Fra_SmlSavePattern( Fra_Man_t * p ) Aig_Obj_t * pObj; int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); - Aig_ManForEachPi( p->pManFraig, pObj, i ) + Aig_ManForEachCi( p->pManFraig, pObj, i ) // if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True ) if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) ) Abc_InfoSetBit( p->pPatWords, i ); @@ -259,7 +259,7 @@ void Fra_SmlSavePattern( Fra_Man_t * p ) /* printf( "Pattern: " ); - Aig_ManForEachPi( p->pManFraig, pObj, i ) + Aig_ManForEachCi( p->pManFraig, pObj, i ) printf( "%d", Abc_InfoHasBit( p->pPatWords, i ) ); printf( "\n" ); */ @@ -299,7 +299,7 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo ) BestPat = i * 32 + k; // fill in the counter-example data pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 ); - Aig_ManForEachPi( p->pManAig, pObjPi, i ) + Aig_ManForEachCi( p->pManAig, pObjPi, i ) { pModel[i] = Abc_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat); // printf( "%d", pModel[i] ); @@ -330,7 +330,7 @@ int Fra_SmlCheckOutput( Fra_Man_t * p ) // make sure the reference simulation pattern does not detect the bug pObj = Aig_ManPo( p->pManAig, 0 ); assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); - Aig_ManForEachPo( p->pManAig, pObj, i ) + Aig_ManForEachCo( p->pManAig, pObj, i ) { if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) ) { @@ -414,7 +414,7 @@ void Fra_SmlInitialize( Fra_Sml_t * p, int fInit ) } else { - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) Fra_SmlAssignRandom( p, pObj ); } } @@ -438,7 +438,7 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) if ( p->nFrames == 1 ) { // copy the PI info - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 ); // flip one bit Limit = Abc_MinInt( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); @@ -980,7 +980,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in // find the PO that failed iPo = -1; iFrame = -1; - Aig_ManForEachPo( pFrames, pObj, i ) + Aig_ManForEachCo( pFrames, pObj, i ) if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] ) { iPo = i % nTruePos; diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c index 6b36fe30..57d6e7d0 100644 --- a/src/proof/int/intCheck.c +++ b/src/proof/int/intCheck.c @@ -67,13 +67,13 @@ Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames ) Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); // create variables for register outputs Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); + pObj->pData = Aig_ObjCreateCi( pFrames ); // add timeframes for ( f = 0; f < nFrames; f++ ) { // create PI nodes for this frame Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); + pObj->pData = Aig_ObjCreateCi( pFrames ); // add internal nodes of this frame Aig_ManForEachNode( pAig, pObj, i ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); @@ -84,7 +84,7 @@ Aig_Man_t * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames ) Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) { pObjLo->pData = pObjLi->pData; - Aig_ObjCreatePo( pFrames, (Aig_Obj_t *)pObjLo->pData ); + Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLo->pData ); } } Aig_ManCleanup( pFrames ); @@ -240,7 +240,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut assert( RetValue ); } // add equality clauses for the flop variables - Aig_ManForEachPi( pCnfInt->pMan, pObj, i ) + Aig_ManForEachCi( pCnfInt->pMan, pObj, i ) { pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i); Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] ); diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c index 58b408d7..213c557c 100644 --- a/src/proof/int/intContain.c +++ b/src/proof/int/intContain.c @@ -121,7 +121,7 @@ Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) ); Saig_ManForEachLo( pAig, pObj, i ) { - pObj->pData = Aig_ObjCreatePi( pFrames ); + pObj->pData = Aig_ObjCreateCi( pFrames ); Vec_PtrPush( *pvMapReg, pObj->pData ); } // add timeframes @@ -129,7 +129,7 @@ Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** { // create PI nodes for this frame Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); + pObj->pData = Aig_ObjCreateCi( pFrames ); // add internal nodes of this frame Aig_ManForEachNode( pAig, pObj, i ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); @@ -165,14 +165,14 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew // create the PIs Aig_ManCleanData( pOld ); Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( pOld, pObj, i ) + Aig_ManForEachCi( pOld, pObj, i ) pObj->pData = ppNewPis[i]; // duplicate internal nodes Aig_ManForEachNode( pOld, pObj, i ) pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); // add one PO to new pObj = Aig_ManPo( pOld, 0 ); - Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); + Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); } @@ -287,7 +287,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf // get the counter-example vPis = Vec_IntAlloc( 100 ); - Aig_ManForEachPi( pCnf->pMan, pObj, k ) + Aig_ManForEachCi( pCnf->pMan, pObj, k ) Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] ); assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) ); pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize ); diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c index 9ba8c9df..22e689f4 100644 --- a/src/proof/int/intCtrex.c +++ b/src/proof/int/intCtrex.c @@ -61,7 +61,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) { // create PI nodes for this frame Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); + pObj->pData = Aig_ObjCreateCi( pFrames ); // add internal nodes of this frame Aig_ManForEachNode( pAig, pObj, i ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); @@ -76,7 +76,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) } // create POs for the output of the last frame pObj = Aig_ManPo( pAig, 0 ); - Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) ); Aig_ManCleanup( pFrames ); return pFrames; } diff --git a/src/proof/int/intDup.c b/src/proof/int/intDup.c index 551473ef..adc692cb 100644 --- a/src/proof/int/intDup.c +++ b/src/proof/int/intDup.c @@ -52,9 +52,9 @@ Aig_Man_t * Inter_ManStartInitState( int nRegs ) ppInputs = ABC_ALLOC( Aig_Obj_t *, nRegs ); p = Aig_ManStart( nRegs ); for ( i = 0; i < nRegs; i++ ) - ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) ); + ppInputs[i] = Aig_Not( Aig_ObjCreateCi(p) ); pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND ); - Aig_ObjCreatePo( p, pRes ); + Aig_ObjCreateCo( p, pRes ); ABC_FREE( ppInputs ); return p; } @@ -83,8 +83,8 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p ) // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( p, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pNew ); + Aig_ManForEachCi( p, pObj, i ) + pObj->pData = Aig_ObjCreateCi( pNew ); // set registers pNew->nTruePis = p->nTruePis; pNew->nTruePos = Saig_ManConstrNum(p); @@ -98,12 +98,12 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p ) { if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) ) continue; - Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); + Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); } // create register inputs with MUXes Saig_ManForEachLi( p, pObj, i ) - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); Aig_ManCleanup( pNew ); return pNew; } @@ -133,11 +133,11 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ) // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) { if ( i == Saig_ManPiNum(p) ) - pCtrl = Aig_ObjCreatePi( pNew ); - pObj->pData = Aig_ObjCreatePi( pNew ); + pCtrl = Aig_ObjCreateCi( pNew ); + pObj->pData = Aig_ObjCreateCi( pNew ); } // set registers pNew->nRegs = fAddFirstPo? 0 : p->nRegs; @@ -152,14 +152,14 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ) { if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) ) continue; - Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); + Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); } // add the PO if ( fAddFirstPo ) { pObj = Aig_ManPo( p, 0 ); - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); } else { @@ -168,7 +168,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ) { pObj = Aig_Mux( pNew, pCtrl, (Aig_Obj_t *)pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); // pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) ); - Aig_ObjCreatePo( pNew, pObj ); + Aig_ObjCreateCo( pNew, pObj ); } } Aig_ManCleanup( pNew ); diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c index 0fbab6cb..8e74d99a 100644 --- a/src/proof/int/intFrames.c +++ b/src/proof/int/intFrames.c @@ -63,14 +63,14 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts else { Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); + pObj->pData = Aig_ObjCreateCi( pFrames ); } // add timeframes for ( f = 0; f < nFrames; f++ ) { // create PI nodes for this frame Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); + pObj->pData = Aig_ObjCreateCi( pFrames ); // add internal nodes of this frame Aig_ManForEachNode( pAig, pObj, i ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); @@ -79,7 +79,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts { if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) ) continue; - Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); + Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) ); } if ( f == nFrames - 1 ) break; @@ -94,13 +94,13 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts if ( fAddRegOuts ) { Saig_ManForEachLi( pAig, pObj, i ) - Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) ); } // create the only PO of the manager else { pObj = Aig_ManPo( pAig, 0 ); - Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) ); } Aig_ManCleanup( pFrames ); return pFrames; diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c index 139c9bbd..c37cb2c6 100644 --- a/src/proof/int/intM114.c +++ b/src/proof/int/intM114.c @@ -113,7 +113,7 @@ sat_solver * Inter_ManDeriveSatSolver( } else { - Aig_ManForEachPi( pInter, pObj, i ) + Aig_ManForEachCi( pInter, pObj, i ) { pObj2 = Saig_ManLo( pAig, i ); @@ -137,7 +137,7 @@ sat_solver * Inter_ManDeriveSatSolver( Vec_IntClear( vVarsAB ); if ( fUseBackward ) { - Aig_ManForEachPo( pFrames, pObj, i ) + Aig_ManForEachCo( pFrames, pObj, i ) { assert( pCnfFrames->pVarNums[pObj->Id] >= 0 ); Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] ); @@ -155,7 +155,7 @@ sat_solver * Inter_ManDeriveSatSolver( } else { - Aig_ManForEachPi( pFrames, pObj, i ) + Aig_ManForEachCi( pFrames, pObj, i ) { if ( i == Aig_ManRegNum(pAig) ) break; diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c index 7c011426..6164a389 100644 --- a/src/proof/int/intM114p.c +++ b/src/proof/int/intM114p.c @@ -87,7 +87,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p( assert( 0 ); } // connector clauses - Aig_ManForEachPi( pInter, pObj, i ) + Aig_ManForEachCi( pInter, pObj, i ) { pObj2 = Saig_ManLo( pAig, i ); Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); @@ -109,7 +109,7 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p( assert( 0 ); } // connector clauses - Aig_ManForEachPi( pFrames, pObj, i ) + Aig_ManForEachCi( pFrames, pObj, i ) { if ( i == Aig_ManRegNum(pAig) ) break; @@ -296,7 +296,7 @@ Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapR Vec_IntFree( vLiterals ); Vec_IntFree( vClauses ); Vec_IntFree( vResolvent ); - Aig_ObjCreatePo( p, pInter ); + Aig_ObjCreateCo( p, pInter ); Aig_ManCleanup( p ); return p; } @@ -372,7 +372,7 @@ Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) ); Vec_PtrFree( vInters ); - Aig_ObjCreatePo( p, pInter ); + Aig_ObjCreateCo( p, pInter ); Aig_ManCleanup( p ); assert( Aig_ManCheck(p) ); return p; diff --git a/src/proof/live/liveness.c b/src/proof/live/liveness.c index a86a8cd1..d961e509 100644 --- a/src/proof/live/liveness.c +++ b/src/proof/live/liveness.c @@ -119,7 +119,7 @@ char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pA int index; assert( Saig_ObjIsPi( pAigNew, pObjPivot ) ); - Aig_ManForEachPi( pAigNew, pObj, index ) + Aig_ManForEachCi( pAigNew, pObj, index ) if( pObj == pObjPivot ) break; assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) ); @@ -287,7 +287,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ Saig_ManForEachPi( p, pObj, i ) { piCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); @@ -298,7 +298,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - pObjSavePi = Aig_ObjCreatePi( pNew ); + pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); } @@ -309,7 +309,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ Saig_ManForEachLo( p, pObj, i ) { loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); @@ -321,7 +321,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { loCreated++; - pObjSavedLo = Aig_ObjCreatePi( pNew ); + pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); @@ -360,7 +360,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } - pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) ); + pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) ); } else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 ) { @@ -379,12 +379,12 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } collectiveAssumeSafety = pObjAndAcc; - pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); + pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); } else { printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n"); - pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); + pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); } } @@ -394,7 +394,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ //******************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); + pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); } // create register inputs for the original registers @@ -403,7 +403,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); - Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); + Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } @@ -412,7 +412,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { #ifndef DUPLICATE_CKT_DEBUG - pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved ); + pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++; @@ -423,7 +423,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator Saig_ManForEachLo( p, pObj, i ) { - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -434,7 +434,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ #endif pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -459,7 +459,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ { liveLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -469,7 +469,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ #endif pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -488,7 +488,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ { fairLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -498,7 +498,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ #endif pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -584,7 +584,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M Saig_ManForEachPi( p, pObj, i ) { piCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); @@ -595,7 +595,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - pObjSavePi = Aig_ObjCreatePi( pNew ); + pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); } @@ -606,7 +606,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M Saig_ManForEachLo( p, pObj, i ) { loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); @@ -618,7 +618,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { loCreated++; - pObjSavedLo = Aig_ObjCreatePi( pNew ); + pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); @@ -657,7 +657,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } - Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) ); + Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) ); } else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 ) { @@ -676,12 +676,12 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAcc ); } collectiveAssumeSafety = pObjAndAcc; - Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); + Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); } else { printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n"); - Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); + Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); } } @@ -691,7 +691,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M //******************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); + pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); } // create register inputs for the original registers @@ -700,7 +700,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); - Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); + Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } @@ -709,7 +709,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { #ifndef DUPLICATE_CKT_DEBUG - pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved ); + pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++; @@ -725,7 +725,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M } Vec_IntForEachEntry( vFlops, iEntry, i ) { - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); pObj = Aig_ManLo( p, iEntry ); #ifdef PROPAGATE_NAMES @@ -737,7 +737,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M #endif pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -762,7 +762,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M { liveLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -772,7 +772,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M #endif pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -791,7 +791,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M { fairLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -801,7 +801,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M #endif pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -892,7 +892,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt Saig_ManForEachPi( p, pObj, i ) { piCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); @@ -903,7 +903,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt //**************************************************************** if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE ) { - pObjSavePi = Aig_ObjCreatePi( pNew ); + pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); } @@ -914,7 +914,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt Saig_ManForEachLo( p, pObj, i ) { loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); @@ -926,7 +926,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt #if 0 loCreated++; - pObjSavedLo = Aig_ObjCreatePi( pNew ); + pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); @@ -954,7 +954,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt //******************************************************************** Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { - pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); + pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); } #endif @@ -965,7 +965,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt pObjAndAcc = NULL; Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { - //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); + //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); if( pObjAndAcc == NULL ) pObjAndAcc = pArgument; @@ -975,14 +975,14 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt pObjAndAcc = Aig_And( pNew, pArgument, pObjAndAccDummy ); } } - Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) ); + Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) ); } else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 ) { pObjAndAcc = NULL; Vec_PtrForEachEntry( Aig_Obj_t *, vAssertSafety, pObj, i ) { - //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); + //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); if( pObjAndAcc == NULL ) pObjAndAcc = pArgument; @@ -996,7 +996,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt pObjAndAcc = NULL; Vec_PtrForEachEntry( Aig_Obj_t *, vAssumeSafety, pObj, i ) { - //pObj->pData = Aig_ObjCreatePo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); + //pObj->pData = Aig_ObjCreateCo( pNew, Aig_NotCond(Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ) ); pArgument = Aig_NotCond( (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0( pObj ) ); if( pObjAndAcc == NULL ) pObjAndAcc = pArgument; @@ -1007,7 +1007,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt } } collectiveAssumeSafety = pObjAndAcc; - Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); + Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); } else printf("No safety property is specified, hence no safety gate is created\n"); @@ -1021,7 +1021,7 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt if( mode == FULL_BIERE_ONE_LOOP_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_ONE_LOOP_MODE ) { - pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); + pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); } // create register inputs for the original registers @@ -1030,15 +1030,15 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); - //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) ); - Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); + //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) ); + Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } #if 0 // create register input corresponding to the register "saved" - pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved ); + pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++;7 #endif @@ -1919,7 +1919,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A Saig_ManForEachPi( p, pObj, i ) { piCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); @@ -1930,7 +1930,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A //**************************************************************** if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - pObjSavePi = Aig_ObjCreatePi( pNew ); + pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); } @@ -1941,7 +1941,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A Saig_ManForEachLo( p, pObj, i ) { loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); @@ -1953,7 +1953,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { loCreated++; - pObjSavedLo = Aig_ObjCreatePi( pNew ); + pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); @@ -1995,7 +1995,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A } pNegatedSafetyConjunction = Aig_Not(pObjAndAcc); if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) - pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not(pObjAndAcc) ); + pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not(pObjAndAcc) ); } else if( Vec_PtrSize( vAssertSafety ) != 0 && Vec_PtrSize( vAssumeSafety ) != 0 ) { @@ -2016,14 +2016,14 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A collectiveAssumeSafety = pObjAndAcc; pNegatedSafetyConjunction = Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ); if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) - pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); + pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_And( pNew, Aig_Not(collectiveAssertSafety), collectiveAssumeSafety ) ); } else { printf("WARNING!! No safety property is found, a new (negated) constant 1 output is created\n"); pNegatedSafetyConjunction = Aig_Not( Aig_ManConst1(pNew) ); if( mode == FULL_BIERE_MODE || mode == IGNORE_LIVENESS_KEEP_SAFETY_MODE ) - pObjOriginalSafetyPropertyOutput = Aig_ObjCreatePo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); + pObjOriginalSafetyPropertyOutput = Aig_ObjCreateCo( pNew, Aig_Not( Aig_ManConst1(pNew) ) ); } } assert( pNegatedSafetyConjunction != NULL ); @@ -2042,7 +2042,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A } for( i=0; i<Vec_PtrSize( vTopASTNodeArray ); i++ ) { - pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); + pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); Vec_PtrPush( vPoForLtlProps, pObjSafetyPropertyOutput ); } } @@ -2058,7 +2058,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); - Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); + Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } @@ -2069,7 +2069,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { #ifndef DUPLICATE_CKT_DEBUG - pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved ); + pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++; @@ -2087,7 +2087,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A // if( strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[0]" ) == 0 // || strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[1]" ) == 0 || strcmp( Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) ), "top|route0_queue1_num[2]" ) == 0 ) { - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -2098,7 +2098,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A #endif pObjShadowLiDriver = Aig_Mux( pNew, pObjSaveAndNotSaved, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -2175,9 +2175,9 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A liveLatch++; pDriverImage = pObj; - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); pObjShadowLiDriver = Aig_Or( pNew, pObjShadowLo, Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; diff --git a/src/proof/live/liveness_sim.c b/src/proof/live/liveness_sim.c index c631e187..552c5204 100644 --- a/src/proof/live/liveness_sim.c +++ b/src/proof/live/liveness_sim.c @@ -82,7 +82,7 @@ static char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Ma int index; assert( Saig_ObjIsPi( pAigNew, pObjPivot ) ); - Aig_ManForEachPi( pAigNew, pObj, index ) + Aig_ManForEachCi( pAigNew, pObj, index ) if( pObj == pObjPivot ) break; assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) ); @@ -243,7 +243,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ Saig_ManForEachPi( p, pObj, i ) { piCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); @@ -253,7 +253,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ // Step 4: create the special Pi corresponding to SAVE //**************************************************************** #ifndef DUPLICATE_CKT_DEBUG - pObjSavePi = Aig_ObjCreatePi( pNew ); + pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = Abc_UtilStrsav("SAVE_BIERE"), Vec_PtrPush( vecPiNames, nodeName ); #endif @@ -264,7 +264,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ Saig_ManForEachLo( p, pObj, i ) { loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); @@ -275,7 +275,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ //**************************************************************** #ifndef DUPLICATE_CKT_DEBUG loCreated++; - pObjSavedLo = Aig_ObjCreatePi( pNew ); + pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = Abc_UtilStrsav("SAVED_LO"); Vec_PtrPush( vecLoNames, nodeName ); @@ -303,7 +303,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ // of the whole circuit, discuss with Sat/Alan for an alternative implementation //******************************************************************** #ifndef DUPLICATE_CKT_DEBUG - pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); + pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); #endif //******************************************************************** @@ -313,7 +313,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ #ifdef DUPLICATE_CKT_DEBUG Saig_ManForEachPo( p, pObj, i ) { - Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); } #endif @@ -323,15 +323,15 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); - //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) ); - Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); + //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) ); + Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } // create register input corresponding to the register "saved" #ifndef DUPLICATE_CKT_DEBUG - pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved ); + pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++; @@ -340,7 +340,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ // create the family of shadow registers, then create the cascade of Xnor and And gates for the comparator Saig_ManForEachLo( p, pObj, i ) { - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -350,7 +350,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ #endif pObjShadowLiDriver = Aig_Mux( pNew, pObjSavePi, (Aig_Obj_t *)pObj->pData, pObjShadowLo ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -380,7 +380,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ //Aig_ObjPrint( pNew, pObj ); liveLatch++; pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -391,7 +391,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ pObjShadowLiDriver = Aig_Or( pNew, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo), Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -421,7 +421,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ fairLatch++; //assert( Aig_ObjIsNode( Aig_ObjChild0( pObj ) ) ); pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); - pObjShadowLo = Aig_ObjCreatePi( pNew ); + pObjShadowLo = Aig_ObjCreateCi( pNew ); #ifdef PROPAGATE_NAMES Vec_PtrPush( vecLos, pObjShadowLo ); @@ -432,7 +432,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ pObjShadowLiDriver = Aig_Or( pNew, Aig_Mux(pNew, pObjSavePi, Aig_Not(Aig_ManConst1(pNew)), pObjShadowLo), Aig_And( pNew, pDriverImage, pObjSaveOrSaved ) ); - pObjShadowLi = Aig_ObjCreatePo( pNew, pObjShadowLiDriver ); + pObjShadowLi = Aig_ObjCreateCo( pNew, pObjShadowLiDriver ); nRegCount++; loCreated++; liCreated++; @@ -520,7 +520,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt Saig_ManForEachPi( p, pObj, i ) { piCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecPis, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkPi( pNtk, i ) )); Vec_PtrPush( vecPiNames, nodeName ); @@ -529,7 +529,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt //**************************************************************** // Step 4: create the special Pi corresponding to SAVE //**************************************************************** - pObjSavePi = Aig_ObjCreatePi( pNew ); + pObjSavePi = Aig_ObjCreateCi( pNew ); nodeName = "SAVE_BIERE", Vec_PtrPush( vecPiNames, nodeName ); @@ -539,7 +539,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt Saig_ManForEachLo( p, pObj, i ) { loCopied++; - pObj->pData = Aig_ObjCreatePi(pNew); + pObj->pData = Aig_ObjCreateCi(pNew); Vec_PtrPush( vecLos, pObj->pData ); nodeName = Abc_UtilStrsav(Abc_ObjName( Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i ) )); Vec_PtrPush( vecLoNames, nodeName ); @@ -551,7 +551,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt #if 0 loCreated++; - pObjSavedLo = Aig_ObjCreatePi( pNew ); + pObjSavedLo = Aig_ObjCreateCi( pNew ); Vec_PtrPush( vecLos, pObjSavedLo ); nodeName = "SAVED_LO"; Vec_PtrPush( vecLoNames, nodeName ); @@ -579,7 +579,7 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt // of the whole circuit, discuss with Sat/Alan for an alternative implementation //******************************************************************** - pObjSafetyPropertyOutput = Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); + pObjSafetyPropertyOutput = Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData ); // create register inputs for the original registers nRegCount = 0; @@ -587,15 +587,15 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt Saig_ManForEachLo( p, pObj, i ) { pMatch = Saig_ObjLoToLi( p, pObj ); - //Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pMatch) ); - Aig_ObjCreatePo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); + //Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pMatch) ); + Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pMatch)->pData, Aig_ObjFaninC0( pMatch ) ) ); nRegCount++; liCopied++; } #if 0 // create register input corresponding to the register "saved" - pObjSavedLi = Aig_ObjCreatePo( pNew, pObjSaveOrSaved ); + pObjSavedLi = Aig_ObjCreateCo( pNew, pObjSaveOrSaved ); nRegCount++; liCreated++; #endif diff --git a/src/proof/llb/llb1Constr.c b/src/proof/llb/llb1Constr.c index 67fb30ba..4ce911db 100644 --- a/src/proof/llb/llb1Constr.c +++ b/src/proof/llb/llb1Constr.c @@ -236,7 +236,7 @@ DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p ) Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); pObj = Aig_ManConst1(p); pObj->pData = Cudd_ReadOne(dd); Cudd_Ref( (DdNode *)pObj->pData ); - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) { pObj->pData = Cudd_bddIthVar(dd, i); Cudd_Ref( (DdNode *)pObj->pData ); } @@ -246,7 +246,7 @@ DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p ) bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData ); } - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) { pObj->pData = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); Cudd_Ref( (DdNode *)pObj->pData ); } diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c index f68030ff..6e705a38 100644 --- a/src/proof/llb/llb1Hint.c +++ b/src/proof/llb/llb1Hint.c @@ -46,7 +46,7 @@ int Llb_ManMaxFanoutCi( Aig_Man_t * pAig ) { Aig_Obj_t * pObj; int i, WeightMax = -ABC_INFINITY, iInput = -1; - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) if ( WeightMax < Aig_ObjRefs(pObj) ) { WeightMax = Aig_ObjRefs(pObj); diff --git a/src/proof/llb/llb1Pivot.c b/src/proof/llb/llb1Pivot.c index 688060bc..7a5bb66f 100644 --- a/src/proof/llb/llb1Pivot.c +++ b/src/proof/llb/llb1Pivot.c @@ -154,7 +154,7 @@ void Llb_ManLabelLiCones( Aig_Man_t * p ) int i; // mark const and PIs Aig_ManConst1(p)->fMarkB = 1; - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) pObj->fMarkB = 1; // mark cones Saig_ManForEachLi( p, pObj, i ) @@ -223,7 +223,7 @@ Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal ) Aig_Obj_t * pObj; int i; // mark inputs/outputs - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) pObj->fMarkA = 1; Saig_ManForEachLi( p, pObj, i ) pObj->fMarkA = 1; @@ -235,7 +235,7 @@ Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal ) // assign variable numbers Aig_ManConst1(p)->fMarkA = 0; vVar2Obj = Vec_IntAlloc( 100 ); - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) Vec_IntPush( vVar2Obj, Aig_ObjId(pObj) ); Aig_ManForEachNode( p, pObj, i ) if ( pObj->fMarkA ) diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c index 722a8342..d8c667ae 100644 --- a/src/proof/llb/llb1Reach.c +++ b/src/proof/llb/llb1Reach.c @@ -430,7 +430,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs // transfer them to the global AIG Aig_ManCleanData( p->pAigGlo ); Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd ); - Aig_ManForEachPi( p->pAigGlo, pObj, i ) + Aig_ManForEachCi( p->pAigGlo, pObj, i ) pObj->pData = Aig_ManPi(p->pAig, i)->pData; // derive consraints bConstr = Cudd_ReadOne( p->dd ); Cudd_Ref( bConstr ); diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c index 544d7c04..295f0bfe 100644 --- a/src/proof/llb/llb2Flow.c +++ b/src/proof/llb/llb2Flow.c @@ -960,7 +960,7 @@ void Llb_ManFlowPrepareCut( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUppe } // clean PIs and const Aig_ManConst1(p)->fMarkB = 0; - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) pObj->fMarkB = 0; // clean upper cut //printf( "Upper: "); @@ -1077,7 +1077,7 @@ Vec_Ptr_t * Llb_ManComputeCutLo( Aig_Man_t * p ) Aig_Obj_t * pObj; int i; vMinCut = Vec_PtrAlloc( 100 ); - Aig_ManForEachPi( p, pObj, i ) + Aig_ManForEachCi( p, pObj, i ) Vec_PtrPush( vMinCut, pObj ); return vMinCut; } diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c index d28edecc..678a6fff 100644 --- a/src/proof/llb/llb3Nonlin.c +++ b/src/proof/llb/llb3Nonlin.c @@ -712,7 +712,7 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * p p->vRings = Vec_PtrAlloc( 100 ); // create leaves p->vLeaves = Vec_PtrAlloc( Aig_ManPiNum(pAig) ); - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) Vec_PtrPush( p->vLeaves, pObj ); // create roots p->vRoots = Vec_PtrAlloc( Aig_ManPoNum(pAig) ); @@ -723,7 +723,7 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * p p->pOrderL2= ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); p->pOrderG = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) ); - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) p->pVars2Q[Aig_ObjId(pObj)] = 1; for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ ) p->pOrderL[i] = p->pOrderL2[i] = p->pOrderG[i] = i; diff --git a/src/proof/llb/llb4Cex.c b/src/proof/llb/llb4Cex.c index 3a1c96e5..69ba6ab1 100644 --- a/src/proof/llb/llb4Cex.c +++ b/src/proof/llb/llb4Cex.c @@ -230,7 +230,7 @@ Vec_Ptr_t * Llb4_Nonlin4VerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) Aig_ManForEachNode( pAig, pObj, k ) pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); - Aig_ManForEachPo( pAig, pObj, k ) + Aig_ManForEachCo( pAig, pObj, k ) pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); if ( i == p->iFrame ) break; diff --git a/src/proof/llb/llb4Cluster.c b/src/proof/llb/llb4Cluster.c index 8d29eed4..c151a618 100644 --- a/src/proof/llb/llb4Cluster.c +++ b/src/proof/llb/llb4Cluster.c @@ -94,20 +94,20 @@ Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig, int * pCounter ) Aig_ManForEachNode( pAig, pObj, i ) if ( Aig_ObjLevel(pObj) > 3 ) pObj->fMarkA = 1; - Aig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachCo( pAig, pObj, i ) Aig_ObjFanin0(pObj)->fMarkA = 0; // collect nodes in the order vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); Aig_ManIncrementTravId( pAig ); Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); -// Aig_ManForEachPo( pAig, pObj, i ) +// Aig_ManForEachCo( pAig, pObj, i ) Saig_ManForEachLi( pAig, pObj, i ) { Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter ); } - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) if ( Llb_ObjBddVar(vOrder, pObj) < 0 ) Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); Aig_ManCleanMarkA( pAig ); @@ -232,7 +232,7 @@ Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 ); Saig_ManForEachLo( pAig, pObj, i ) Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 ); -// Aig_ManForEachPo( pAig, pObj, i ) +// Aig_ManForEachCo( pAig, pObj, i ) Saig_ManForEachLi( pAig, pObj, i ) Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 ); return vVars2Q; diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c index 6442d62e..31f94acf 100644 --- a/src/proof/llb/llb4Nonlin.c +++ b/src/proof/llb/llb4Nonlin.c @@ -81,7 +81,7 @@ DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vO Aig_ManCleanData( pAig ); // assign elementary variables Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); // compute internal nodes vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vPos), Saig_ManPoNum(pAig) ); @@ -171,7 +171,7 @@ Vec_Ptr_t * Llb_Nonlin4DerivePartitions( DdManager * dd, Aig_Man_t * pAig, Vec_I Aig_ManCleanData( pAig ); // assign elementary variables Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); Aig_ManForEachNode( pAig, pObj, i ) if ( Llb_ObjBddVar(vOrder, pObj) >= 0 ) @@ -248,7 +248,7 @@ Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig ) Aig_Obj_t * pObj; int i, Counter = 0; vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); Saig_ManForEachLi( pAig, pObj, i ) Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); @@ -364,7 +364,7 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) ); Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); Llb_Nonlin4CreateOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter ); } - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) if ( Llb_ObjBddVar(vOrder, pObj) < 0 ) { // if ( Saig_ObjIsLo(pAig, pObj) ) diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c index d13c366f..292fb176 100644 --- a/src/proof/llb/llb4Sweep.c +++ b/src/proof/llb/llb4Sweep.c @@ -92,12 +92,12 @@ Vec_Int_t * Llb_Nonlin4SweepOrder( Aig_Man_t * pAig, int * pCounter, int fSaveAl vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); Aig_ManIncrementTravId( pAig ); Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); - Aig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachCo( pAig, pObj, i ) { Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); Llb_Nonlin4SweepOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter, fSaveAll ); } - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) if ( Llb_ObjBddVar(vOrder, pObj) < 0 ) Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); // assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes @@ -127,7 +127,7 @@ int Llb4_Nonlin4SweepCutpoints( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nBddLi dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); // assign elementary variables Aig_ManCleanData( pAig ); - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachCi( pAig, pObj, i ) pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); // sweep internal nodes Aig_ManForEachNode( pAig, pObj, i ) diff --git a/src/proof/pdr/pdrClass.c b/src/proof/pdr/pdrClass.c index 4b28c196..cbe5e1c2 100644 --- a/src/proof/pdr/pdrClass.c +++ b/src/proof/pdr/pdrClass.c @@ -55,8 +55,8 @@ Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap ) // create CI mapping Aig_ManCleanData( pAig ); Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames); - Aig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi(pFrames); + Aig_ManForEachCi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreateCi(pFrames); Saig_ManForEachLo( pAig, pObj, i ) { iReg = Vec_IntEntry(vMap, i); @@ -69,8 +69,8 @@ Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap ) Aig_ManForEachNode( pAig, pObj, i ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); // add output nodes - Aig_ManForEachPo( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); + Aig_ManForEachCo( pAig, pObj, i ) + pObj->pData = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) ); // finish off Aig_ManCleanup( pFrames ); Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) ); diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c index 8ab99f83..5cdced62 100644 --- a/src/proof/ssw/sswAig.c +++ b/src/proof/ssw/sswAig.c @@ -120,13 +120,13 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, // add the constraint if ( fTwoPos ) { - Aig_ObjCreatePo( pFrames, pObjNew2 ); - Aig_ObjCreatePo( pFrames, pObjNew ); + Aig_ObjCreateCo( pFrames, pObjNew2 ); + Aig_ObjCreateCo( pFrames, pObjNew ); } else { pMiter = Aig_Exor( pFrames, pObjNew, pObjNew2 ); - Aig_ObjCreatePo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); + Aig_ObjCreateCo( pFrames, Aig_NotCond(pMiter, Aig_ObjPhaseReal(pMiter)) ); } } @@ -155,7 +155,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames ); // create latches for the first frame Saig_ManForEachLo( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); + Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) ); // add timeframes iLits = 0; for ( f = 0; f < p->pPars->nFramesK; f++ ) @@ -164,7 +164,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) { - pObjNew = Aig_ObjCreatePi(pFrames); + pObjNew = Aig_ObjCreateCi(pFrames); pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); } @@ -179,7 +179,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f, 1 ); } // transfer to the primary outputs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj,f) ); // transfer latch input to the latch outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) @@ -188,7 +188,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) assert( p->vInits == NULL || Vec_IntSize(p->vInits) == iLits + Saig_ManPiNum(p->pAig) ); // add the POs for the latch outputs of the last frame Saig_ManForEachLo( p->pAig, pObj, i ) - Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) ); + Aig_ObjCreateCo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) ); // remove dangling nodes Aig_ManCleanup( pFrames ); @@ -225,10 +225,10 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) // map constants and PIs Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); + Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) ); // create latches for the first frame Saig_ManForEachLo( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) ); + Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) ); // set the constraints on the latch outputs Saig_ManForEachLo( p->pAig, pObj, i ) Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, 0, 0 ); @@ -241,7 +241,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) } // add the POs for the latch outputs of the last frame Saig_ManForEachLi( p->pAig, pObj, i ) - Aig_ObjCreatePo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) ); + Aig_ObjCreateCo( pFrames, Ssw_ObjChild0Fra(p, pObj,0) ); // remove dangling nodes Aig_ManCleanup( pFrames ); Aig_ManSetRegNum( pFrames, Aig_ManRegNum(p->pAig) ); diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c index 8cb14f4a..0eabaa92 100644 --- a/src/proof/ssw/sswBmc.c +++ b/src/proof/ssw/sswBmc.c @@ -50,7 +50,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f ) if ( Aig_ObjIsConst1(pObj) ) pRes = Aig_ManConst1( pFrm->pFrames ); else if ( Saig_ObjIsPi(pFrm->pAig, pObj) ) - pRes = Aig_ObjCreatePi( pFrm->pFrames ); + pRes = Aig_ObjCreateCi( pFrm->pFrames ); else if ( Aig_ObjIsPo(pObj) ) { Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f ); diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index 239e35b9..6d8a152d 100644 --- a/src/proof/ssw/sswConstr.c +++ b/src/proof/ssw/sswConstr.c @@ -63,19 +63,19 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames ) // map constants and PIs Aig_ObjSetCopy( Aig_ManConst1(p), Aig_ManConst1(pFrames) ); Saig_ManForEachPi( p, pObj, i ) - Aig_ObjSetCopy( pObj, Aig_ObjCreatePi(pFrames) ); + Aig_ObjSetCopy( pObj, Aig_ObjCreateCi(pFrames) ); // add internal nodes of this frame Aig_ManForEachNode( p, pObj, i ) Aig_ObjSetCopy( pObj, Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ) ); // transfer to the primary output - Aig_ManForEachPo( p, pObj, i ) + Aig_ManForEachCo( p, pObj, i ) Aig_ObjSetCopy( pObj, Aig_ObjChild0Copy(pObj) ); // create constraint outputs Saig_ManForEachPo( p, pObj, i ) { if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) ) continue; - Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) ); + Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjCopy(pObj) ) ); } // transfer latch inputs to the latch outputs Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) @@ -125,10 +125,10 @@ int Ssw_ManSetConstrPhases( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) if ( RetValue == l_True && pvInits ) { *pvInits = Vec_IntAlloc( 1000 ); - Aig_ManForEachPi( pFrames, pObj, i ) + Aig_ManForEachCi( pFrames, pObj, i ) Vec_IntPush( *pvInits, sat_solver_var_value(pSat, pCnf->pVarNums[Aig_ObjId(pObj)]) ); -// Aig_ManForEachPi( pFrames, pObj, i ) +// Aig_ManForEachCi( pFrames, pObj, i ) // printf( "%d", Vec_IntEntry(*pvInits, i) ); // printf( "\n" ); } @@ -268,7 +268,7 @@ void Ssw_ManRefineByConstrSim( Ssw_Man_t * p ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); // assign the COs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); // check the outputs Saig_ManForEachPo( p->pAig, pObj, i ) @@ -424,7 +424,7 @@ clk = clock(); Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) { - pObjNew = Aig_ObjCreatePi(p->pFrames); + pObjNew = Aig_ObjCreateCi(p->pFrames); pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); } @@ -464,7 +464,7 @@ clk = clock(); if ( f == p->pPars->nFramesK - 1 ) break; // transfer latch input to the latch outputs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); // build logic cones for register outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) @@ -514,7 +514,7 @@ clk = clock(); Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) { - pObjNew = Aig_ObjCreatePi(p->pFrames); + pObjNew = Aig_ObjCreateCi(p->pFrames); pObjNew->fPhase = Vec_IntEntry( p->vInits, iLits++ ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); } @@ -544,7 +544,7 @@ clk = clock(); if ( f == p->pPars->nFramesK - 1 ) break; // transfer latch input to the latch outputs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); // build logic cones for register outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) @@ -648,7 +648,7 @@ clk = clock(); Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) { - pObjNew = Aig_ObjCreatePi(p->pFrames); + pObjNew = Aig_ObjCreateCi(p->pFrames); pObjNew->fPhase = (p->vInits != NULL) && Vec_IntEntry(p->vInits, iLits++); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); } diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c index d9a16e22..0f6002fa 100644 --- a/src/proof/ssw/sswDyn.c +++ b/src/proof/ssw/sswDyn.c @@ -215,7 +215,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) int i, f, nFrames; // transfer simulation information - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) { pObjFraig = Ssw_ObjFrame( p, pObj, 0 ); if ( pObjFraig == Aig_ManConst0(p->pFrames) ) @@ -385,7 +385,7 @@ clk = clock(); f = p->pPars->nFramesK; Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); Aig_ManSetPioNumbers( p->pFrames ); // label nodes corresponding to primary inputs Ssw_ManLabelPiNodes( p ); diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c index 4f6fb26e..536316ff 100644 --- a/src/proof/ssw/sswFilter.c +++ b/src/proof/ssw/sswFilter.c @@ -65,7 +65,7 @@ void Ssw_ManRefineByFilterSim( Ssw_Man_t * p, int nFrames ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); // assign the COs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); // transfer if ( f == 0 ) @@ -115,7 +115,7 @@ void Ssw_ManRollForward( Ssw_Man_t * p, int nFrames ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); // assign the COs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); } // record the new pattern @@ -157,7 +157,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); // assign the COs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); } assert( iBit == pCex->nBits ); @@ -317,7 +317,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit ) Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) { - pObjNew = Aig_ObjCreatePi(p->pFrames); + pObjNew = Aig_ObjCreateCi(p->pFrames); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); } // sweep internal nodes @@ -351,7 +351,7 @@ int Ssw_ManSweepBmcFilter( Ssw_Man_t * p, int TimeLimit ) if ( TimeLimit && ((float)TimeLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) ) break; // transfer latch input to the latch outputs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); // build logic cones for register outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c index ca95cf23..3173ec6f 100644 --- a/src/proof/ssw/sswIslands.c +++ b/src/proof/ssw/sswIslands.c @@ -90,7 +90,7 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs ) assert( pObj1->pData == pObj0 ); } // make sure the POs are not matched - Aig_ManForEachPo( p0, pObj0, i ) + Aig_ManForEachCo( p0, pObj0, i ) { pObj1 = Aig_ManPo( p1, i ); assert( pObj0->pData == NULL ); @@ -295,7 +295,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 ) { if ( pObj0->pData != NULL ) continue; - pObj1 = Aig_ObjCreatePi( p1 ); + pObj1 = Aig_ObjCreateCi( p1 ); pObj0->pData = pObj1; pObj1->pData = pObj0; Vec_PtrPush( vNewLis, pObj0Li ); @@ -311,7 +311,7 @@ void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 ) } // create register outputs in p0 that are absent in p1 Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i ) - Aig_ObjCreatePo( p1, Aig_ObjChild0Copy(pObj0Li) ); + Aig_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) ); // increment the number of registers Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) ); Vec_PtrFree( vNewLis ); diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c index ce9c2563..c41a74ef 100644 --- a/src/proof/ssw/sswLcorr.c +++ b/src/proof/ssw/sswLcorr.c @@ -49,7 +49,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p ) unsigned * pInfo; int i; // transfer simulation information - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) { pObjFraig = Ssw_ObjFrame( p, pObj, 0 ); if ( pObjFraig == Aig_ManConst0(p->pFrames) ) @@ -245,7 +245,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) // map constants and PIs Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(p->pFrames) ); // implement equivalence classes Saig_ManForEachLo( p->pAig, pObj, i ) @@ -253,7 +253,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) pRepr = Aig_ObjRepr( p->pAig, pObj ); if ( pRepr == NULL ) { - pTemp = Aig_ObjCreatePi(p->pFrames); + pTemp = Aig_ObjCreateCi(p->pFrames); pTemp->pData = pObj; } else diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 25a80be7..6e36ae12 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -587,7 +587,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f Aig_ManIncrementTravId( p->pAig ); // check comb inputs if ( fUpdate ) - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) { pRepr = Aig_ObjRepr(p->pAig, pObj); if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) ) @@ -631,7 +631,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f } } // transfer to POs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) { pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) ); pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) ); @@ -826,7 +826,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); // assign the COs - Aig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachCo( pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); } assert( iBit == pCex->nBits ); diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c index ac22b0d5..dce7ac3e 100644 --- a/src/proof/ssw/sswRarity2.c +++ b/src/proof/ssw/sswRarity2.c @@ -277,7 +277,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ) & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) ); // assign the COs - Aig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachCo( pAig, pObj, i ) pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) ); } assert( iBit == pCex->nBits ); diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c index ec50ab50..a04f6f54 100644 --- a/src/proof/ssw/sswSemi.c +++ b/src/proof/ssw/sswSemi.c @@ -198,7 +198,7 @@ clk = clock(); // map constants and PIs Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c index 9ce89a71..946224cd 100644 --- a/src/proof/ssw/sswSim.c +++ b/src/proof/ssw/sswSim.c @@ -458,7 +458,7 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo ) BestPat = i * 32 + k; // fill in the counter-example data pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pAig)+1 ); - Aig_ManForEachPi( p->pAig, pObjPi, i ) + Aig_ManForEachCi( p->pAig, pObjPi, i ) { pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat); // printf( "%d", pModel[i] ); @@ -486,7 +486,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p ) // make sure the reference simulation pattern does not detect the bug pObj = Aig_ManPo( p->pAig, 0 ); assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) { if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) ) { @@ -628,7 +628,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) if ( p->nFrames == 1 ) { // copy the PI info - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 ); // flip one bit Limit = Abc_MinInt( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); @@ -678,7 +678,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ) assert( p->nFrames > 0 ); // copy the pattern into the primary inputs - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 ); // set distance one PIs for the first frame @@ -909,7 +909,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit ) } else { - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) Ssw_SmlAssignRandom( p, pObj ); } } diff --git a/src/proof/ssw/sswSimSat.c b/src/proof/ssw/sswSimSat.c index 4c094a2d..098b1e0f 100644 --- a/src/proof/ssw/sswSimSat.c +++ b/src/proof/ssw/sswSimSat.c @@ -48,7 +48,7 @@ void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr ) int i, RetValue1, RetValue2, clk = clock(); // set the PI simulation information Aig_ManConst1(p->pAig)->fMarkB = 1; - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) pObj->fMarkB = Abc_InfoHasBit( p->pPatWords, i ); // simulate internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index e2a4f65d..a3a8d1c8 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -117,7 +117,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f ) Aig_Obj_t * pObj; int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) ) Abc_InfoSetBit( p->pPatWords, i ); } @@ -138,7 +138,7 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f ) Aig_Obj_t * pObj; int i; memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords ); - Aig_ManForEachPi( p->pAig, pObj, i ) + Aig_ManForEachCi( p->pAig, pObj, i ) if ( Ssw_ManGetSatVarValue( p, pObj, f ) ) Abc_InfoSetBit( p->pPatWords, i ); } @@ -284,7 +284,7 @@ clk = clock(); // map constants and PIs Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { @@ -298,7 +298,7 @@ clk = clock(); if ( f == p->pPars->nFramesK - 1 ) break; // transfer latch input to the latch outputs - Aig_ManForEachPo( p->pAig, pObj, i ) + Aig_ManForEachCo( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Ssw_ObjChild0Fra(p, pObj, f) ); // build logic cones for register outputs Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i ) @@ -393,7 +393,7 @@ clk = clock(); f = p->pPars->nFramesK; Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) - Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) ); + Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); p->timeReduce += clock() - clk; // sweep internal nodes |