From ce39e6e92c27dd59290be18a12ed4cd4c40c01a7 Mon Sep 17 00:00:00 2001
From: "Hoang M. Le" <hle@informatik.uni-bremen.de>
Date: Thu, 5 Oct 2017 12:05:26 +0200
Subject: [cmake] detect available metaSMT backends using a pre-defined flag
 and raise compile flags accordingly

---
 cmake/find_metasmt.cmake | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'cmake')

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
-- 
cgit 1.4.1