diff options
| author | Clifford Wolf <clifford@clifford.at> | 2014-02-22 01:29:02 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2014-02-22 01:29:02 +0100 |
| commit | 1ec01d8c637e611eddd16a492d1eb0f652b95da0 (patch) | |
| tree | 32a63ffa5e929b27d5ef7ec6336bbc349ee0ffc2 /libs | |
| parent | 8b508dc90b87c99e13f1fa9f8e79e48c7fa52e90 (diff) | |
| download | yosys-1ec01d8c637e611eddd16a492d1eb0f652b95da0.tar.gz yosys-1ec01d8c637e611eddd16a492d1eb0f652b95da0.tar.bz2 yosys-1ec01d8c637e611eddd16a492d1eb0f652b95da0.zip | |
Made MiniSat solver backend configurable in ezminisat.h
Diffstat (limited to 'libs')
| -rw-r--r-- | libs/ezsat/ezminisat.cc | 7 | ||||
| -rw-r--r-- | libs/ezsat/ezminisat.h | 6 |
2 files changed, 10 insertions, 3 deletions
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; |