summaryrefslogtreecommitdiff
path: root/libs/ezsat/ezminisat.h
diff options
context:
space:
mode:
Diffstat (limited to 'libs/ezsat/ezminisat.h')
-rw-r--r--libs/ezsat/ezminisat.h16
1 files changed, 14 insertions, 2 deletions
diff --git a/libs/ezsat/ezminisat.h b/libs/ezsat/ezminisat.h
index 59fa2134..e7e08289 100644
--- a/libs/ezsat/ezminisat.h
+++ b/libs/ezsat/ezminisat.h
@@ -20,7 +20,7 @@
#ifndef EZMINISAT_H
#define EZMINISAT_H
-#define EZMINISAT_SOLVER Minisat::Solver
+#define EZMINISAT_SIMPSOLVER 0
#define EZMINISAT_VERBOSITY 0
#define EZMINISAT_INCREMENTAL 1
@@ -38,10 +38,19 @@ namespace Minisat {
class ezMiniSAT : public ezSAT
{
private:
- EZMINISAT_SOLVER *minisatSolver;
+#if EZMINISAT_SIMPSOLVER
+ typedef Minisat::SimpSolver Solver;
+#else
+ typedef Minisat::Solver Solver;
+#endif
+ Solver *minisatSolver;
std::vector<int> minisatVars;
bool foundContradiction;
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ std::set<int> cnfFrozenVars;
+#endif
+
static ezMiniSAT *alarmHandlerThis;
static clock_t alarmHandlerTimeout;
static void alarmHandler(int);
@@ -50,6 +59,9 @@ public:
ezMiniSAT();
virtual ~ezMiniSAT();
virtual void clear();
+#if EZMINISAT_SIMPSOLVER && EZMINISAT_INCREMENTAL
+ virtual void freeze(int id);
+#endif
virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
};