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/ezminisat.h | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'libs/ezsat/ezminisat.h')

diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 59fa2134..e7e08289 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -20,7 +20,7 @@
 #ifndef EZMINISAT_H
 #define EZMINISAT_H
 
-#define EZMINISAT_SOLVER Minisat::Solver
+#define EZMINISAT_SIMPSOLVER 0
 #define EZMINISAT_VERBOSITY 0
 #define EZMINISAT_INCREMENTAL 1
 
@@ -38,10 +38,19 @@ namespace Minisat {
 class ezMiniSAT : public ezSAT
 {
 private:
-	EZMINISAT_SOLVER *minisatSolver;
+#if EZMINISAT_SIMPSOLVER
+	typedef Minisat::SimpSolver Solver;
+#else
+	typedef Minisat::Solver Solver;
+#endif
+	Solver *minisatSolver;
 	std::vector<int> minisatVars;
 	bool foundContradiction;
 
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+	std::set<int> cnfFrozenVars;
+#endif
+
 	static ezMiniSAT *alarmHandlerThis;
 	static clock_t alarmHandlerTimeout;
 	static void alarmHandler(int);
@@ -50,6 +59,9 @@ public:
 	ezMiniSAT();
 	virtual ~ezMiniSAT();
 	virtual void clear();
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+	virtual void freeze(int id);
+#endif
 	virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
 };
 
-- 
cgit v1.2.3