Removed undef feature from ezsat api

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 05eb2af5d16fce12d30cdf82d712980804b3daed..d545834cf28b5ee08a5449e15409fb6c342e4598 100644 (file)
--- 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;

diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 3fb5fcaf65d681ab903f53a07a5268ffcf874d9c..abec0b239a84818be0d073c6001dd2ec5766c6b7 100644 (file)
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -101,9 +101,6 @@ 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) {