From 8a7705ad979096d4e611fb2b8b397c48dd5fffc1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 20:14:01 +0000 Subject: Make it possible to build KLEE without using STP and only MetaSMT. The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency. --- lib/Basic/CmdLineOptions.cpp | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) (limited to 'lib/Basic') diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index d7157b25..2f97b200 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -73,7 +73,7 @@ llvm::cl::list queryLoggingOptions( llvm::cl::CommaSeparated ); -#ifdef SUPPORT_METASMT +#ifdef ENABLE_METASMT llvm::cl::opt MetaSMTBackend( "metasmt-backend", @@ -86,16 +86,31 @@ llvm::cl::opt MetaSMTBackend( clEnumValEnd), llvm::cl::init(METASMT_BACKEND_STP)); -#endif /* SUPPORT_METASMT */ - +#endif /* ENABLE_METASMT */ + +// Pick the default core solver based on configuration +#ifdef ENABLE_STP +#define STP_IS_DEFAULT_STR " (default)" +#define METASMT_IS_DEFAULT_STR "" +#define DEFAULT_CORE_SOLVER STP_SOLVER +#elif ENABLE_METASMT +#define STP_IS_DEFAULT_STR "" +#define METASMT_IS_DEFAULT_STR " (default)" +#define DEFAULT_CORE_SOLVER METASMT_SOLVER +#else +#error "Unsupported solver configuration" +#endif 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"), + llvm::cl::values(clEnumValN(STP_SOLVER, "stp", "stp" STP_IS_DEFAULT_STR), + clEnumValN(METASMT_SOLVER, "metasmt", "metaSMT" METASMT_IS_DEFAULT_STR), clEnumValN(DUMMY_SOLVER, "dummy", "Dummy solver"), clEnumValEnd), - llvm::cl::init(STP_SOLVER)); + llvm::cl::init(DEFAULT_CORE_SOLVER)); } +#undef STP_IS_DEFAULT_STR +#undef METASMT_IS_DEFAULT_STR +#undef DEFAULT_CORE_SOLVER -- cgit 1.4.1