diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/kleaver/Makefile | 11 | ||||
| -rw-r--r-- | tools/kleaver/main.cpp | 56 | ||||
| -rw-r--r-- | tools/klee/Makefile | 11 |
3 files changed, 77 insertions, 1 deletions
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index b6ccc91f..b57f8a1f 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -20,3 +20,14 @@ LINK_COMPONENTS = support include $(LEVEL)/Makefile.common LIBS += -lstp + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ + -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ + -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ + -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core -lboost_thread-mt +endif \ No newline at end of file diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index accc48e4..f5bbfaf0 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -45,6 +45,28 @@ using namespace llvm; using namespace klee; using namespace klee::expr; +#ifdef SUPPORT_METASMT + +#include <metaSMT/DirectSolver_Context.hpp> +#include <metaSMT/backend/Z3_Backend.hpp> +#include <metaSMT/backend/Boolector.hpp> + +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + + namespace { llvm::cl::opt<std::string> InputFile(llvm::cl::desc("<input query log>"), llvm::cl::Positional, @@ -211,7 +233,39 @@ static bool EvaluateInputAST(const char *Filename, return false; // FIXME: Support choice of solver. - Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + 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 = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + } +#else + coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); +#endif /* SUPPORT_METASMT */ + if (!UseDummySolver) { if (0 != MaxCoreSolverTime) { diff --git a/tools/klee/Makefile b/tools/klee/Makefile index e1dbefce..e065879e 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -21,3 +21,14 @@ endif include $(LEVEL)/Makefile.common LIBS += -lstp + +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ + -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ + -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ + -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + LIBS += -lrt -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lboolector -lminisat_core -lboost_thread-mt +endif \ No newline at end of file |