diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 5 | ||||
-rw-r--r-- | src/aig/gia/giaCSat.c | 18 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 11 | ||||
-rw-r--r-- | src/aig/gia/giaMan.c | 2 |
4 files changed, 26 insertions, 10 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e5e5b303..23363687 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -113,6 +113,7 @@ struct Gia_Man_t_ int fAddStrash; // performs additional structural hashing int fSweeper; // sweeper is running int fGiaSimple; // simple mode (no const-propagation and strashing) + Vec_Int_t vRefs; // the reference count int * pRefs; // the reference count int * pLutRefs; // the reference count Vec_Int_t * vLevels; // levels of the nodes @@ -1203,6 +1204,10 @@ extern Abc_Cex_t * Gia_ManCexExtendToIncludeAllObjects( Gia_Man_t * p, A /*=== giaCsatOld.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ +typedef struct Cbs_Man_t_ Cbs_Man_t; +extern Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia ); +extern void Cbs_ManStop( Cbs_Man_t * p ); +extern int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCTas.c ============================================================*/ extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index e0e0e315..5f516e21 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -59,7 +59,7 @@ struct Cbs_Que_t_ Gia_Obj_t ** pData; // nodes stored in the queue }; -typedef struct Cbs_Man_t_ Cbs_Man_t; +//typedef struct Cbs_Man_t_ Cbs_Man_t; struct Cbs_Man_t_ { Cbs_Par_t Pars; // parameters @@ -146,7 +146,7 @@ void Cbs_SetDefaultParams( Cbs_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -Cbs_Man_t * Cbs_ManAlloc() +Cbs_Man_t * Cbs_ManAlloc( Gia_Man_t * pGia ) { Cbs_Man_t * p; p = ABC_CALLOC( Cbs_Man_t, 1 ); @@ -158,6 +158,7 @@ Cbs_Man_t * Cbs_ManAlloc() p->vModel = Vec_IntAlloc( 1000 ); p->vLevReas = Vec_IntAlloc( 1000 ); p->vTemp = Vec_PtrAlloc( 1000 ); + p->pAig = pGia; Cbs_SetDefaultParams( &p->Pars ); return p; } @@ -619,7 +620,7 @@ static inline void Cbs_ManDeriveReason( Cbs_Man_t * p, int Level ) pReason = Cbs_VarReason0( p, pObj ); if ( pReason == pObj ) // no reason { - assert( pQue->pData[pQue->iHead] == NULL ); + //assert( pQue->pData[pQue->iHead] == NULL ); pQue->pData[pQue->iHead] = pObj; continue; } @@ -929,7 +930,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level ) SeeAlso [] ***********************************************************************/ -int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) +int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ) { int RetValue = 0; s_Counter = 0; @@ -938,6 +939,8 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) assert( p->pClauses.iHead == 1 && p->pClauses.iTail == 1 ); p->Pars.nBTThis = p->Pars.nJustThis = p->Pars.nBTThisNc = 0; Cbs_ManAssign( p, pObj, 0, NULL, NULL ); + if ( pObj2 ) + Cbs_ManAssign( p, pObj2, 0, NULL, NULL ); if ( !Cbs_ManSolve_rec(p, 0) && !Cbs_ManCheckLimits(p) ) Cbs_ManSaveModel( p, p->vModel ); else @@ -1014,9 +1017,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt Gia_ManFillValue( pAig ); // maps nodes into trail ids Gia_ManSetPhase( pAig ); // maps nodes into trail ids // create logic network - p = Cbs_ManAlloc(); + p = Cbs_ManAlloc( pAig ); p->Pars.nBTLimit = nConfs; - p->pAig = pAig; // create resulting data-structures vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); vCexStore = Vec_IntAlloc( 10000 ); @@ -1046,14 +1048,14 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt clk = Abc_Clock(); p->Pars.fUseHighest = 1; p->Pars.fUseLowest = 0; - status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); + status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot), NULL ); // printf( "\n" ); /* if ( status == -1 ) { p->Pars.fUseHighest = 0; p->Pars.fUseLowest = 1; - status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot) ); + status = Cbs_ManSolve( p, Gia_ObjChild0(pRoot), NULL ); } */ Vec_StrPush( vStatus, (char)status ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 2be08453..552918d5 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1988,10 +1988,11 @@ void Gia_ManQuantExist_rec( Gia_Man_t * p, int iObj, int pRes[2] ) } int Gia_ManQuantExist( Gia_Man_t * p0, int iLit, int(*pFuncCiToKeep)(void *, int), void * pData ) { +// abctime clk = Abc_Clock(); Gia_Man_t * pNew; Vec_Int_t * vOuts, * vOuts2, * vCis; Gia_Obj_t * pObj = Gia_ManObj( p0, Abc_Lit2Var(iLit) ); - int i, n, Entry, Lit, OutLit = -1, pLits[2]; + int i, n, Entry, Lit, OutLit = -1, pLits[2], nVarsQua, nAndsOld, nAndsNew; if ( iLit < 2 ) return iLit; if ( Gia_ObjIsCi(pObj) ) return pFuncCiToKeep(pData, Gia_ObjCioId(pObj)) ? iLit : 1; assert( Gia_ObjIsAnd(pObj) ); @@ -2007,6 +2008,8 @@ int Gia_ManQuantExist( Gia_Man_t * p0, int iLit, int(*pFuncCiToKeep)(void *, int vOuts2 = Vec_IntAlloc( 100 ); assert( OutLit > 1 ); Vec_IntPush( vOuts, OutLit ); + nVarsQua = pNew->iSuppPi; + nAndsOld = Gia_ManAndNum(pNew); while ( --pNew->iSuppPi >= 0 ) { //printf( "Quantifying input %d:\n", p->iSuppPi ); @@ -2047,8 +2050,14 @@ int Gia_ManQuantExist( Gia_Man_t * p0, int iLit, int(*pFuncCiToKeep)(void *, int Vec_IntFree( vOuts2 ); // transfer back Gia_ManAppendCo( pNew, OutLit ); + nAndsNew = Gia_ManAndNum(p0); Lit = Gia_ManDupConeBack( p0, pNew, vCis ); + nAndsNew = Gia_ManAndNum(p0) - nAndsNew; Gia_ManStop( pNew ); + // report the result +// printf( "Performed quantification with %6d nodes, %3d keep-vars, %3d quant-vars, resulting in %5d new nodes. ", +// nAndsOld, Vec_IntSize(vCis) - nVarsQua, nVarsQua, nAndsNew ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Vec_IntFree( vCis ); return Lit; } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 48ae25a0..032980fe 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -142,6 +142,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFree( p->vCos ); Vec_IntErase( &p->vHash ); Vec_IntErase( &p->vHTable ); + Vec_IntErase( &p->vRefs ); ABC_FREE( p->pData2 ); ABC_FREE( p->pTravIds ); ABC_FREE( p->pPlacement ); @@ -157,7 +158,6 @@ void Gia_ManStop( Gia_Man_t * p ) ABC_FREE( p->pSibls ); ABC_FREE( p->pRefs ); ABC_FREE( p->pLutRefs ); -// ABC_FREE( p->pHTable ); ABC_FREE( p->pMuxes ); ABC_FREE( p->pObjs ); ABC_FREE( p->pSpec ); |