From 25ae2d4df0cf9fcd4069e66d260c207300415af9 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 8 Jun 2013 12:14:20 +0200 Subject: Fixes and improvements in ezSAT library --- libs/ezsat/ezminisat.cc | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'libs/ezsat/ezminisat.cc') 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 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; -- cgit v1.2.3