diff options
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 ); |