diff options
| author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2017-10-05 12:05:26 +0200 |
|---|---|---|
| committer | Andrea Mattavelli <andreamattavelli@users.noreply.github.com> | 2017-10-17 22:22:14 +0100 |
| commit | ce39e6e92c27dd59290be18a12ed4cd4c40c01a7 (patch) | |
| tree | 8e3937aa77a66579762cdf4c8dfdb97522f7300d /lib/Solver | |
| parent | 9eb0125f77fdd1f0db2b9769d9fb192d05e43226 (diff) | |
| download | klee-ce39e6e92c27dd59290be18a12ed4cd4c40c01a7.tar.gz | |
[cmake] detect available metaSMT backends using a pre-defined flag and raise compile flags accordingly
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 24 |
1 files changed, 24 insertions, 0 deletions
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; |