summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--libs/ezsat/ezminisat.cc21
-rw-r--r--libs/ezsat/ezsat.h3
-rw-r--r--passes/sat/sat_solve.cc5
3 files changed, 23 insertions, 6 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) {
diff --git a/passes/sat/sat_solve.cc b/passes/sat/sat_solve.cc
index 362efb2d..eb9e3163 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 = "---------------------------------------------------------------------------------------------------"