From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 9 Jun 2013 12:21:18 +0000 (+0200)
Subject: Added ezSAT api support for don't care values in models
X-Git-Tag: yosys-0.2.0~595
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41932e8b64414da138e941c75f03077f43654c89;p=yosys.git

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

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 = "---------------------------------------------------------------------------------------------------"