summaryrefslogtreecommitdiff
path: root/libs
diff options
context:
space:
mode:
Diffstat (limited to 'libs')
-rw-r--r--libs/ezsat/ezminisat.cc21
-rw-r--r--libs/ezsat/ezsat.h3
2 files changed, 19 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;
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index ea873a85..8371071e 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -98,6 +98,9 @@ public:
// If you are planning on using the solver API (and not simply create a CNF) you must use a child class
// of ezSAT that actually implements a solver backend, such as ezMiniSAT (see ezminisat.h).
+ // Note: Solvers that can output don't-care values for model variables return a twice as big modelValues
+ // vector. The first half contains the values and the second half the don't-care flags.
+
virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
bool solve(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) {