From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 25 Nov 2013 01:50:34 +0000 (+0100)
Subject: Removed undef feature from ezsat api
X-Git-Tag: yosys-0.2.0~302
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d433317483d5db3087037619bb681a6e917fc7d;p=yosys.git

Removed undef feature from ezsat api
---

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) {