From aa705a9af63b3c3859345311693eb50fbf751cb7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 2 Oct 2012 20:20:46 -0700 Subject: Renamed reference counting APIs in GIA package. --- src/aig/gia/gia.h | 28 ++++++++++------------------ src/aig/gia/giaCSat.c | 6 +++--- src/aig/gia/giaCSatOld.c | 6 +++--- src/aig/gia/giaCTas.c | 6 +++--- src/aig/gia/giaChoice.c | 2 +- src/aig/gia/giaCof.c | 6 +++--- src/aig/gia/giaDup.c | 8 ++++---- src/aig/gia/giaEmbed.c | 22 +++++++++++----------- src/aig/gia/giaEnable.c | 2 +- src/aig/gia/giaForce.c | 22 +++++++++++----------- src/aig/gia/giaFront.c | 2 +- src/aig/gia/giaIf.c | 4 ++-- src/aig/gia/giaMan.c | 2 +- src/aig/gia/giaSat.c | 2 +- src/aig/gia/giaSwitch.c | 8 ++++---- src/aig/gia/giaUtil.c | 10 +++++----- src/base/cmd/cmdPlugin.c | 2 +- src/opt/nwk/nwkAig.c | 8 ++++---- src/proof/abs/absRpm.c | 20 ++++++++++---------- src/proof/cec/cecClass.c | 4 ++-- src/proof/cec/cecCorr.c | 4 ++-- src/proof/cec/cecSeq.c | 2 +- src/proof/cec/cecSweep.c | 2 +- 23 files changed, 85 insertions(+), 93 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index fd47d2c7..b3efa455 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -109,7 +109,6 @@ struct Gia_Man_t_ int nHTable; // hash table size int fAddStrash; // performs additional structural hashing int * pRefs; // the reference count - int * pNodeRefs; // node references Vec_Int_t * vLevels; // levels of the nodes int nLevels; // the mamixum level int nConstrs; // the number of constraints @@ -368,21 +367,14 @@ static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) static inline int Gia_ObjNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (int)(unsigned char)Vec_StrGetEntry(p->vTtNums, Gia_ObjId(p,pObj)); } static inline void Gia_ObjSetNum( Gia_Man_t * p, Gia_Obj_t * pObj, int n ) { assert( n >= 0 && n < 254 ); Vec_StrSetEntry(p->vTtNums, Gia_ObjId(p,pObj), (char)n); } -static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; } -static inline int Gia_ObjRefsId( Gia_Man_t * p, int Id ) { assert( p->pRefs); return p->pRefs[Id]; } -static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++; } -static inline int Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)]; } -static inline void Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj)); } -static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj)); } -static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); } -static inline void Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj)); } - -static inline int Gia_ObjNodeRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pNodeRefs); return p->pNodeRefs[Gia_ObjId(p, pObj)]; } -static inline int Gia_ObjNodeRefsId( Gia_Man_t * p, int Id ) { assert( p->pNodeRefs); return p->pNodeRefs[Id]; } -static inline int Gia_ObjNodeRefIncId( Gia_Man_t * p, int Id ) { assert( p->pNodeRefs); return p->pNodeRefs[Id]++; } -static inline int Gia_ObjNodeRefDecId( Gia_Man_t * p, int Id ) { assert( p->pNodeRefs); return --p->pNodeRefs[Id]; } -static inline int Gia_ObjNodeRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pNodeRefs); return p->pNodeRefs[Gia_ObjId(p, pObj)]++; } -static inline int Gia_ObjNodeRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pNodeRefs); return --p->pNodeRefs[Gia_ObjId(p, pObj)]; } +static inline int Gia_ObjRefNumId( Gia_Man_t * p, int Id ) { assert(p->pRefs); return p->pRefs[Id]; } +static inline int Gia_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; } +static inline int Gia_ObjRefInc( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]++; } +static inline int Gia_ObjRefDec( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(p->pRefs); return --p->pRefs[Gia_ObjId(p, pObj)]; } +static inline void Gia_ObjRefFanin0Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert(p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin0(pObj)); } +static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ assert(p->pRefs); Gia_ObjRefInc(p, Gia_ObjFanin1(pObj)); } +static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert(p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); } +static inline void Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert(p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj)); } static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; } static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; } @@ -911,9 +903,9 @@ extern void Gia_ManSetPhase( Gia_Man_t * p ); extern void Gia_ManSetPhase1( Gia_Man_t * p ); extern void Gia_ManCleanPhase( Gia_Man_t * p ); extern int Gia_ManLevelNum( Gia_Man_t * p ); -extern void Gia_ManSetRefs( Gia_Man_t * p ); -extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p ); +extern void Gia_ManCreateValueRefs( Gia_Man_t * p ); extern void Gia_ManCreateRefs( Gia_Man_t * p ); +extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p ); extern int Gia_ManCrossCut( Gia_Man_t * p ); extern int Gia_ManIsNormalized( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManCollectPoIds( Gia_Man_t * p ); diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index b4bc5b3e..6d7df6b5 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -375,8 +375,8 @@ static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj ) int Count0, Count1; assert( !Gia_IsComplement(pObj) ); assert( Gia_ObjIsAnd(pObj) ); - Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) ); - Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) ); + Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) ); + Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) ); return Abc_MaxInt( Count0, Count1 ); } @@ -888,7 +888,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level ) else assert( 0 ); assert( Cbs_VarIsJust( pVar ) ); // chose decision variable using fanout count - if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) ) + if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) ) pDecVar = Gia_Not(Gia_ObjChild0(pVar)); else pDecVar = Gia_Not(Gia_ObjChild1(pVar)); diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c index 1dd4a425..75b4c3e0 100644 --- a/src/aig/gia/giaCSatOld.c +++ b/src/aig/gia/giaCSatOld.c @@ -330,8 +330,8 @@ static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj ) int Count0, Count1; assert( !Gia_IsComplement(pObj) ); assert( Gia_ObjIsAnd(pObj) ); - Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) ); - Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) ); + Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) ); + Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) ); return Abc_MaxInt( Count0, Count1 ); } @@ -612,7 +612,7 @@ int Cbs0_ManSolve_rec( Cbs0_Man_t * p ) else assert( 0 ); assert( Cbs0_VarIsJust( pVar ) ); // chose decision variable using fanout count - if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) ) + if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) ) pDecVar = Gia_Not(Gia_ObjChild0(pVar)); else pDecVar = Gia_Not(Gia_ObjChild1(pVar)); diff --git a/src/aig/gia/giaCTas.c b/src/aig/gia/giaCTas.c index 6dd0e0fa..79b42c66 100644 --- a/src/aig/gia/giaCTas.c +++ b/src/aig/gia/giaCTas.c @@ -441,8 +441,8 @@ static inline int Tas_VarFaninFanoutMax( Tas_Man_t * p, Gia_Obj_t * pObj ) int Count0, Count1; assert( !Gia_IsComplement(pObj) ); assert( Gia_ObjIsAnd(pObj) ); - Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) ); - Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) ); + Count0 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin0(pObj) ); + Count1 = Gia_ObjRefNum( p->pAig, Gia_ObjFanin1(pObj) ); return Abc_MaxInt( Count0, Count1 ); } @@ -1321,7 +1321,7 @@ int Tas_ManSolve_rec( Tas_Man_t * p, int Level ) if ( pVar != NULL ) { assert( Tas_VarIsJust( pVar ) ); - if ( Gia_ObjRefs(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefs(p->pAig, Gia_ObjFanin1(pVar)) ) + if ( Gia_ObjRefNum(p->pAig, Gia_ObjFanin0(pVar)) > Gia_ObjRefNum(p->pAig, Gia_ObjFanin1(pVar)) ) pDecVar = Gia_Not(Gia_ObjChild0(pVar)); else pDecVar = Gia_Not(Gia_ObjChild1(pVar)); diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c index a1d9e325..f5619028 100644 --- a/src/aig/gia/giaChoice.c +++ b/src/aig/gia/giaChoice.c @@ -228,7 +228,7 @@ int Gia_ManHasChoices( Gia_Man_t * p ) Gia_ManCreateRefs( p ); Gia_ManForEachAnd( p, pObj, i ) { - if ( Gia_ObjRefs(p, pObj) == 0 ) + if ( Gia_ObjRefNum(p, pObj) == 0 ) { if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL ) nFailNoRepr++; diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c index d41b6723..e9fd6c8b 100644 --- a/src/aig/gia/giaCof.c +++ b/src/aig/gia/giaCof.c @@ -143,7 +143,7 @@ Cof_Man_t * Cof_ManCreateLogicSimple( Gia_Man_t * pGia ) pObj->Value = iHandle; pObjLog = Cof_ManObj( p, iHandle ); pObjLog->nFanins = 0; - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); pObjLog->Id = i; pObjLog->Value = 0; if ( Gia_ObjIsAnd(pObj) ) @@ -811,7 +811,7 @@ Vec_Int_t * Gia_ManCofVars( Gia_Man_t * p, int nFanLim ) Gia_ManCreateRefs( p ); vVars = Vec_IntAlloc( 100 ); Gia_ManForEachObj( p, pObj, i ) - if ( Gia_ObjIsCand(pObj) && Gia_ObjRefs(p, pObj) >= nFanLim ) + if ( Gia_ObjIsCand(pObj) && Gia_ObjRefNum(p, pObj) >= nFanLim ) Vec_IntPush( vVars, i ); ABC_FREE( p->pRefs ); return vVars; @@ -877,7 +877,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose Vec_IntSort( vSigsNew, 0 ); iVar = Vec_IntPop( vSigsNew ); // Gia_ManCreateRefs( pAig ); -// printf( "ref count = %d\n", Gia_ObjRefs( pAig, Gia_ManObj(pAig, iVar) ) ); +// printf( "ref count = %d\n", Gia_ObjRefNum( pAig, Gia_ManObj(pAig, iVar) ) ); // ABC_FREE( pAig->pRefs ); pCof = Gia_ManDupCofInt( pAig, iVar ); pNew = Gia_ManCleanup( pCof ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index d598b511..e49ce616 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1061,7 +1061,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fD // check if there are PIs to be added Gia_ManCreateRefs( p ); Gia_ManForEachPi( p, pObj, i ) - if ( !fTrimCis || Gia_ObjRefs(p, pObj) ) + if ( !fTrimCis || Gia_ObjRefNum(p, pObj) ) break; if ( i == Gia_ManPiNum(p) ) // there is no PIs - add dummy PI Gia_ManAppendCi(pNew); @@ -1069,7 +1069,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fD Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) - if ( !fTrimCis || Gia_ObjRefs(p, pObj) || Gia_ObjIsRo(p, pObj) ) + if ( !fTrimCis || Gia_ObjRefNum(p, pObj) || Gia_ObjIsRo(p, pObj) ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManForEachAnd( p, pObj, i ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); @@ -1142,7 +1142,7 @@ Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p ) Gia_ObjRefFanin0Dec( p, pObj ); // check if PIs are left Gia_ManForEachPi( p, pObj, i ) - if ( Gia_ObjRefs(p, pObj) ) + if ( Gia_ObjRefNum(p, pObj) ) break; if ( i == Gia_ManPiNum(p) ) // there is no PIs - add dummy PI Gia_ManAppendCi(pNew); @@ -1150,7 +1150,7 @@ Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p ) Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) - if ( Gia_ObjRefs(p, pObj) || Gia_ObjIsRo(p, pObj) ) + if ( Gia_ObjRefNum(p, pObj) || Gia_ObjIsRo(p, pObj) ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManForEachAnd( p, pObj, i ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c index 17f80707..b6c4655e 100644 --- a/src/aig/gia/giaEmbed.c +++ b/src/aig/gia/giaEmbed.c @@ -190,7 +190,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia ) pObjLog = Emb_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = Gia_ManCoNum(pGia); //0; - pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, Gia_ManConst0(pGia) ); // count objects hHandle += Emb_ObjSize( pObjLog ); nNodes = 1; @@ -204,7 +204,7 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia ) pObjLog = Emb_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = Gia_ObjIsRo( pGia, pObj ); - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); pObjLog->fCi = 1; // count objects hHandle += Emb_ObjSize( pObjLog ); @@ -213,13 +213,13 @@ Emb_Man_t * Emb_ManStartSimple( Gia_Man_t * pGia ) // create internal nodes Gia_ManForEachAnd( pGia, pObj, i ) { - assert( Gia_ObjRefs( pGia, pObj ) > 0 ); + assert( Gia_ObjRefNum( pGia, pObj ) > 0 ); // create node object pObj->Value = hHandle; pObjLog = Emb_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = 2; - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); // add fanins pFanLog = Emb_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); Emb_ObjAddFanin( pObjLog, pFanLog ); @@ -364,7 +364,7 @@ void Emb_ManCreateRefsSpecial( Gia_Man_t * p ) Gia_ObjRefDec( p, Gia_Regular(pObjD0) ); } Gia_ManForEachAnd( p, pObj, i ) - assert( Gia_ObjRefs(p, pObj) > 0 ); + assert( Gia_ObjRefNum(p, pObj) > 0 ); Gia_ManCleanMark0( p ); } @@ -394,7 +394,7 @@ void Emb_ManTransformRefs( Gia_Man_t * p, int * pnObjs, int * pnFanios ) pObj->fMark0 = 1; // mark those nodes that have ref count more than 1 Gia_ManForEachAnd( p, pObj, i ) - pObj->fMark0 = (Gia_ObjRefs(p, pObj) > 1); + pObj->fMark0 = (Gia_ObjRefNum(p, pObj) > 1); // mark the output drivers Gia_ManForEachCoDriver( p, pObj, i ) pObj->fMark0 = 1; @@ -516,7 +516,7 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia ) pObjLog = Emb_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = Gia_ManCoNum(pGia); //0; - pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, Gia_ManConst0(pGia) ); // count objects hHandle += Emb_ObjSize( pObjLog ); nNodes++; @@ -530,7 +530,7 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia ) pObjLog = Emb_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = Gia_ObjIsRo( pGia, pObj ); - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); pObjLog->fCi = 1; // count objects hHandle += Emb_ObjSize( pObjLog ); @@ -543,17 +543,17 @@ Emb_Man_t * Emb_ManStart( Gia_Man_t * pGia ) { if ( pObj->fMark0 == 0 ) { - assert( Gia_ObjRefs( pGia, pObj ) == 0 ); + assert( Gia_ObjRefNum( pGia, pObj ) == 0 ); continue; } - assert( Gia_ObjRefs( pGia, pObj ) > 0 ); + assert( Gia_ObjRefNum( pGia, pObj ) > 0 ); Emb_ManCollectSuper( pGia, pObj, vSuper, vVisit ); // create node object pObj->Value = hHandle; pObjLog = Emb_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = Vec_IntSize( vSuper ); - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); // add fanins Gia_ManForEachObjVec( vSuper, pGia, pFanin, k ) { diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c index f2fbd123..9cb0dce5 100644 --- a/src/aig/gia/giaEnable.c +++ b/src/aig/gia/giaEnable.c @@ -110,7 +110,7 @@ void Gia_ManPrintSignals( Gia_Man_t * p, int * pFreq, char * pStr ) if ( pFreq[i] > 10 ) { printf( "%3d : Obj = %6d Refs = %6d Freq = %6d\n", - ++Counter, i, Gia_ObjRefs(p, Gia_ManObj(p,i)), pFreq[i] ); + ++Counter, i, Gia_ObjRefNum(p, Gia_ManObj(p,i)), pFreq[i] ); Vec_IntPush( vObjs, i ); } Vec_IntFree( vObjs ); diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c index a32e71b4..d37fa455 100644 --- a/src/aig/gia/giaForce.c +++ b/src/aig/gia/giaForce.c @@ -168,7 +168,7 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia ) pObjLog = Frc_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = 0; - pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, Gia_ManConst0(pGia) ); // count objects hHandle += Frc_ObjSize( pObjLog ); nNodes = 1; @@ -182,7 +182,7 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia ) pObjLog = Frc_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = 0; - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); pObjLog->fCi = 0; // count objects hHandle += Frc_ObjSize( pObjLog ); @@ -191,13 +191,13 @@ Frc_Man_t * Frc_ManStartSimple( Gia_Man_t * pGia ) // create internal nodes Gia_ManForEachAnd( pGia, pObj, i ) { - assert( Gia_ObjRefs( pGia, pObj ) > 0 ); + assert( Gia_ObjRefNum( pGia, pObj ) > 0 ); // create node object pObj->Value = hHandle; pObjLog = Frc_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = 2; - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); // add fanins pFanLog = Frc_ManObj( p, Gia_ObjValue(Gia_ObjFanin0(pObj)) ); Frc_ObjAddFanin( pObjLog, pFanLog ); @@ -341,7 +341,7 @@ void Frc_ManCreateRefsSpecial( Gia_Man_t * p ) Gia_ObjRefDec( p, Gia_Regular(pObjD0) ); } Gia_ManForEachAnd( p, pObj, i ) - assert( Gia_ObjRefs(p, pObj) > 0 ); + assert( Gia_ObjRefNum(p, pObj) > 0 ); Gia_ManCleanMark0( p ); } @@ -371,7 +371,7 @@ void Frc_ManTransformRefs( Gia_Man_t * p, int * pnObjs, int * pnFanios ) pObj->fMark0 = 1; // mark those nodes that have ref count more than 1 Gia_ManForEachAnd( p, pObj, i ) - pObj->fMark0 = (Gia_ObjRefs(p, pObj) > 1); + pObj->fMark0 = (Gia_ObjRefNum(p, pObj) > 1); // mark the output drivers Gia_ManForEachCoDriver( p, pObj, i ) pObj->fMark0 = 1; @@ -451,7 +451,7 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia ) pObjLog = Frc_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = 0; - pObjLog->nFanouts = Gia_ObjRefs( pGia, Gia_ManConst0(pGia) ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, Gia_ManConst0(pGia) ); // count objects hHandle += Frc_ObjSize( pObjLog ); nNodes++; @@ -465,7 +465,7 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia ) pObjLog = Frc_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = 0; - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); pObjLog->fCi = 1; // count objects hHandle += Frc_ObjSize( pObjLog ); @@ -478,17 +478,17 @@ Frc_Man_t * Frc_ManStart( Gia_Man_t * pGia ) { if ( pObj->fMark0 == 0 ) { - assert( Gia_ObjRefs( pGia, pObj ) == 0 ); + assert( Gia_ObjRefNum( pGia, pObj ) == 0 ); continue; } - assert( Gia_ObjRefs( pGia, pObj ) > 0 ); + assert( Gia_ObjRefNum( pGia, pObj ) > 0 ); Frc_ManCollectSuper( pGia, pObj, vSuper, vVisit ); // create node object pObj->Value = hHandle; pObjLog = Frc_ManObj( p, hHandle ); pObjLog->hHandle = hHandle; pObjLog->nFanins = Vec_IntSize( vSuper ); - pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj ); + pObjLog->nFanouts = Gia_ObjRefNum( pGia, pObj ); // add fanins Gia_ManForEachObjVec( vSuper, pGia, pFanin, k ) { diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c index 08fd6081..322da785 100644 --- a/src/aig/gia/giaFront.c +++ b/src/aig/gia/giaFront.c @@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p ) int nCrossCutMaxInit = Gia_ManCrossCut( p ); int iFront = 0;//, clk = clock(); // set references for all objects - Gia_ManSetRefs( p ); + Gia_ManCreateValueRefs( p ); // start the new manager pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 3fc5c04e..13e4f429 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -153,7 +153,7 @@ If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf ) // set up the choice node /* // if ( p->pReprs && p->pNexts && Gia_ObjIsHead( p, i ) ) - if ( p->pNexts && Gia_ObjNext(p, i) && Gia_ObjRefsId(p, i) ) + if ( p->pNexts && Gia_ObjNext(p, i) && Gia_ObjRefNumId(p, i) ) { int iPrev, iFanin; pIfMan->nChoices++; @@ -509,7 +509,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p ) Gia_LutForEachFanin( p, i, iFan, k ) { Counter += (pLutClass[iFan] == 109); - Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefsId(p, iFan) == 1); + Counter2 += (pLutClass[iFan] == 109) && (Gia_ObjRefNumId(p, iFan) == 1); } OtherClasses += (Counter > 1); OtherClasses2 += (Counter2 > 1); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index e7b831bd..f78ea847 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -108,7 +108,7 @@ void Gia_ManStop( Gia_Man_t * p ) ABC_FREE( p->pReprs ); ABC_FREE( p->pNexts ); ABC_FREE( p->pRefs ); - ABC_FREE( p->pNodeRefs ); +// ABC_FREE( p->pNodeRefs ); ABC_FREE( p->pHTable ); ABC_FREE( p->pObjs ); ABC_FREE( p->pSpec ); diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c index 4f8a6acb..9bea8ef7 100644 --- a/src/aig/gia/giaSat.c +++ b/src/aig/gia/giaSat.c @@ -358,7 +358,7 @@ void Gia_ManSatExperiment( Gia_Man_t * p ) int nWords = 0, nWords2 = 0; pMan = Gia_ManSatStart(); // mark the nodes to become roots of leaf-DAGs - Gia_ManSetRefs( p ); + Gia_ManCreateValueRefs( p ); Gia_ManForEachObj( p, pObj, i ) { pObj->fMark0 = 0; diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c index 63c1ff9f..8bf027a4 100644 --- a/src/aig/gia/giaSwitch.c +++ b/src/aig/gia/giaSwitch.c @@ -720,7 +720,7 @@ float Gia_ManEvaluateSwitching( Gia_Man_t * p ) ABC_FREE( p->pRefs ); Gia_ManCreateRefs( p ); Gia_ManForEachObj( p, pObj, i ) - SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255; + SwitchTotal += (float)Gia_ObjRefNum(p, pObj) * p->pSwitching[i] / 255; return SwitchTotal; } @@ -777,9 +777,9 @@ float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbO pObjDfs = Gia_ObjFromLit( pDfs, pObj->Value ); Switch = pSwitching[ Gia_ObjId(pDfs, pObjDfs) ]; p->pSwitching[i] = (char)((Switch >= 1.0) ? 255 : (int)((0.002 + Switch) * 255)); // 0.00196 = (1/255)/2 - SwitchTotal += (float)Gia_ObjRefs(p, pObj) * p->pSwitching[i] / 255; -// SwitchTotal2 += Gia_ObjRefs(p, pObj) * Switch; -// printf( "%d = %.2f\n", i, Gia_ObjRefs(p, pObj) * Switch ); + SwitchTotal += (float)Gia_ObjRefNum(p, pObj) * p->pSwitching[i] / 255; +// SwitchTotal2 += Gia_ObjRefNum(p, pObj) * Switch; +// printf( "%d = %.2f\n", i, Gia_ObjRefNum(p, pObj) * Switch ); } // printf( "\nSwitch float = %f. Switch char = %f.\n", SwitchTotal2, SwitchTotal ); Vec_IntFree( vSwitching ); diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 2898488f..da713aa0 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -465,7 +465,7 @@ int Gia_ManLevelNum( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManSetRefs( Gia_Man_t * p ) +void Gia_ManCreateValueRefs( Gia_Man_t * p ) { Gia_Obj_t * pObj; int i; @@ -554,7 +554,7 @@ int Gia_ManCrossCut( Gia_Man_t * p ) { Gia_Obj_t * pObj; int i, nCutCur = 0, nCutMax = 0; - Gia_ManSetRefs( p ); + Gia_ManCreateValueRefs( p ); Gia_ManForEachObj( p, pObj, i ) { if ( pObj->Value ) @@ -810,11 +810,11 @@ int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode ) return 0; assert( Gia_ObjIsAnd(pNode) ); pFanin = Gia_ObjFanin0(pNode); - assert( Gia_ObjRefs(p, pFanin) > 0 ); + assert( Gia_ObjRefNum(p, pFanin) > 0 ); if ( Gia_ObjRefDec(p, pFanin) == 0 ) Counter += Gia_NodeDeref_rec( p, pFanin ); pFanin = Gia_ObjFanin1(pNode); - assert( Gia_ObjRefs(p, pFanin) > 0 ); + assert( Gia_ObjRefNum(p, pFanin) > 0 ); if ( Gia_ObjRefDec(p, pFanin) == 0 ) Counter += Gia_NodeDeref_rec( p, pFanin ); return Counter + 1; @@ -1027,7 +1027,7 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj ) Gia_ObjFaninId0p(p, pObj), (Gia_ObjFaninC0(pObj)? "\'" : " "), Gia_ObjFaninId1p(p, pObj), (Gia_ObjFaninC1(pObj)? "\'" : " ") ); if ( p->pRefs ) - printf( " (refs = %3d)", Gia_ObjRefs(p, pObj) ); + printf( " (refs = %3d)", Gia_ObjRefNum(p, pObj) ); printf( "\n" ); /* if ( p->pRefs ) diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c index 93eee5b8..b89238fc 100644 --- a/src/base/cmd/cmdPlugin.c +++ b/src/base/cmd/cmdPlugin.c @@ -301,7 +301,7 @@ Vec_Int_t * Abc_ManExpandCex( Gia_Man_t * pGia, Vec_Int_t * vCex ) { Gia_ManForEachPi( pGia, pObj, i ) { - if ( Gia_ObjRefs(pGia, pObj) == 0 ) + if ( Gia_ObjRefNum(pGia, pObj) == 0 ) Vec_IntPush( vCexNew, 0 ); else { diff --git a/src/opt/nwk/nwkAig.c b/src/opt/nwk/nwkAig.c index 5b0aaf20..b70c71fc 100644 --- a/src/opt/nwk/nwkAig.c +++ b/src/opt/nwk/nwkAig.c @@ -165,12 +165,12 @@ Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t * ppCopies = ABC_ALLOC( Nwk_Obj_t *, Gia_ManObjNum(p) ); // copy objects pObj = Gia_ManConst0(p); -// ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefs(p,pObj) ); - ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefs(p,pObj) + (Vec_IntSize(vLeaves) > Vec_IntSize(vPPis) ? Vec_IntSize(vLeaves) - Vec_IntSize(vPPis) : 0) ); +// ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefNum(p,pObj) ); + ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefNum(p,pObj) + (Vec_IntSize(vLeaves) > Vec_IntSize(vPPis) ? Vec_IntSize(vLeaves) - Vec_IntSize(vPPis) : 0) ); Vec_IntPush( vMaps, Gia_ObjId(p,pObj) ); Gia_ManForEachObjVec( vLeaves, p, pObj, i ) { - ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) ); + ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateCi( pNtk, Gia_ObjRefNum(p,pObj) ); assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) ); Vec_IntPush( vMaps, Gia_ObjId(p,pObj) ); } @@ -181,7 +181,7 @@ Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t * } Gia_ManForEachObjVec( vNodes, p, pObj, i ) { - ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 2, Gia_ObjRefs(p,pObj) ); + ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 2, Gia_ObjRefNum(p,pObj) ); Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId0p(p,pObj)] ); Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId1p(p,pObj)] ); assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) ); diff --git a/src/proof/abs/absRpm.c b/src/proof/abs/absRpm.c index b0dc1665..3d5b2ac3 100644 --- a/src/proof/abs/absRpm.c +++ b/src/proof/abs/absRpm.c @@ -93,7 +93,7 @@ void Gia_ManComputeDoms( Gia_Man_t * p ) { if ( i == 0 || Gia_ObjIsCi(pObj) ) continue; - if ( pObj->fMark1 || (p->pRefs && Gia_ObjIsAnd(pObj) && Gia_ObjRefs(p, pObj) == 0) ) + if ( pObj->fMark1 || (p->pRefs && Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p, pObj) == 0) ) continue; if ( Gia_ObjIsCo(pObj) ) { @@ -173,7 +173,7 @@ Vec_Int_t * Gia_ManCollectDoms( Gia_Man_t * p ) { if ( !pObj->fMark1 ) continue; - if ( p->pRefs && Gia_ObjRefs(p, pObj) == 0 ) + if ( p->pRefs && Gia_ObjRefNum(p, pObj) == 0 ) continue; iDom = Gia_ObjDom(p, pObj); if ( iDom == -1 ) @@ -238,7 +238,7 @@ void Gia_ManCountFanoutlessFlops( Gia_Man_t * p ) int Counter = 0; Gia_ManCreateRefs( p ); Gia_ManForEachRo( p, pObj, i ) - if ( Gia_ObjRefs(p, pObj) == 0 ) + if ( Gia_ObjRefNum(p, pObj) == 0 ) Counter++; printf( "Fanoutless flops = %d.\n", Counter ); ABC_FREE( p->pRefs ); @@ -305,11 +305,11 @@ int Abs_GiaObjDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode ) return 0; assert( Gia_ObjIsAnd(pNode) ); pFanin = Gia_ObjFanin0(pNode); - assert( Gia_ObjRefs(p, pFanin) > 0 ); + assert( Gia_ObjRefNum(p, pFanin) > 0 ); if ( Gia_ObjRefDec(p, pFanin) == 0 ) Counter += Abs_GiaObjDeref_rec( p, pFanin ); pFanin = Gia_ObjFanin1(pNode); - assert( Gia_ObjRefs(p, pFanin) > 0 ); + assert( Gia_ObjRefNum(p, pFanin) > 0 ); if ( Gia_ObjRefDec(p, pFanin) == 0 ) Counter += Abs_GiaObjDeref_rec( p, pFanin ); return Counter + 1; @@ -347,14 +347,14 @@ int Abs_GiaSortNodes( Gia_Man_t * p, Vec_Int_t * vSupp ) int nSize = Vec_IntSize(vSupp); int i, RetValue; Gia_ManForEachObjVec( vSupp, p, pObj, i ) - if ( i < nSize && Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves + if ( i < nSize && Gia_ObjRefNum(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj) ) // add removable leaves { assert( pObj->fMark1 ); Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); } RetValue = Vec_IntSize(vSupp) - nSize; Gia_ManForEachObjVec( vSupp, p, pObj, i ) - if ( i < nSize && !(Gia_ObjRefs(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj)) ) // add non-removable leaves + if ( i < nSize && !(Gia_ObjRefNum(p, pObj) == 0 && !Gia_ObjIsRo(p, pObj)) ) // add non-removable leaves Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); assert( Vec_IntSize(vSupp) == 2 * nSize ); memmove( Vec_IntArray(vSupp), Vec_IntArray(vSupp) + nSize, sizeof(int) * nSize ); @@ -413,7 +413,7 @@ void Abs_ManSupport2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) if ( Gia_ObjIsTravIdCurrent(p, pObj) ) return; Gia_ObjSetTravIdCurrent(p, pObj); - if ( pObj->fMark1 || Gia_ObjIsRo(p, pObj) || Gia_ObjRefs(p, pObj) > 0 ) + if ( pObj->fMark1 || Gia_ObjIsRo(p, pObj) || Gia_ObjRefNum(p, pObj) > 0 ) { Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); return; @@ -464,7 +464,7 @@ int Abs_ManSupport3( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp ) if ( !Gia_ObjIsAnd(pTemp) ) continue; assert( !pTemp->fMark1 ); - assert( Gia_ObjRefs(p, pTemp) > 0 ); + assert( Gia_ObjRefNum(p, pTemp) > 0 ); pFan0 = Gia_ObjFanin0(pTemp); pFan1 = Gia_ObjFanin1(pTemp); if ( Gia_ObjIsTravIdCurrent(p, pFan0) && Gia_ObjIsTravIdCurrent(p, pFan1) ) @@ -630,7 +630,7 @@ void Abs_RpmPerformMark( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerb Gia_ManForEachObjVec( vDoms, p, pObj, i ) { assert( !pObj->fMark1 ); - assert( Gia_ObjRefs( p, pObj ) > 0 ); + assert( Gia_ObjRefNum( p, pObj ) > 0 ); // dereference root node nNodes = Abs_GiaObjDeref_rec( p, pObj ); /* diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c index 46e585a9..2d820c39 100644 --- a/src/proof/cec/cecClass.c +++ b/src/proof/cec/cecClass.c @@ -857,7 +857,7 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ) p->pAig->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p->pAig) ); p->pAig->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p->pAig) ); // create references - Gia_ManSetRefs( p->pAig ); + Gia_ManCreateValueRefs( p->pAig ); // set starting representative of internal nodes to be constant 0 if ( p->pPars->fLatchCorr ) Gia_ManForEachObj( p->pAig, pObj, i ) @@ -908,7 +908,7 @@ int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax ) int Cec_ManSimClassesRefine( Cec_ManSim_t * p ) { int i; - Gia_ManSetRefs( p->pAig ); + Gia_ManCreateValueRefs( p->pAig ); p->nWords = p->pPars->nWords; for ( i = 0; i < p->pPars->nRounds; i++ ) { diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index 300c10d5..f35cd952 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -548,7 +548,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore Vec_Ptr_t * vSimInfo; int RetValue = 0, iStart = 0; vPairs = Gia_ManCorrCreateRemapping( pSim->pAig ); - Gia_ManSetRefs( pSim->pAig ); + Gia_ManCreateValueRefs( pSim->pAig ); // pSim->pPars->nWords = 63; pSim->pPars->nFrames = nFrames; vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords ); @@ -584,7 +584,7 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS { Vec_Ptr_t * vSimInfo; int RetValue = 0, iStart = 0; - Gia_ManSetRefs( pSim->pAig ); + Gia_ManCreateValueRefs( pSim->pAig ); pSim->pPars->nFrames = 1; vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords ); while ( iStart < Vec_IntSize(vCexStore) ) diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c index 3afbd1c8..da60de1d 100644 --- a/src/proof/cec/cecSeq.c +++ b/src/proof/cec/cecSeq.c @@ -191,7 +191,7 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig); pParsSim->nWords = Vec_PtrReadWordsSimInfo( vSimInfo ); pParsSim->fCheckMiter = fCheckMiter; - Gia_ManSetRefs( pAig ); + Gia_ManCreateValueRefs( pAig ); pSim = Cec_ManSimStart( pAig, pParsSim ); if ( pBestState ) pSim->pBestState = pBestState; diff --git a/src/proof/cec/cecSweep.c b/src/proof/cec/cecSweep.c index 16697776..9ba2e07e 100644 --- a/src/proof/cec/cecSweep.c +++ b/src/proof/cec/cecSweep.c @@ -197,7 +197,7 @@ p->timePat += clock() - clk; clk = clock(); if ( vInfo != NULL ) { - Gia_ManSetRefs( p->pAig ); + Gia_ManCreateValueRefs( p->pAig ); for ( i = 0; i < pPat->nSeries; i++ ) { Cec_ManFraCreateInfo( pSim, pSim->vCiSimInfo, vInfo, i ); -- cgit v1.2.3