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 /cmake | |
| 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 'cmake')
| -rw-r--r-- | cmake/find_metasmt.cmake | 13 |
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 |