From 1ec01d8c637e611eddd16a492d1eb0f652b95da0 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 22 Feb 2014 01:29:02 +0100
Subject: Made MiniSat solver backend configurable in ezminisat.h

---
 libs/ezsat/ezminisat.cc | 7 +++++--
 libs/ezsat/ezminisat.h  | 6 +++++-
 2 files changed, 10 insertions(+), 3 deletions(-)

(limited to 'libs/ezsat')

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index d545834c..4d3301c4 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -29,6 +29,7 @@
 #include <cinttypes>
 
 #include <minisat/core/Solver.h>
+#include <minisat/simp/SimpSolver.h>
 
 ezMiniSAT::ezMiniSAT() : minisatSolver(NULL)
 {
@@ -90,8 +91,10 @@ contradiction:
 	for (auto id : modelExpressions)
 		modelIdx.push_back(bind(id));
 
-	if (minisatSolver == NULL)
-		minisatSolver = new Minisat::Solver;
+	if (minisatSolver == NULL) {
+		minisatSolver = new EZMINISAT_SOLVER;
+		minisatSolver->verbosity = EZMINISAT_VERBOSITY;
+	}
 
 	std::vector<std::vector<int>> cnf;
 	consumeCnf(cnf);
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 2919aa2e..04a010d6 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -20,6 +20,9 @@
 #ifndef EZMINISAT_H
 #define EZMINISAT_H
 
+#define EZMINISAT_SOLVER Minisat::Solver
+#define EZMINISAT_VERBOSITY 0
+
 #include "ezsat.h"
 #include <time.h>
 
@@ -28,12 +31,13 @@
 // don't force ezSAT users to use minisat headers..
 namespace Minisat {
 	class Solver;
+	class SimpSolver;
 }
 
 class ezMiniSAT : public ezSAT
 {
 private:
-	Minisat::Solver *minisatSolver;
+	EZMINISAT_SOLVER *minisatSolver;
 	std::vector<int> minisatVars;
 	bool foundContradiction;
 
-- 
cgit v1.2.3