summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--libs/ezsat/ezminisat.cc7
-rw-r--r--libs/ezsat/ezminisat.h6
2 files changed, 10 insertions, 3 deletions
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;