Made MiniSat solver backend configurable in ezminisat.h

diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index d545834cf28b5ee08a5449e15409fb6c342e4598..4d3301c4d51168b18448eb7ab92d315db16eb653 100644 (file)
--- 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 2919aa2e3b45c8d8f31e6c0009b294594881fada..04a010d68eb2eed729edb55bb8eb99eee7e8c5a2 100644 (file)
--- 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;