diff options
-rw-r--r-- | include/klee/Solver.h | 6 | ||||
-rw-r--r-- | lib/Solver/CoreSolver.cpp | 48 | ||||
-rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 33 |
3 files changed, 39 insertions, 48 deletions
diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 32c8cf9e..7f12ddfb 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -253,7 +253,11 @@ namespace klee { virtual char *getConstraintLog(const Query&); virtual void setCoreSolverTimeout(double timeout); -}; + }; + + /// createMetaSMTSolver - Create a solver using the metaSMT backend set by + /// the option MetaSMTBackend. + Solver *createMetaSMTSolver(); #endif /* ENABLE_METASMT */ diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp index d36a3219..72b82807 100644 --- a/lib/Solver/CoreSolver.cpp +++ b/lib/Solver/CoreSolver.cpp @@ -14,52 +14,6 @@ #include "llvm/Support/raw_ostream.h" #include <string> -#ifdef ENABLE_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 klee; -using namespace metaSMT; -using namespace metaSMT::solver; - -static klee::Solver *handleMetaSMT() { - Solver *coreSolver = NULL; - std::string backend; - switch (MetaSMTBackend) { - 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: - llvm_unreachable("Unrecognised MetaSMT backend"); - break; - }; - klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); - return coreSolver; -} -#endif /* ENABLE_METASMT */ - namespace klee { Solver *createCoreSolver(CoreSolverType cst) { @@ -75,7 +29,7 @@ Solver *createCoreSolver(CoreSolverType cst) { case METASMT_SOLVER: #ifdef ENABLE_METASMT klee_message("Using MetaSMT solver backend"); - return handleMetaSMT(); + return createMetaSMTSolver(); #else klee_message("Not compiled with MetaSMT support"); return NULL; diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index a453de40..3b3eaf35 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -17,6 +17,8 @@ #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" +#include "llvm/Support/ErrorHandling.h" + #include <metaSMT/DirectSolver_Context.hpp> #include <metaSMT/backend/Z3_Backend.hpp> #include <metaSMT/backend/Boolector.hpp> @@ -405,5 +407,36 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Boolector> >; template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::Z3_Backend> >; template class MetaSMTSolver<DirectSolver_Context<metaSMT::solver::STP_Backend> >; + +Solver *createMetaSMTSolver() { + using metaSMT::DirectSolver_Context; + using namespace metaSMT::solver; + + Solver *coreSolver = NULL; + std::string backend; + switch (MetaSMTBackend) { + 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: + llvm_unreachable("Unrecognised MetaSMT backend"); + break; + }; + klee_message("Starting MetaSMTSolver(%s)", backend.c_str()); + return coreSolver; +} + } #endif // ENABLE_METASMT |