summaryrefslogtreecommitdiff
path: root/libs/ezsat/ezminisat.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-06-08 12:14:20 +0200
committerClifford Wolf <clifford@clifford.at>2013-06-08 12:14:20 +0200
commit25ae2d4df0cf9fcd4069e66d260c207300415af9 (patch)
tree9980c73b1a9c1ffffbc9bc9a0f732474d3cb32ff /libs/ezsat/ezminisat.cc
parentc681c17038acb5f60d5abcf58f20d6a8d2bdffef (diff)
Fixes and improvements in ezSAT library
Diffstat (limited to 'libs/ezsat/ezminisat.cc')
-rw-r--r--libs/ezsat/ezminisat.cc15
1 files changed, 9 insertions, 6 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index fbc85c1f..a5ceb9e5 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;