diff options
| author | Clifford Wolf <clifford@clifford.at> | 2013-06-09 14:21:18 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2013-06-09 14:21:18 +0200 |
| commit | 41932e8b64414da138e941c75f03077f43654c89 (patch) | |
| tree | b9678439aa0461b3403ba2ff2c63304014463d13 | |
| parent | b7ba90910dfc06d89bf45b6ead9e40e9bf985fe1 (diff) | |
| download | yosys-41932e8b64414da138e941c75f03077f43654c89.tar.gz yosys-41932e8b64414da138e941c75f03077f43654c89.tar.bz2 yosys-41932e8b64414da138e941c75f03077f43654c89.zip | |
Added ezSAT api support for don't care values in models
| -rw-r--r-- | libs/ezsat/ezminisat.cc | 21 | ||||
| -rw-r--r-- | libs/ezsat/ezsat.h | 3 | ||||
| -rw-r--r-- | passes/sat/sat_solve.cc | 5 |
3 files changed, 23 insertions, 6 deletions
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index a5ceb9e56..c34ad7480 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 ea873a859..8371071ed 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) { diff --git a/passes/sat/sat_solve.cc b/passes/sat/sat_solve.cc index 362efb2de..eb9e31631 100644 --- a/passes/sat/sat_solve.cc +++ b/passes/sat/sat_solve.cc @@ -419,8 +419,11 @@ rerun_solver: for (auto &info : modelInfo) { RTLIL::Const value; - for (int i = 0; i < info.width; i++) + for (int i = 0; i < info.width; i++) { value.bits.push_back(modelValues.at(info.offset+i) ? RTLIL::State::S1 : RTLIL::State::S0); + if (modelValues.size() == 2*modelExpressions.size() && modelValues.at(modelExpressions.size()+info.offset+i)) + value.bits.back() = RTLIL::State::Sx; + } if (info.timestep != last_timestep) { const char *hline = "---------------------------------------------------------------------------------------------------" |