Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providing

a ``createCoreSolver()`` function. The solver used is set by the new
``--solver-backend`` command line argument. The default is STP.

This change necessitated refactoring the MetaSMT stuff. That clearly
didn't belong in the Executor! The MetaSMT command line option is
now ``--metasmt-backend`` as this only picks the MetaSMT backend.

In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed.

Note I don't have MetaSMT built on my development machine so I don't
know if the MetaSMT stuff even compiles...

1 files changed, 87 insertions, 0 deletions

diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
new file mode 100644
index 00000000..9d21931d
--- /dev/null
+++ b/lib/Solver/CoreSolver.cpp
@@ -0,0 +1,87 @@
+//===-- CoreSolver.cpp ------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/CommandLine.h"
+#include "klee/Solver.h"
+#include "llvm/Support/ErrorHandling.h"
+#include "llvm/Support/raw_ostream.h"
+#include <string>
+
+#ifdef SUPPORT_METASMT
+
+#include <metaSMT/frontend/Array.hpp>
+#include <metaSMT/backend/Z3_Backend.hpp>
+#include <metaSMT/backend/Boolector.hpp>
+#include <metaSMT/backend/MiniSAT.hpp>
+#include <metaSMT/DirectSolver_Context.hpp>
+#include <metaSMT/support/run_algorithm.hpp>
+#include <metaSMT/API/Stack.hpp>
+#include <metaSMT/API/Group.hpp>
+
+#define Expr VCExpr
+#define Type VCType
+#define STP STP_Backend
+#include <metaSMT/backend/STP.hpp>
+#undef Expr
+#undef Type
+#undef STP
+
+using namespace metaSMT;
+using namespace metaSMT::solver;
+
+static 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;
+  };
+  llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
+  return coreSolver;
+}
+#endif /* SUPPORT_METASMT */
+
+namespace klee {
+
+Solver *createCoreSolver(CoreSolverType cst) {
+  switch (cst) {
+  case STP_SOLVER:
+    llvm::errs() << "Using STP solver backend\n";
+    return new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides);
+  case METASMT_SOLVER:
+#ifdef SUPPORT_METASMT
+    llvm::errs() << "Using MetaSMT solver backend\n";
+    return handleMetaSMT();
+#else
+    llvm::errs() << "Not compiled with MetaSMT support\n";
+    return NULL;
+#endif
+  case DUMMY_SOLVER:
+    return createDummySolver();
+  default:
+    llvm_unreachable("Unsupported CoreSolverType");
+  }
+}
+}