summaryrefslogtreecommitdiff
path: root/src/prop/sat_solver_factory.h
diff options
context:
space:
mode:
authorLiana Hadarean <lianahady@gmail.com>2012-04-04 02:02:06 +0000
committerLiana Hadarean <lianahady@gmail.com>2012-04-04 02:02:06 +0000
commit52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch)
tree040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/prop/sat_solver_factory.h
parent4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff)
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally * added more bv regressions
Diffstat (limited to 'src/prop/sat_solver_factory.h')
-rw-r--r--src/prop/sat_solver_factory.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 367397fdf..379141cc6 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -30,7 +30,7 @@ namespace prop {
class SatSolverFactory {
public:
- static BVSatSolverInterface* createMinisat();
+ static BVSatSolverInterface* createMinisat(context::Context* mainSatContext);
static DPLLSatSolverInterface* createDPLLMinisat();
static SatSolver* create(const char* id);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback