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, 17 insertions, 9 deletions

diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index eac54141..d7157b25 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -75,18 +75,26 @@ llvm::cl::list<QueryLoggingSolverType> queryLoggingOptions(
 
 #ifdef SUPPORT_METASMT
 
-llvm::cl::opt<klee::MetaSMTBackendType>
-UseMetaSMT("use-metasmt",
-           llvm::cl::desc("Use MetaSMT as an underlying SMT solver and specify the solver backend type."),
-           llvm::cl::values(clEnumValN(METASMT_BACKEND_NONE, "none", "Don't use metaSMT"),
-                      clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
-                      clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
-                      clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor", "Use metaSMT with Boolector"),
-                      clEnumValEnd),  
-           llvm::cl::init(METASMT_BACKEND_NONE));
+llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend(
+    "metasmt-backend",
+    llvm::cl::desc("Specify the MetaSMT solver backend type."),
+    llvm::cl::values(
+        clEnumValN(METASMT_BACKEND_STP, "stp", "Use metaSMT with STP"),
+        clEnumValN(METASMT_BACKEND_Z3, "z3", "Use metaSMT with Z3"),
+        clEnumValN(METASMT_BACKEND_BOOLECTOR, "btor",
+                   "Use metaSMT with Boolector"),
+        clEnumValEnd),
+    llvm::cl::init(METASMT_BACKEND_STP));
 
 #endif /* SUPPORT_METASMT */
 
+llvm::cl::opt<CoreSolverType> CoreSolverToUse(
+    "solver-backend", llvm::cl::desc("Specifiy the core solver backend to use"),
+    llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp (default)"),
+                     clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT"),
+                     clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"),
+                     clEnumValEnd),
+    llvm::cl::init(STP_SOLVER));
 }