Added ezSAT api support for don't care values in models

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index a5ceb9e56a53fdc028edaffada0530e744f435a7..c34ad7480e087bf5e85aeed588605940b98df8e3 100644 (file)
--- 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 ea873a859601492446fcd09782363c5864186a27..8371071ed9a075465574bb7eb300a8dcb74a5e0e 100644 (file)
--- 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 362efb2dee02d0699f7fce0dcb6f865fa8aa37b9..eb9e3163165b5524f9b98aecbd8091b2553488a2 100644 (file)
--- 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 = "---------------------------------------------------------------------------------------------------"