[CMake] Refactor Z3 detection and change the default value of

`ENABLE_SOLVER_Z3` to be set dynamically based on whether Z3 is
available. Previously the default was always off.

2 files changed, 52 insertions, 29 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 325997c2..edd533c3 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -311,35 +311,7 @@ include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
 include(${CMAKE_SOURCE_DIR}/cmake/find_stp.cmake)
 
 # Z3
-option(ENABLE_SOLVER_Z3 "Enable Z3 solver support" OFF)
-if (ENABLE_SOLVER_Z3)
-  message(STATUS "Z3 solver support enabled")
-  find_package(Z3)
-  if (Z3_FOUND)
-    message(STATUS "Found Z3")
-    set(ENABLE_Z3 1) # For config.h
-    list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${Z3_INCLUDE_DIRS})
-    list(APPEND KLEE_SOLVER_LIBRARIES ${Z3_LIBRARIES})
-
-    # Check the signature of `Z3_get_error_msg()`
-    set (_old_CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES}")
-    set(CMAKE_REQUIRED_LIBRARIES ${CMAKE_REQUIRED_LIBRARIES} ${Z3_LIBRARIES})
-    check_prototype_definition(Z3_get_error_msg
-      "Z3_string Z3_get_error_msg(Z3_context c, Z3_error_code err)"
-      "NULL" "${Z3_INCLUDE_DIRS}/z3.h" HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT)
-    set(CMAKE_REQUIRED_LIBRARIES ${_old_CMAKE_REQUIRED_LIBRARIES})
-    if (HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT)
-      message(STATUS "Z3_get_error_msg requires context")
-    else()
-      message(STATUS "Z3_get_error_msg does not require context")
-    endif()
-  else()
-    message(FATAL_ERROR "Z3 not found.")
-  endif()
-else()
-  message(STATUS "Z3 solver support disabled")
-  set(ENABLE_Z3 0) # For config.h
-endif()
+include(${CMAKE_SOURCE_DIR}/cmake/find_z3.cmake)
 
 # metaSMT
 option(ENABLE_SOLVER_METASMT "Enable metaSMT solver support" OFF)
diff --git a/cmake/find_z3.cmake b/cmake/find_z3.cmake
new file mode 100644
index 00000000..60e27c26
--- /dev/null
+++ b/cmake/find_z3.cmake
@@ -0,0 +1,51 @@
+#===------------------------------------------------------------------------===#
+#
+#                     The KLEE Symbolic Virtual Machine
+#
+# This file is distributed under the University of Illinois Open Source
+# License. See LICENSE.TXT for details.
+#
+#===------------------------------------------------------------------------===#
+
+find_package(Z3)
+# Set the default so that if the following is true:
+# * Z3 was found
+# * ENABLE_SOLVER_Z3 is not already set as a cache variable
+#
+# then the default is set to `ON`. Otherwise set the default to `OFF`.
+# A consequence of this is if we fail to detect Z3 the first time
+# subsequent calls to CMake will not change the default.
+if (Z3_FOUND)
+  set(ENABLE_SOLVER_Z3_DEFAULT ON)
+else()
+  set(ENABLE_SOLVER_Z3_DEFAULT OFF)
+endif()
+option(ENABLE_SOLVER_Z3 "Enable Z3 solver support" ${ENABLE_SOLVER_Z3_DEFAULT})
+
+if (ENABLE_SOLVER_Z3)
+  message(STATUS "Z3 solver support enabled")
+  if (Z3_FOUND)
+    message(STATUS "Found Z3")
+    set(ENABLE_Z3 1) # For config.h
+    list(APPEND KLEE_COMPONENT_EXTRA_INCLUDE_DIRS ${Z3_INCLUDE_DIRS})
+    list(APPEND KLEE_SOLVER_LIBRARIES ${Z3_LIBRARIES})
+
+    # Check the signature of `Z3_get_error_msg()`
+    set (_old_CMAKE_REQUIRED_LIBRARIES "${CMAKE_REQUIRED_LIBRARIES}")
+    set(CMAKE_REQUIRED_LIBRARIES ${CMAKE_REQUIRED_LIBRARIES} ${Z3_LIBRARIES})
+    check_prototype_definition(Z3_get_error_msg
+      "Z3_string Z3_get_error_msg(Z3_context c, Z3_error_code err)"
+      "NULL" "${Z3_INCLUDE_DIRS}/z3.h" HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT)
+    set(CMAKE_REQUIRED_LIBRARIES ${_old_CMAKE_REQUIRED_LIBRARIES})
+    if (HAVE_Z3_GET_ERROR_MSG_NEEDS_CONTEXT)
+      message(STATUS "Z3_get_error_msg requires context")
+    else()
+      message(STATUS "Z3_get_error_msg does not require context")
+    endif()
+  else()
+    message(FATAL_ERROR "Z3 not found.")
+  endif()
+else()
+  message(STATUS "Z3 solver support disabled")
+  set(ENABLE_Z3 0) # For config.h
+endif()