From d500bd749f84c0b05a8ec96d2a5fc33ace0c5b58 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 1 Mar 2014 21:00:34 +0100
Subject: [PATCH] Added ezSAT::eliminated API to help the SAT solver remember
 eliminated variables

---
 libs/ezsat/ezminisat.cc |  8 ++++++++
 libs/ezsat/ezminisat.h  |  1 +
 libs/ezsat/ezsat.cc     | 10 +++++++---
 libs/ezsat/ezsat.h      |  1 +
 4 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 287177b1c..d488a9062 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -65,6 +65,14 @@ void ezMiniSAT::freeze(int id)
 {
 	cnfFrozenVars.insert(bind(id));
 }
+
+bool ezMiniSAT::eliminated(int idx)
+{
+	idx = idx < 0 ? -idx : idx;
+	if (minisatSolver != NULL && idx > 0 && idx <= int(minisatVars.size()))
+		return minisatSolver->isEliminated(minisatVars.at(idx-1));
+	return false;
+}
 #endif
 
 ezMiniSAT *ezMiniSAT::alarmHandlerThis = NULL;
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index e7e082891..c634e66e7 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -61,6 +61,7 @@ public:
 	virtual void clear();
 #if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
 	virtual void freeze(int id);
+	virtual bool eliminated(int idx);
 #endif
 	virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
 };
diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index cc6301e44..4389c7a62 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -348,9 +348,13 @@ void ezSAT::freeze(int)
 {
 }
 
-void ezSAT::assume(int id)
+bool ezSAT::eliminated(int)
 {
+	return false;
+}
 
+void ezSAT::assume(int id)
+{
 	if (id < 0)
 	{
 		assert(0 < -id && -id <= int(expressions.size()));
@@ -486,7 +490,7 @@ int ezSAT::bind(int id)
 	if (id >= 0) {
 		assert(0 < id && id <= int(literals.size()));
 		cnfLiteralVariables.resize(literals.size());
-		if (cnfLiteralVariables[id-1] == 0) {
+		if (cnfLiteralVariables[id-1] == 0 || eliminated(cnfLiteralVariables[id-1])) {
 			cnfLiteralVariables[id-1] = ++cnfVariableCount;
 			if (id == TRUE)
 				add_clause(+cnfLiteralVariables[id-1]);
@@ -499,7 +503,7 @@ int ezSAT::bind(int id)
 	assert(0 < -id && -id <= int(expressions.size()));
 	cnfExpressionVariables.resize(expressions.size());
 
-	if (cnfExpressionVariables[-id-1] == 0)
+	if (cnfExpressionVariables[-id-1] == 0 || eliminated(cnfExpressionVariables[-id-1]))
 	{
 		OpId op;
 		std::vector<int> args;
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index 8d340b3d6..16f940a1d 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -141,6 +141,7 @@ public:
 
 	virtual void clear();
 	virtual void freeze(int id);
+	virtual bool eliminated(int idx);
 	void assume(int id);
 	int bind(int id);
 	int bound(int id) const;
-- 
2.30.2