From e81f5ceed580d4d267e3c857b47637d6bd065499 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 7 Jan 2016 12:00:25 +0000
Subject: 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...
---
 tools/kleaver/main.cpp | 42 +++---------------------------------------
 1 file changed, 3 insertions(+), 39 deletions(-)

(limited to 'tools/kleaver')

diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index af337abe..f91693c5 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -104,9 +104,6 @@ namespace {
                          "Fold constants and simplify expressions."),
               clEnumValEnd));
 
-  cl::opt<bool>
-  UseDummySolver("use-dummy-solver",
-		   cl::init(false));
 
   llvm::cl::opt<std::string> directoryToWriteQueryLogs("query-log-dir",llvm::cl::desc("The folder to write query logs to. Defaults is current working directory."),
 		                                               llvm::cl::init("."));
@@ -224,42 +221,9 @@ static bool EvaluateInputAST(const char *Filename,
   if (!success)
     return false;
 
-  // FIXME: Support choice of solver.
-  Solver *coreSolver = NULL; // 
-  
-#ifdef SUPPORT_METASMT
-  if (UseMetaSMT != METASMT_BACKEND_NONE) {
-    
-    std::string backend;
-    
-    switch (UseMetaSMT) {
-          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:
-              assert(false);
-              break;
-    };
-    llvm::errs() << "Starting MetaSMTSolver(" << backend << ") ...\n";
-  }
-  else {
-    coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
-  }
-#else
-  coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver);
-#endif /* SUPPORT_METASMT */
-  
-  
-  if (!UseDummySolver) {
+  Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
+
+  if (CoreSolverToUse != DUMMY_SOLVER) {
     if (0 != MaxCoreSolverTime) {
       coreSolver->setCoreSolverTimeout(MaxCoreSolverTime);
     }
-- 
cgit 1.4.1