diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-06-08 12:14:20 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-06-08 12:14:20 +0200 |
| commit | 25ae2d4df0cf9fcd4069e66d260c207300415af9 (patch) | |
| tree | 9980c73b1a9c1ffffbc9bc9a0f732474d3cb32ff /libs/ezsat/ezminisat.cc | |
| parent | c681c17038acb5f60d5abcf58f20d6a8d2bdffef (diff) | |
| download | yosys-25ae2d4df0cf9fcd4069e66d260c207300415af9.tar.gz yosys-25ae2d4df0cf9fcd4069e66d260c207300415af9.tar.bz2 yosys-25ae2d4df0cf9fcd4069e66d260c207300415af9.zip | |
Fixes and improvements in ezSAT library
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; |