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, 4 insertions, 2 deletions

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 043aa5d24..86fbe4433 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -19,6 +19,7 @@
 #pragma once
 
 #include "prop/sat_solver.h"
+#include "prop/sat_solver_registry.h"
 #include "prop/bvminisat/simp/SimpSolver.h"
 
 namespace CVC4 {
@@ -27,8 +28,8 @@ namespace prop {
 class MinisatSatSolver: public BVSatSolverInterface {
   BVMinisat::SimpSolver* d_minisat;
 
-  MinisatSatSolver();
 public:
+  MinisatSatSolver();
   ~MinisatSatSolver();
   void addClause(SatClause& clause, bool removable);
 
@@ -76,9 +77,10 @@ public:
   };
 
   Statistics d_statistics;
-  friend class SatSolverFactory;
 };
 
+template class SatSolverConstructor<MinisatSatSolver>;
+
 }
 }