summaryrefslogtreecommitdiff
path: root/src/prop/minisat/minisat.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat/minisat.h')
-rw-r--r--src/prop/minisat/minisat.h8
1 files changed, 5 insertions, 3 deletions
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 549c0b679..66aca717d 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -19,6 +19,7 @@
#pragma once
#include "prop/sat_solver.h"
+#include "prop/sat_solver_registry.h"
#include "prop/minisat/simp/SimpSolver.h"
namespace CVC4 {
@@ -36,11 +37,11 @@ class DPLLMinisatSatSolver : public DPLLSatSolverInterface {
/** Context we will be using to synchronzie the sat solver */
context::Context* d_context;
- DPLLMinisatSatSolver ();
-
public:
+ DPLLMinisatSatSolver ();
~DPLLMinisatSatSolver();
+
static SatVariable toSatVariable(Minisat::Var var);
static Minisat::Lit toMinisatLit(SatLiteral lit);
static SatLiteral toSatLiteral(Minisat::Lit lit);
@@ -93,9 +94,10 @@ public:
};
Statistics d_statistics;
- friend class SatSolverFactory;
};
+template class SatSolverConstructor<DPLLMinisatSatSolver>;
+
} // prop namespace
} // cvc4 namespace
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback