summaryrefslogtreecommitdiff
path: root/libs/ezsat/ezminisat.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-06-09 14:21:18 +0200
committerClifford Wolf <clifford@clifford.at>2013-06-09 14:21:18 +0200
commit41932e8b64414da138e941c75f03077f43654c89 (patch)
treeb9678439aa0461b3403ba2ff2c63304014463d13 /libs/ezsat/ezminisat.cc
parentb7ba90910dfc06d89bf45b6ead9e40e9bf985fe1 (diff)
Added ezSAT api support for don't care values in models
Diffstat (limited to 'libs/ezsat/ezminisat.cc')
-rw-r--r--libs/ezsat/ezminisat.cc21
1 files changed, 16 insertions, 5 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index a5ceb9e5..c34ad748 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -108,14 +108,25 @@ contradiction:
return false;
modelValues.clear();
- modelValues.reserve(modelIdx.size());
- for (auto idx : modelIdx) {
+ modelValues.resize(2 * modelIdx.size());
+
+ for (size_t i = 0; i < modelIdx.size(); i++)
+ {
+ int idx = modelIdx[i];
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(refvalue));
+
+ using namespace Minisat;
+ lbool value = minisatSolver->modelValue(minisatVars.at(idx-1));
+ if (value == l_Undef) {
+ modelValues[i] = false;
+ modelValues[modelIdx.size() + i] = true;
+ } else {
+ modelValues[i] = value == Minisat::lbool(refvalue);
+ modelValues[modelIdx.size() + i] = false;
+ }
}
return true;