From 3ae967137fc715ff4ae5109895771fd1ca0724e4 Mon Sep 17 00:00:00 2001
From: "Hoang M. Le" <hle@informatik.uni-bremen.de>
Date: Wed, 15 Mar 2017 13:21:44 +0100
Subject: replace handleMetaSMT() with klee::createMetaSMTSolver() and move it
 into MetaSMTSolver.cpp so that the backend headers only need to be included
 once there

---
 lib/Solver/CoreSolver.cpp | 48 +----------------------------------------------
 1 file changed, 1 insertion(+), 47 deletions(-)

(limited to 'lib/Solver/CoreSolver.cpp')

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;
-- 
cgit 1.4.1