Global registry of SAT solvers, where they are registered at compile time. The available SAT solvers can be seen with the --show-sat-solvers option.

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