summaryrefslogtreecommitdiff
path: root/libs/ezsat/ezminisat.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-11-25 02:50:34 +0100
committerClifford Wolf <clifford@clifford.at>2013-11-25 02:50:34 +0100
commit4d433317483d5db3087037619bb681a6e917fc7d (patch)
tree435185a1ae1b1a3a53e1d86431e8243883460767 /libs/ezsat/ezminisat.cc
parent76f7c10cfc7450e6be8eb25fc26f5447e05759b0 (diff)
Removed undef feature from ezsat api
Diffstat (limited to 'libs/ezsat/ezminisat.cc')
-rw-r--r--libs/ezsat/ezminisat.cc10
1 files changed, 2 insertions, 8 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 05eb2af5..d545834c 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -146,7 +146,7 @@ contradiction:
return false;
modelValues.clear();
- modelValues.resize(2 * modelIdx.size());
+ modelValues.resize(modelIdx.size());
for (size_t i = 0; i < modelIdx.size(); i++)
{
@@ -158,13 +158,7 @@ contradiction:
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;
- }
+ modelValues[i] = (value == Minisat::lbool(refvalue));
}
return true;