diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-01-13 12:38:59 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-01-13 12:38:59 -0800 |
commit | ae4b51351c93983a1285ce1028e3bbd90a6d5721 (patch) | |
tree | b06797a1771bb1c79124f2ac7d57f1a54c9afc34 /src/aig/mfx/mfxSat.c | |
parent | f4066b5be3b5473f5c64ab71d1983df6ca7aec76 (diff) | |
download | abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.tar.gz abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.tar.bz2 abc-ae4b51351c93983a1285ce1028e3bbd90a6d5721.zip |
Cumulative changes in the last few weeks.
Diffstat (limited to 'src/aig/mfx/mfxSat.c')
-rw-r--r-- | src/aig/mfx/mfxSat.c | 10 |
1 files changed, 5 insertions, 5 deletions
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 ); |