diff options
Diffstat (limited to 'src/opt/mfs/mfsInter.c')
| -rw-r--r-- | src/opt/mfs/mfsInter.c | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 1b3f2415..0934513b 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -96,13 +96,13 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, 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(); @@ -178,7 +178,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_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 - iVar = Vec_IntEntry( p->vProjVars, i ); + iVar = Vec_IntEntry( p->vProjVarsCnf, i ); // add the corresponding EXOR gate if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) ) { @@ -198,15 +198,17 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, 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 ( !Abc_MfsSatAddXor( 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 ) @@ -259,7 +261,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i // 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 @@ -362,7 +364,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_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 |