diff options
Diffstat (limited to 'libs/ezsat/ezminisat.cc')
| -rw-r--r-- | libs/ezsat/ezminisat.cc | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index fbc85c1ff..a5ceb9e56 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -86,9 +86,9 @@ contradiction: Minisat::vec<Minisat::Lit> ps; for (auto idx : clause) if (idx > 0) - ps.push(Minisat::mkLit(minisatVars[idx-1])); + ps.push(Minisat::mkLit(minisatVars.at(idx-1))); else - ps.push(Minisat::mkLit(minisatVars[-idx-1], true)); + ps.push(Minisat::mkLit(minisatVars.at(-idx-1), true)); if (!minisatSolver->addClause(ps)) goto contradiction; } @@ -100,9 +100,9 @@ contradiction: for (auto idx : extraClauses) if (idx > 0) - assumps.push(Minisat::mkLit(minisatVars[idx-1])); + assumps.push(Minisat::mkLit(minisatVars.at(idx-1))); else - assumps.push(Minisat::mkLit(minisatVars[-idx-1], true)); + assumps.push(Minisat::mkLit(minisatVars.at(-idx-1), true)); if (!minisatSolver->solve(assumps)) return false; @@ -110,9 +110,12 @@ contradiction: modelValues.clear(); modelValues.reserve(modelIdx.size()); for (auto idx : modelIdx) { - auto value = minisatSolver->modelValue(minisatVars[idx-1]); + bool refvalue = true; + if (idx < 0) + idx = -idx, refvalue = false; + auto value = minisatSolver->modelValue(minisatVars.at(idx-1)); // FIXME: Undef values - modelValues.push_back(value == Minisat::lbool(true)); + modelValues.push_back(value == Minisat::lbool(refvalue)); } return true; |