From e81f5ceed580d4d267e3c857b47637d6bd065499 Mon Sep 17 00:00:00 2001 From: Dan Liew 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... --- lib/Basic/CmdLineOptions.cpp | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) (limited to 'lib/Basic') 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 queryLoggingOptions( #ifdef SUPPORT_METASMT -llvm::cl::opt -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 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 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)); } -- cgit 1.4.1