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, 12 insertions, 1 deletions

diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index fbb244789..c5972d7bb 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -17,6 +17,7 @@
  **/
 
 #include "prop/sat_solver_factory.h"
+#include "prop/sat_solver_registry.h"
 #include "prop/minisat/minisat.h"
 #include "prop/bvminisat/bvminisat.h"
 
@@ -31,6 +32,16 @@ DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() {
   return new DPLLMinisatSatSolver();
 }
 
+SatSolver* SatSolverFactory::create(const char* name) {
+  SatSolverConstructorInterface* constructor = SatSolverRegistry::getConstructor(name);
+  if (constructor) {
+    return constructor->construct();
+  } else {
+    return NULL;
+  }
+}
 
-
+void SatSolverFactory::getSolverIds(std::vector<std::string>& solvers) {
+  SatSolverRegistry::getSolverIds(solvers);
+}