Added ezSAT::eliminated API to help the SAT solver remember eliminated variables

1 files changed, 7 insertions, 3 deletions

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index cc6301e4..4389c7a6 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;