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.

10 files changed, 241 insertions, 9 deletions

diff --git a/.cproject b/.cproject
index 6467c05f2..bcc6a9ca5 100644
--- a/.cproject
+++ b/.cproject
@@ -326,6 +326,14 @@
 				<useDefaultCommand>true</useDefaultCommand>
 				<runAllBuilders>true</runAllBuilders>
 			</target>
+			<target name="check" path="test/regress" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+				<buildCommand>make</buildCommand>
+				<buildArguments>-j10</buildArguments>
+				<buildTarget>check</buildTarget>
+				<stopOnError>true</stopOnError>
+				<useDefaultCommand>true</useDefaultCommand>
+				<runAllBuilders>true</runAllBuilders>
+			</target>
 			<target name="check" path="test/unit" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
 				<buildCommand>make</buildCommand>
 				<buildArguments>-j10</buildArguments>
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index c1dc3b828..e505c168e 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -17,7 +17,9 @@ libprop_la_SOURCES = \
 	cnf_stream.cpp \
 	sat_solver.h \
 	sat_solver_factory.h \
-	sat_solver_factory.cpp 
+	sat_solver_factory.cpp \
+	sat_solver_registry.h \
+	sat_solver_registry.cpp
 	
 SUBDIRS = minisat bvminisat
 
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>;
+
 }
 }
 
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
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index eb694852c..61c67ed5f 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -21,7 +21,8 @@
 #ifndef __CVC4__PROP__SAT_MODULE_H
 #define __CVC4__PROP__SAT_MODULE_H
 
-#include <stdint.h> 
+#include <string>
+#include <stdint.h>
 #include "util/options.h"
 #include "util/stats.h"
 #include "context/cdlist.h"
@@ -166,7 +167,6 @@ public:
 
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
-
  
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve() = 0;
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);
+}
 
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 09d66b8d4..367397fdf 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -20,6 +20,8 @@
 
 #include "cvc4_public.h"
 
