From 785dbbdcdbb5694e62c18e57c257cf89e7eb94a2 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 30 Aug 2018 18:30:23 +0200
Subject: [PATCH] CMake version parsing of z3 without z3 binary
---
resources/3rdparty/CMakeLists.txt | 53 ++++++++++++------------
resources/3rdparty/z3/output_version.cpp | 9 ++++
2 files changed, 35 insertions(+), 27 deletions(-)
create mode 100644 resources/3rdparty/z3/output_version.cpp
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index f52ae7f3d..472560abe 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -141,46 +141,45 @@ find_package(Z3 QUIET)
# Z3 Defines
set(STORM_HAVE_Z3 ${Z3_FOUND})
+
if(Z3_FOUND)
- # Check whether the version of z3 supports optimization
- if (Z3_EXEC)
- execute_process (COMMAND ${Z3_EXEC} -version
- OUTPUT_VARIABLE z3_version_output
- ERROR_QUIET
- OUTPUT_STRIP_TRAILING_WHITESPACE)
+ # Get the z3 version by compiling and running a simple program
+ try_run(version_run_result version_compile_result "${STORM_3RDPARTY_BINARY_DIR}/z3/" "${PROJECT_SOURCE_DIR}/resources/3rdparty/z3/output_version.cpp" LINK_LIBRARIES "${Z3_LIBRARIES}" RUN_OUTPUT_VARIABLE z3_version_output)
+ if (version_compile_result AND version_run_result EQUAL 0)
if (z3_version_output MATCHES "([0-9]*\\.[0-9]*\\.[0-9]*)")
set(Z3_VERSION "${CMAKE_MATCH_1}")
- if(NOT "${Z3_VERSION}" VERSION_LESS "4.5.0")
- set(STORM_HAVE_Z3_OPTIMIZE ON)
- endif()
endif()
endif()
- if(STORM_HAVE_Z3_OPTIMIZE)
- message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version supports optimization)")
+ if(Z3_VERSION)
+ # Split Z3 version into its components
+ string(REPLACE "." ";" Z3_VERSION_LIST ${Z3_VERSION})
+ list(GET Z3_VERSION_LIST 0 STORM_Z3_VERSION_MAJOR)
+ list(GET Z3_VERSION_LIST 1 STORM_Z3_VERSION_MINOR)
+ list(GET Z3_VERSION_LIST 2 STORM_Z3_VERSION_PATCH)
+
+ # Check whether the version of z3 supports optimization
+ if(NOT "${Z3_VERSION}" VERSION_LESS "4.5.0")
+ set(STORM_HAVE_Z3_OPTIMIZE ON)
+ message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version supports optimization)")
+ else()
+ message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version does not support optimization)")
+ endif()
+ if (NOT "${Z3_VERSION}" VERSION_LESS "4.7.1")
+ set(STORM_Z3_API_USES_STANDARD_INTEGERS ON)
+ endif()
+
+ add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS})
+ list(APPEND STORM_DEP_TARGETS z3_SHARED)
else()
- message (STATUS "Storm - Linking with Z3 (version ${Z3_VERSION}). (Z3 version does not support optimization)")
+ message(WARNING "Storm - Could not obtain Z3 version. Building of Prism/JANI models will not be supported.")
+ set(Z3_FOUND FALSE)
endif()
- add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS})
- list(APPEND STORM_DEP_TARGETS z3_SHARED)
else()
message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.")
endif(Z3_FOUND)
-# split Z3 version into its components
-if(Z3_VERSION)
- string(REPLACE "." ";" Z3_VERSION_LIST ${Z3_VERSION})
- list(GET Z3_VERSION_LIST 0 STORM_Z3_VERSION_MAJOR)
- list(GET Z3_VERSION_LIST 1 STORM_Z3_VERSION_MINOR)
- list(GET Z3_VERSION_LIST 2 STORM_Z3_VERSION_PATCH)
- if (NOT "${Z3_VERSION}" VERSION_LESS "4.7.1")
- set(STORM_Z3_API_USES_STANDARD_INTEGERS ON)
- endif()
-else()
- message(WARNING "Storm - Could not obtain Z3 version. Do you have the binary installed?. Building of Prism/JANI models will not be supported.")
- set(Z3_FOUND FALSE)
-endif()
#############################################################
##
diff --git a/resources/3rdparty/z3/output_version.cpp b/resources/3rdparty/z3/output_version.cpp
new file mode 100644
index 000000000..3f631199e
--- /dev/null
+++ b/resources/3rdparty/z3/output_version.cpp
@@ -0,0 +1,9 @@
+#include <iostream>
+#include <z3.h>
+
+int main() {
+ unsigned major, minor, build_number, revision_number;
+ Z3_get_version(&major, &minor, &build_number, &revision_number);
+ std::cout << major << "." << minor << "." << build_number << std::endl;
+ return 0;
+}