diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-11-25 02:50:34 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-11-25 02:50:34 +0100 |
| commit | 4d433317483d5db3087037619bb681a6e917fc7d (patch) | |
| tree | 435185a1ae1b1a3a53e1d86431e8243883460767 /libs | |
| parent | 76f7c10cfc7450e6be8eb25fc26f5447e05759b0 (diff) | |
| download | yosys-4d433317483d5db3087037619bb681a6e917fc7d.tar.gz yosys-4d433317483d5db3087037619bb681a6e917fc7d.tar.bz2 yosys-4d433317483d5db3087037619bb681a6e917fc7d.zip | |
Removed undef feature from ezsat api
Diffstat (limited to 'libs')
| -rw-r--r-- | libs/ezsat/ezminisat.cc | 10 | ||||
| -rw-r--r-- | libs/ezsat/ezsat.h | 3 |
2 files changed, 2 insertions, 11 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index 05eb2af5d..d545834cf 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; diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 3fb5fcaf6..abec0b239 100644 --- 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) { |