+#include <string>
+#include <vector>
 #include "prop/sat_solver.h"
 
 namespace CVC4 {
@@ -27,8 +29,15 @@ namespace prop {
 
 class SatSolverFactory {
 public:
+
   static BVSatSolverInterface* createMinisat();
   static DPLLSatSolverInterface* createDPLLMinisat();
+
+  static SatSolver* create(const char* id);
+
+  /** Get the solver ids that are available */
+  static void getSolverIds(std::vector<std::string>& solvers);
+
 };
 
 }
diff --git a/src/prop/sat_solver_registry.cpp b/src/prop/sat_solver_registry.cpp
new file mode 100644
index 000000000..01434bd80
--- /dev/null
+++ b/src/prop/sat_solver_registry.cpp
@@ -0,0 +1,61 @@
+/*********************                                                        */
+/*! \file sat_solver_registry.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): barrett, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This class transforms a sequence of formulas into clauses.
+ **
+ ** This class takes a sequence of formulas.
+ ** It outputs a stream of clauses that is propositionally
+ ** equi-satisfiable with the conjunction of the formulas.
+ ** This stream is maintained in an online fashion.
+ **
+ ** Compile time registration of SAT solvers with the SAT solver factory
+ **/
+
+#include "prop/sat_solver_registry.h"
+#include "sstream"
+
+using namespace std;
+using namespace CVC4;
+using namespace prop;
+
+SatSolverConstructorInterface* SatSolverRegistry::getConstructor(string id) {
+  SatSolverRegistry* registry = getInstance();
+  registry_type::const_iterator find = registry->d_solvers.find(id);
+  if (find == registry->d_solvers.end()) {
+    return NULL;
+  } else {
+    return find->second;
+  }
+}
+
+void SatSolverRegistry::getSolverIds(std::vector<std::string>& solvers) {
+  SatSolverRegistry* registry = getInstance();
+  registry_type::const_iterator it = registry->d_solvers.begin();
+  registry_type::const_iterator it_end = registry->d_solvers.end();
+  for (; it != it_end; ++ it) {
+    solvers.push_back(it->first);
+  }
+}
+
+SatSolverRegistry* SatSolverRegistry::getInstance() {
+  static SatSolverRegistry registry;
+  return &registry;
+}
+
+SatSolverRegistry::~SatSolverRegistry() {
+  registry_type::const_iterator it = d_solvers.begin();
+  registry_type::const_iterator it_end = d_solvers.begin();
+  for (; it != it_end; ++ it) {
+    delete it->second;
+  }
+}
diff --git a/src/prop/sat_solver_registry.h b/src/prop/sat_solver_registry.h
new file mode 100644
index 000000000..df1cf86f8
--- /dev/null
+++ b/src/prop/sat_solver_registry.h
@@ -0,0 +1,118 @@
+/*********************                                                        */
+/*! \file sat_solver_registry.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): barrett, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This class transforms a sequence of formulas into clauses.
+ **
+ ** This class takes a sequence of formulas.
+ ** It outputs a stream of clauses that is propositionally
+ ** equi-satisfiable with the conjunction of the formulas.
+ ** This stream is maintained in an online fashion.
+ **
+ ** Compile time registration of SAT solvers with the SAT solver factory
+ **/
+
+#pragma once
+
+#include "cvc4_private.h"
+
+#include <map>
+#include <string>
+#include <cxxabi.h>
+#include "prop/sat_solver.h"
+#include "prop/sat_solver_factory.h"
+
+namespace CVC4 {
+namespace prop {
+
+/**
+ * Interface for SAT solver constructors. Solvers should declare an instantiatiation of the
+ * SatSolverConstructor interface below.
+ */
+class SatSolverConstructorInterface {
+public:
+  virtual ~SatSolverConstructorInterface() {}
+  virtual SatSolver* construct() = 0;
+};
+
+/**
+ * Registry containing all the registered SAT solvers.
+ */
+class SatSolverRegistry {
+
+  typedef std::map<std::string, SatSolverConstructorInterface*> registry_type;
+
+  /** Map from ids to solver constructors */
+  registry_type d_solvers;
+
+  /** Nobody can create the registry, there can be only one! */
+  SatSolverRegistry() {}
+
+  /**
+   * Register a SAT solver with the registry. The Constructor type should be a subclass
+   * of the SatSolverConstrutor.
+   */
+  template <typename Constructor>
+  size_t registerSolver(const char* id) {
+    int status;
+    char* demangled = abi::__cxa_demangle(id, 0, 0, &status);
+    d_solvers[demangled] = new Constructor();
+    free(demangled);
+    return d_solvers.size();
+  }
+
+  /** Get the instance of the registry */
+  static SatSolverRegistry* getInstance();
+
+public:
+
+  /** Destructor */
+  ~SatSolverRegistry();
+
+  /**
+   * Returns the constructor for the given SAT solver.
+   */
+  static SatSolverConstructorInterface* getConstructor(std::string id);
+
+  /** Get the ids of the available solvers */
+  static void getSolverIds(std::vector<std::string>& solvers);
+
+  /** The Constructors are friends, since they need to register */
+  template<typename Solver>
+  friend class SatSolverConstructor;
+
+};
+
+/**
+ * Declare an instance of this class with the SAT solver in order to put it in the registry.
+ */
+template<typename Solver>
+class SatSolverConstructor : public SatSolverConstructorInterface {
+
+  /** Static solver id we use for initialization */
+  static const size_t s_solverId;
+
+public:
+
+  /** Constructs the solver */
+  SatSolver* construct() {
+    return new Solver();
+  }
+
+};
+
+template<typename Solver>
+const size_t SatSolverConstructor<Solver>::s_solverId = SatSolverRegistry::getInstance()->registerSolver<SatSolverConstructor>(typeid(Solver).name());
+
+}
+}
+
diff --git a/src/util/options.cpp b/src/util/options.cpp
index d3426e152..b6956a31b 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -35,6 +35,7 @@
 #include "util/options.h"
 #include "util/output.h"
 #include "util/dump.h"
+#include "prop/sat_solver_factory.h"
 
 #include "cvc4autoconfig.h"
 
@@ -163,6 +164,7 @@ Additional CVC4 options:\n\
    --debug | -d           debug something (e.g. -d arith), can repeat\n\
    --show-debug-tags      show all avalable tags for debugging\n\
    --show-trace-tags      show all avalable tags for tracing\n\
+   --show-sat-solvers     show all available SAT solvers\n\
    --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
    --print-expr-types     print types with variables when printing exprs\n\
    --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
@@ -324,6 +326,7 @@ enum OptionValue {
   USE_MMAP,
   SHOW_DEBUG_TAGS,
   SHOW_TRACE_TAGS,
+  SHOW_SAT_SOLVERS,
   SHOW_CONFIG,
   STRICT_PARSING,
   DEFAULT_EXPR_DEPTH,
@@ -399,6 +402,7 @@ static struct option cmdlineOptions[] = {
   { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION },
   { "show-debug-tags", no_argument  , NULL, SHOW_DEBUG_TAGS },
   { "show-trace-tags", no_argument  , NULL, SHOW_TRACE_TAGS },
+  { "show-sat-solvers", no_argument  , NULL, SHOW_SAT_SOLVERS },
   { "show-config", no_argument      , NULL, SHOW_CONFIG },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
   { "help"       , no_argument      , NULL, 'h'         },
@@ -930,6 +934,21 @@ throw(OptionException) {
       exit(0);
       break;
 
+    case SHOW_SAT_SOLVERS:
+    {
+      vector<string> solvers;
+      prop::SatSolverFactory::getSolverIds(solvers);
+      printf("Available SAT solvers: ");
+      for (unsigned i = 0; i < solvers.size(); ++ i) {
+        if (i > 0) {
+          printf(", ");
+        }
+        printf("%s", solvers[i].c_str());
+      }
+      printf("\n");
+      exit(0);
+      break;
+    }
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");