replace handleMetaSMT() with klee::createMetaSMTSolver() and move it into MetaSMTSolver.cpp so that the backend headers only need to be included once there

3 files changed, 39 insertions, 48 deletions

diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 32c8cf9e..7f12ddfb 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -253,7 +253,11 @@ namespace klee {
   
     virtual char *getConstraintLog(const Query&);
     virtual void setCoreSolverTimeout(double timeout);
-};
+  };
+
+  /// createMetaSMTSolver - Create a solver using the metaSMT backend set by 
+  /// the option MetaSMTBackend.
+  Solver *createMetaSMTSolver();
 
 #endif /* ENABLE_METASMT */
 
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index d36a3219..72b82807 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -14,52 +14,6 @@
 #include "llvm/Support/raw_ostream.h"
 #include <string>
 
-#ifdef ENABLE_METASMT
-
-#include <metaSMT/DirectSolver_Context.hpp>
-#include <metaSMT/backend/Z3_Backend.hpp>
-#include <metaSMT/backend/Boolector.hpp>
-
-#define Expr VCExpr
-#define Type VCType
-#define STP STP_Backend
-#include <metaSMT/backend/STP.hpp>
-#undef Expr
-#undef Type
-#undef STP
-
-using namespace klee;
-using namespace metaSMT;
-using namespace metaSMT::solver;
-
-static klee::Solver *handleMetaSMT() {
-  Solver *coreSolver = NULL;
-  std::string backend;
-  switch (MetaSMTBackend) {
-  case METASMT_BACKEND_STP:
-    backend = "STP";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >(
-        UseForkedCoreSolver, CoreSolverOptimizeDivides);
-    break;
-  case METASMT_BACKEND_Z3:
-    backend = "Z3";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >(
-        UseForkedCoreSolver, CoreSolverOptimizeDivides);
-    break;
-  case METASMT_BACKEND_BOOLECTOR:
-    backend = "Boolector";
-    coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >(
-        UseForkedCoreSolver, CoreSolverOptimizeDivides);
-    break;
-  default:
-    llvm_unreachable("Unrecognised MetaSMT backend");
-    break;
-  };
-  klee_message("Starting MetaSMTSolver(%s)", backend.c_str());
-  return coreSolver;
-}
-#endif /* ENABLE_METASMT */
-
 namespace klee {
 
 Solver *createCoreSolver(CoreSolverType cst) {
@@ -75,7 +29,7 @@ Solver *createCoreSolver(CoreSolverType cst) {
   case METASMT_SOLVER:
 #ifdef ENABLE_METASMT
     klee_message("Using MetaSMT solver backend");
-    return handleMetaSMT();
+    return createMetaSMTSolver();
 #else
     klee_message("Not compiled with MetaSMT support");
     return NULL;
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index a453de40..3b3eaf35 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -17,6 +17,8 @@
 #include "klee/util/Assignment.h"
 #include "klee/util/ExprUtil.h"
 
+#include "llvm/Support/ErrorHandling.h"
+
 #include <metaSMT/DirectSolver_Context.hpp>
 #include <metaSMT/backend/Z3_Backend.hpp>
 #include <metaSMT/backend/Boolector.hpp>
@@ -405,5 +407,36 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
 template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Boolector> >;
 template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Z3_Backend> >;
 template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::STP_Backend> >;
+
+Solver *createMetaSMTSolver() {
+  using metaSMT::DirectSolver_Context;
+  using namespace metaSMT::solver;
+
+  Solver *coreSolver = NULL;
+  std::string backend;
+  switch (MetaSMTBackend) {
+  case METASMT_BACKEND_STP:
+    backend = "STP";
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >(
+        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    break;
+  case METASMT_BACKEND_Z3:
+    backend = "Z3";
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >(
+        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    break;
+  case METASMT_BACKEND_BOOLECTOR:
+    backend = "Boolector";
+    coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >(
+        UseForkedCoreSolver, CoreSolverOptimizeDivides);
+    break;
+  default:
+    llvm_unreachable("Unrecognised MetaSMT backend");
+    break;
+  };
+  klee_message("Starting MetaSMTSolver(%s)", backend.c_str());
+  return coreSolver;
+}
+
 }
 #endif // ENABLE_METASMT