From 64868646eed7384c38db41aff5002215b92c1601 Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Fri, 4 Oct 2013 18:32:55 +0100 Subject: MetaSMT builder, solver and command-line options. --- lib/Core/Executor.cpp | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 62 insertions(+), 1 deletion(-) (limited to 'lib/Core/Executor.cpp') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index caf0de36..b2cff8ba 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -105,6 +105,33 @@ using namespace llvm; using namespace klee; + +#ifdef SUPPORT_METASMT + +#include +#include +#include +#include +#include +#include +#include +#include + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + namespace { cl::opt DumpStatesOnHalt("dump-states-on-halt", @@ -268,7 +295,41 @@ Executor::Executor(const InterpreterOptions &opts, : std::max(MaxCoreSolverTime,MaxInstructionTime)) { if (coreSolverTimeout) UseForkedCoreSolver = true; - Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + + 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; + }; + std::cerr << "Starting MetaSMTSolver(" << backend << ") ...\n"; + } + else { + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + } +#else + coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); +#endif /* SUPPORT_METASMT */ + + Solver *solver = constructSolverChain(coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), -- cgit 1.4.1