From 357f3f6e93df1ebf2aa28a6c433a84f320fad043 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 22 Feb 2014 11:34:31 +0100
Subject: Added ezMiniSat EZMINISAT_INCREMENTAL compile-time option

---
 libs/ezsat/ezminisat.cc | 17 ++++++++++++++++-
 libs/ezsat/ezminisat.h  |  1 +
 2 files changed, 17 insertions(+), 1 deletion(-)

(limited to 'libs')

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index 4d3301c4..a1cb8052 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -96,8 +96,12 @@ contradiction:
 		minisatSolver->verbosity = EZMINISAT_VERBOSITY;
 	}
 
+#if EZMINISAT_INCREMENTAL
 	std::vector<std::vector<int>> cnf;
 	consumeCnf(cnf);
+#else
+	const std::vector<std::vector<int>> &cnf = this->cnf();
+#endif
 
 	while (int(minisatVars.size()) < numCnfVariables())
 		minisatVars.push_back(minisatSolver->newVar());
@@ -145,8 +149,14 @@ contradiction:
 		alarm(old_alarm_timeout);
 	}
 
-	if (!foundSolution)
+	if (!foundSolution) {
+#if !EZMINISAT_INCREMENTAL
+		delete minisatSolver;
+		minisatSolver = NULL;
+		minisatVars.clear();
+#endif
 		return false;
+	}
 
 	modelValues.clear();
 	modelValues.resize(modelIdx.size());
@@ -164,6 +174,11 @@ contradiction:
 		modelValues[i] = (value == Minisat::lbool(refvalue));
 	}
 
+#if !EZMINISAT_INCREMENTAL
+	delete minisatSolver;
+	minisatSolver = NULL;
+	minisatVars.clear();
+#endif
 	return true;
 }
 
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 04a010d6..59fa2134 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -22,6 +22,7 @@
 
 #define EZMINISAT_SOLVER Minisat::Solver
 #define EZMINISAT_VERBOSITY 0
+#define EZMINISAT_INCREMENTAL 1
 
 #include "ezsat.h"
 #include <time.h>
-- 
cgit v1.2.3