[cmake] detect available metaSMT backends using a pre-defined flag and raise compile flags accordingly

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;