From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 22 Feb 2014 00:29:02 +0000 (+0100)
Subject: Made MiniSat solver backend configurable in ezminisat.h
X-Git-Tag: yosys-0.3.0~114
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ec01d8c637e611eddd16a492d1eb0f652b95da0;p=yosys.git

Made MiniSat solver backend configurable in ezminisat.h
---

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index d545834cf..4d3301c4d 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 2919aa2e3..04a010d68 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;