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...
---
 include/klee/CommandLine.h | 6 ++++--
 include/klee/Solver.h      | 5 ++++-
 2 files changed, 8 insertions(+), 3 deletions(-)

(limited to 'include')

diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h
index c4c70069..44f1afd4 100644
--- a/include/klee/CommandLine.h
+++ b/include/klee/CommandLine.h
@@ -44,17 +44,19 @@ enum QueryLoggingSolverType
  */
 extern llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions;
 
+enum CoreSolverType { STP_SOLVER, METASMT_SOLVER, DUMMY_SOLVER };
+extern llvm::cl::opt<CoreSolverType> CoreSolverToUse;
+
 #ifdef SUPPORT_METASMT
 
 enum MetaSMTBackendType
 {
-    METASMT_BACKEND_NONE,
     METASMT_BACKEND_STP,
     METASMT_BACKEND_Z3,
     METASMT_BACKEND_BOOLECTOR
 };
 
-extern llvm::cl::opt<klee::MetaSMTBackendType> UseMetaSMT;
+extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
 
 #endif /* SUPPORT_METASMT */
 
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index 906309d2..e3adac6a 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_SOLVER_H
 #define KLEE_SOLVER_H
 
+#include "klee/CommandLine.h" // FIXME: This is just for CoreSolverType
 #include "klee/Expr.h"
 
 #include <vector>
@@ -290,7 +291,9 @@ namespace klee {
   /// createDummySolver - Create a dummy solver implementation which always
   /// fails.
   Solver *createDummySolver();
-  
+
+  // Create a solver based on the supplied ``CoreSolverType``.
+  Solver *createCoreSolver(CoreSolverType cst);
 }
 
 #endif
-- 
cgit 1.4.1