about summary refs log tree commit diff homepage
path: root/cmake/find_metasmt.cmake
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2017-10-05 12:05:26 +0200
committerAndrea Mattavelli <andreamattavelli@users.noreply.github.com>2017-10-17 22:22:14 +0100
commitce39e6e92c27dd59290be18a12ed4cd4c40c01a7 (patch)
tree8e3937aa77a66579762cdf4c8dfdb97522f7300d /cmake/find_metasmt.cmake
parent9eb0125f77fdd1f0db2b9769d9fb192d05e43226 (diff)
downloadklee-ce39e6e92c27dd59290be18a12ed4cd4c40c01a7.tar.gz
[cmake] detect available metaSMT backends using a pre-defined flag and raise compile flags accordingly
Diffstat (limited to 'cmake/find_metasmt.cmake')
-rw-r--r--cmake/find_metasmt.cmake13
1 files changed, 11 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