diff options
| author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2017-10-05 15:50:21 +0200 |
|---|---|---|
| committer | Andrea Mattavelli <andreamattavelli@users.noreply.github.com> | 2017-10-17 22:22:14 +0100 |
| commit | 9eb0125f77fdd1f0db2b9769d9fb192d05e43226 (patch) | |
| tree | ff3a5e333dbd9becdc57dd9a36f4d85f8590f7b8 | |
| parent | bf5f1b659729dde0378a867ce21426c09490d518 (diff) | |
| download | klee-9eb0125f77fdd1f0db2b9769d9fb192d05e43226.tar.gz | |
add support for CVC4 and Yices2 via metaSMT
| -rw-r--r-- | include/klee/CommandLine.h | 4 | ||||
| -rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 10 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 27 |
3 files changed, 30 insertions, 11 deletions
diff --git a/include/klee/CommandLine.h b/include/klee/CommandLine.h index 79f9286b..9668d00b 100644 --- a/include/klee/CommandLine.h +++ b/include/klee/CommandLine.h @@ -61,7 +61,9 @@ enum MetaSMTBackendType { METASMT_BACKEND_STP, METASMT_BACKEND_Z3, - METASMT_BACKEND_BOOLECTOR + METASMT_BACKEND_BOOLECTOR, + METASMT_BACKEND_CVC4, + METASMT_BACKEND_YICES2 }; extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend; diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index bffd3a4f..aaba72f4 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -112,6 +112,12 @@ void KCommandLine::HideUnrelatedOptions( #elif METASMT_DEFAULT_BACKEND_IS_Z3 #define METASMT_DEFAULT_BACKEND_STR "(default = z3)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_Z3 +#elif METASMT_DEFAULT_BACKEND_IS_CVC4 +#define METASMT_DEFAULT_BACKEND_STR "(default = cvc4)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_CVC4 +#elif METASMT_DEFAULT_BACKEND_IS_YICES2 +#define METASMT_DEFAULT_BACKEND_STR "(default = yices2)." +#define METASMT_DEFAULT_BACKEND METASMT_BACKEND_YICES2 #else #define METASMT_DEFAULT_BACKEND_STR "(default = stp)." #define METASMT_DEFAULT_BACKEND METASMT_BACKEND_STP @@ -123,7 +129,9 @@ MetaSMTBackend("metasmt-backend", 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") + "Use metaSMT with Boolector"), + clEnumValN(METASMT_BACKEND_CVC4, "cvc4", "Use metaSMT with CVC4"), + clEnumValN(METASMT_BACKEND_YICES2, "yices2", "Use metaSMT with Yices2") KLEE_LLVM_CL_VAL_END), cl::init(METASMT_DEFAULT_BACKEND)); diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 9b49f995..9003b119 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -23,14 +23,18 @@ #include <metaSMT/DirectSolver_Context.hpp> #include <metaSMT/backend/Z3_Backend.hpp> #include <metaSMT/backend/Boolector.hpp> +#include <metaSMT/backend/CVC4.hpp> +#include <metaSMT/backend/Yices2.hpp> #define Expr VCExpr #define Type VCType #define STP STP_Backend +#define type_t STP_type_t #include <metaSMT/backend/STP.hpp> #undef Expr #undef Type #undef STP +#undef type_t #include <errno.h> #include <unistd.h> @@ -405,30 +409,35 @@ void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { impl->setCoreSolverTimeout(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; + using namespace metaSMT; Solver *coreSolver = NULL; std::string backend; switch (MetaSMTBackend) { case METASMT_BACKEND_STP: backend = "STP"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<STP_Backend> >( + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::STP_Backend> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; case METASMT_BACKEND_Z3: backend = "Z3"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<Z3_Backend> >( + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; case METASMT_BACKEND_BOOLECTOR: backend = "Boolector"; - coreSolver = new MetaSMTSolver<DirectSolver_Context<Boolector> >( + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Boolector> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_CVC4: + backend = "CVC4"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::CVC4> >( + UseForkedCoreSolver, CoreSolverOptimizeDivides); + break; + case METASMT_BACKEND_YICES2: + backend = "Yices2"; + coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Yices2> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; default: |