diff options
| -rw-r--r-- | cmake/find_metasmt.cmake | 13 | ||||
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 24 |
2 files changed, 35 insertions, 2 deletions
diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake index 39079e2b..3dc9fe50 100644 --- a/cmake/find_metasmt.cmake +++ b/cmake/find_metasmt.cmake @@ -62,7 +62,13 @@ if (ENABLE_SOLVER_METASMT) klee_component_add_cxx_flag(${f} REQUIRED) endforeach() - set(available_metasmt_backends "BTOR" "STP" "Z3") + # Check if metaSMT provides an useable backend + if (NOT metaSMT_AVAILABLE_QF_ABV_SOLVERS) + message(FATAL_ERROR "metaSMT does not provide an useable backend.") + endif() + + message(STATUS "metaSMT has the following backend(s): ${metaSMT_AVAILABLE_QF_ABV_SOLVERS}.") + set(available_metasmt_backends ${metaSMT_AVAILABLE_QF_ABV_SOLVERS}) set(METASMT_DEFAULT_BACKEND "STP" CACHE STRING @@ -79,9 +85,12 @@ if (ENABLE_SOLVER_METASMT) "Valid values are ${available_metasmt_backends}") endif() - # Set appropriate define + # Set appropriate defines list(APPEND KLEE_COMPONENT_CXX_DEFINES -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND}) + foreach(backend ${available_metasmt_backends}) + list(APPEND KLEE_COMPONENT_CXX_DEFINES -DMETASMT_HAVE_${backend}) + endforeach() else() message(STATUS "metaSMT solver support disabled") set(ENABLE_METASMT 0) # For config.h diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 9003b119..695c408b 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -21,11 +21,24 @@ #include "llvm/Support/ErrorHandling.h" #include <metaSMT/DirectSolver_Context.hpp> + +#ifdef METASMT_HAVE_Z3 #include <metaSMT/backend/Z3_Backend.hpp> +#endif + +#ifdef METASMT_HAVE_BTOR #include <metaSMT/backend/Boolector.hpp> +#endif + +#ifdef METASMT_HAVE_CVC4 #include <metaSMT/backend/CVC4.hpp> +#endif + +#ifdef METASMT_HAVE_YICES2 #include <metaSMT/backend/Yices2.hpp> +#endif +#ifdef METASMT_HAVE_STP #define Expr VCExpr #define Type VCType #define STP STP_Backend @@ -35,6 +48,7 @@ #undef Type #undef STP #undef type_t +#endif #include <errno.h> #include <unistd.h> @@ -415,31 +429,41 @@ Solver *createMetaSMTSolver() { Solver *coreSolver = NULL; std::string backend; switch (MetaSMTBackend) { +#ifdef METASMT_HAVE_STP case METASMT_BACKEND_STP: backend = "STP"; coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::STP_Backend> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; +#endif +#ifdef METASMT_HAVE_Z3 case METASMT_BACKEND_Z3: backend = "Z3"; coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Z3_Backend> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; +#endif +#ifdef METASMT_HAVE_BTOR case METASMT_BACKEND_BOOLECTOR: backend = "Boolector"; coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Boolector> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; +#endif +#ifdef METASMT_HAVE_CVC4 case METASMT_BACKEND_CVC4: backend = "CVC4"; coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::CVC4> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; +#endif +#ifdef METASMT_HAVE_YICES2 case METASMT_BACKEND_YICES2: backend = "Yices2"; coreSolver = new MetaSMTSolver<DirectSolver_Context<solver::Yices2> >( UseForkedCoreSolver, CoreSolverOptimizeDivides); break; +#endif default: llvm_unreachable("Unrecognised MetaSMT backend"); break; |