diff options
author | Clifford Wolf <clifford@clifford.at> | 2014-02-23 01:35:59 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2014-02-23 01:35:59 +0100 |
commit | dab1612f81212d1bc1c07ee77b265167861ec883 (patch) | |
tree | 2baf983b4b6ee965ceeac4d3038c05b064c4fe9c /libs/ezsat/ezminisat.h | |
parent | b76528d8a557dc324b1dfaa366e2b620795f582d (diff) |
Added support for Minisat::SimpSolver + ezSAT frezze() API
Diffstat (limited to 'libs/ezsat/ezminisat.h')
-rw-r--r-- | libs/ezsat/ezminisat.h | 16 |
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); }; |