From dab1612f81212d1bc1c07ee77b265167861ec883 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 23 Feb 2014 01:35:59 +0100
Subject: Added support for Minisat::SimpSolver + ezSAT frezze() API

---
 libs/ezsat/ezsat.cc | 33 +++++++++++++++++++++++++++------
 1 file changed, 27 insertions(+), 6 deletions(-)

(limited to 'libs/ezsat/ezsat.cc')

diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc
index 57762525..e6c005c6 100644
--- a/libs/ezsat/ezsat.cc
+++ b/libs/ezsat/ezsat.cc
@@ -29,18 +29,18 @@ const int ezSAT::FALSE = 2;
 
 ezSAT::ezSAT()
 {
-	literal("TRUE");
-	literal("FALSE");
-
-	assert(literal("TRUE") == TRUE);
-	assert(literal("FALSE") == FALSE);
-
 	cnfConsumed = false;
 	cnfVariableCount = 0;
 	cnfClausesCount = 0;
 
 	solverTimeout = 0;
 	solverTimoutStatus = false;
+
+	freeze(literal("TRUE"));
+	freeze(literal("FALSE"));
+
+	assert(literal("TRUE") == TRUE);
+	assert(literal("FALSE") == FALSE);
 }
 
 ezSAT::~ezSAT()
@@ -345,6 +345,10 @@ void ezSAT::clear()
 	cnfAssumptions.clear();
 }
 
+void ezSAT::freeze(int)
+{
+}
+
 void ezSAT::assume(int id)
 {
 	cnfAssumptions.insert(id);
@@ -462,6 +466,23 @@ int ezSAT::bound(int id) const
 	return 0;
 }
 
+std::string ezSAT::cnfLiteralInfo(int idx) const
+{
+	for (size_t i = 0; i < cnfLiteralVariables.size(); i++) {
+		if (cnfLiteralVariables[i] == idx)
+			return to_string(i+1);
+		if (cnfLiteralVariables[i] == -idx)
+			return "NOT " + to_string(i+1);
+	}
+	for (size_t i = 0; i < cnfExpressionVariables.size(); i++) {
+		if (cnfExpressionVariables[i] == idx)
+			return to_string(-i-1);
+		if (cnfExpressionVariables[i] == -idx)
+			return "NOT " + to_string(-i-1);
+	}
+	return "<unnamed>";
+}
+
 int ezSAT::bind(int id)
 {
 	if (id >= 0) {
-- 
cgit v1.2.3