From ae4b51351c93983a1285ce1028e3bbd90a6d5721 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 13 Jan 2011 12:38:59 -0800 Subject: Cumulative changes in the last few weeks. --- src/aig/mfx/mfxInt.h | 3 ++- src/aig/mfx/mfxInter.c | 18 ++++++++++-------- src/aig/mfx/mfxMan.c | 6 ++++-- src/aig/mfx/mfxResub.c | 12 ++++++------ src/aig/mfx/mfxSat.c | 10 +++++----- 5 files changed, 27 insertions(+), 22 deletions(-) (limited to 'src/aig/mfx') diff --git a/src/aig/mfx/mfxInt.h b/src/aig/mfx/mfxInt.h index 1fcf4e91..320e7a8e 100644 --- a/src/aig/mfx/mfxInt.h +++ b/src/aig/mfx/mfxInt.h @@ -60,7 +60,8 @@ struct Mfx_Man_t_ Vec_Ptr_t * vNodes; // the internal nodes of the window Vec_Ptr_t * vDivs; // the divisors of the node Vec_Int_t * vDivLits; // the SAT literals of divisor nodes - Vec_Int_t * vProjVars; // the projection variables + Vec_Int_t * vProjVarsCnf; // the projection variables + Vec_Int_t * vProjVarsSat; // the projection variables // intermediate simulation data Vec_Ptr_t * vDivCexes; // the counter-example for dividors int nDivWords; // the number of words diff --git a/src/aig/mfx/mfxInter.c b/src/aig/mfx/mfxInter.c index 2263398d..db2e5e7e 100644 --- a/src/aig/mfx/mfxInter.c +++ b/src/aig/mfx/mfxInter.c @@ -96,13 +96,13 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert ); // collect the outputs of the divisors - Vec_IntClear( p->vProjVars ); + Vec_IntClear( p->vProjVarsCnf ); Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) ) { assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); - Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + Vec_IntPush( p->vProjVarsCnf, p->pCnf->pVarNums[pObjPo->Id] ); } - assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) ); + assert( Vec_IntSize(p->vProjVarsCnf) == Vec_PtrSize(p->vDivs) ); // start the solver pSat = sat_solver_new(); @@ -161,7 +161,7 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - iVar = Vec_IntEntry( p->vProjVars, i ); + iVar = Vec_IntEntry( p->vProjVarsCnf, i ); // add the corresponding EXOR gate if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { @@ -181,15 +181,17 @@ sat_solver * Mfx_CreateSolverResub( Mfx_Man_t * p, int * pCands, int nCands, int else { // add the clauses for the EXOR gates - and remember their outputs - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntClear( p->vProjVarsSat ); + Vec_IntForEachEntry( p->vProjVarsCnf, iVar, i ) { if ( !Mfx_SatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { sat_solver_delete( pSat ); return NULL; } - Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i ); + Vec_IntPush( p->vProjVarsSat, 2 * p->pCnf->nVars + i ); } + assert( Vec_IntSize(p->vProjVarsCnf) == Vec_IntSize(p->vProjVarsSat) ); // simplify the solver status = sat_solver_simplify(pSat); if ( status == 0 ) @@ -242,7 +244,7 @@ unsigned * Mfx_InterplateTruth( Mfx_Man_t * p, int * pCands, int nCands, int fIn // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i ); } // derive the interpolant @@ -342,7 +344,7 @@ Hop_Obj_t * Mfx_Interplate( Mfx_Man_t * p, int * pCands, int nCands ) // get the variable number of this divisor i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars; // get the corresponding SAT variable - pGloVars[c] = Vec_IntEntry( p->vProjVars, i ); + pGloVars[c] = Vec_IntEntry( p->vProjVarsCnf, i ); } // derive the interpolant diff --git a/src/aig/mfx/mfxMan.c b/src/aig/mfx/mfxMan.c index 9d9994bf..ff8b02fd 100644 --- a/src/aig/mfx/mfxMan.c +++ b/src/aig/mfx/mfxMan.c @@ -49,7 +49,8 @@ Mfx_Man_t * Mfx_ManAlloc( Mfx_Par_t * pPars ) p = ABC_ALLOC( Mfx_Man_t, 1 ); memset( p, 0, sizeof(Mfx_Man_t) ); p->pPars = pPars; - p->vProjVars = Vec_IntAlloc( 100 ); + p->vProjVarsCnf = Vec_IntAlloc( 100 ); + p->vProjVarsSat = Vec_IntAlloc( 100 ); p->vDivLits = Vec_IntAlloc( 100 ); p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFX_FANIN_MAX); p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFX_FANIN_MAX+1, p->nDivWords ); @@ -178,7 +179,8 @@ void Mfx_ManStop( Mfx_Man_t * p ) Vec_IntFree( p->vMem ); Vec_VecFree( p->vLevels ); Vec_PtrFree( p->vFanins ); - Vec_IntFree( p->vProjVars ); + Vec_IntFree( p->vProjVarsCnf ); + Vec_IntFree( p->vProjVarsSat ); Vec_IntFree( p->vDivLits ); Vec_PtrFree( p->vDivCexes ); ABC_FREE( p ); diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c index 83673661..5a4786d6 100644 --- a/src/aig/mfx/mfxResub.c +++ b/src/aig/mfx/mfxResub.c @@ -111,7 +111,7 @@ int Mfx_TryResubOnce( Mfx_Man_t * p, int * pCands, int nCands ) } p->nSatCexes++; // store the counter-example - Vec_IntForEachEntry( p->vProjVars, iVar, i ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, i ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! @@ -166,7 +166,7 @@ int Mfx_SolveSatResub( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int fOnlyRe continue; Vec_PtrPush( p->vFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Mfx_TryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -244,7 +244,7 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Mfx_TryResubOnce( p, pCands, nCands+1 ); if ( RetValue == -1 ) return 0; @@ -316,7 +316,7 @@ int Mfx_SolveSatResub2( Mfx_Man_t * p, Nwk_Obj_t * pNode, int iFanin, int iFanin continue; Vec_PtrPush( p->vFanins, pFanin ); iVar = Vec_PtrSize(p->vDivs) - Nwk_ObjFaninNum(pNode) + i; - pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 ); + pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 ); } RetValue = Mfx_TryResubOnce( p, pCands, nCands ); if ( RetValue == -1 ) @@ -390,8 +390,8 @@ p->timeInt += clock() - clk; if ( iVar == Vec_PtrSize(p->vDivs)-Nwk_ObjFaninNum(pNode) ) return 0; - pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar2), 1 ); - pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 ); + pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 ); + pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 ); RetValue = Mfx_TryResubOnce( p, pCands, nCands+2 ); if ( RetValue == -1 ) return 0; diff --git a/src/aig/mfx/mfxSat.c b/src/aig/mfx/mfxSat.c index dc4cd862..974563ab 100644 --- a/src/aig/mfx/mfxSat.c +++ b/src/aig/mfx/mfxSat.c @@ -58,7 +58,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p ) p->nCares++; // add SAT assignment to the solver Mint = 0; - Vec_IntForEachEntry( p->vProjVars, iVar, b ) + Vec_IntForEachEntry( p->vProjVarsSat, iVar, b ) { Lits[b] = toLit( iVar ); if ( sat_solver_var_value( p->pSat, iVar ) ) @@ -70,7 +70,7 @@ int Mfx_SolveSat_iter( Mfx_Man_t * p ) assert( !Aig_InfoHasBit(p->uCare, Mint) ); Aig_InfoSetBit( p->uCare, Mint ); // add the blocking clause - RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) ); + RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) ); if ( RetValue == 0 ) return 0; return 1; @@ -92,15 +92,15 @@ int Mfx_SolveSat( Mfx_Man_t * p, Nwk_Obj_t * pNode ) Aig_Obj_t * pObjPo; int RetValue, i; // collect projection variables - Vec_IntClear( p->vProjVars ); + Vec_IntClear( p->vProjVarsSat ); Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Nwk_ObjFaninNum(pNode) ) { assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 ); - Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] ); + Vec_IntPush( p->vProjVarsSat, p->pCnf->pVarNums[pObjPo->Id] ); } // prepare the truth table of care set - p->nFanins = Vec_IntSize( p->vProjVars ); + p->nFanins = Vec_IntSize( p->vProjVarsSat ); p->nWords = Aig_TruthWordNum( p->nFanins ); memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); -- cgit v1.2.3