1INCLUDE(CheckCXXSourceRuns)
2
3# Function to check Z3's version
4function(check_z3_version z3_include z3_lib)
5  # Get lib path
6  set(z3_link_libs "${z3_lib}")
7
8  # Try to find a threading module in case Z3 was built with threading support.
9  # Threads are required elsewhere in LLVM, but not marked as required here because
10  # Z3 could have been compiled without threading support.
11  find_package(Threads)
12  # CMAKE_THREAD_LIBS_INIT may be empty if the thread functions are provided by the
13  # system libraries and no special flags are needed.
14  if(CMAKE_THREAD_LIBS_INIT)
15    list(APPEND z3_link_libs "${CMAKE_THREAD_LIBS_INIT}")
16  endif()
17
18  # The program that will be executed to print Z3's version.
19  file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
20       "#include <assert.h>
21        #include <stdio.h>
22        #include <z3.h>
23        int main(void) {
24          unsigned int major, minor, build, rev;
25          Z3_get_version(&major, &minor, &build, &rev);
26          printf(\"%u.%u.%u\", major, minor, build);
27          return 0;
28       }")
29
30  try_run(
31    Z3_RETURNCODE
32    Z3_COMPILED
33    ${CMAKE_BINARY_DIR}
34    ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.cpp
35    COMPILE_DEFINITIONS -I"${z3_include}"
36    LINK_LIBRARIES ${z3_link_libs}
37    COMPILE_OUTPUT_VARIABLE COMPILE_OUTPUT
38    RUN_OUTPUT_VARIABLE SRC_OUTPUT
39  )
40
41  if(Z3_COMPILED)
42    string(REGEX REPLACE "([0-9]+\\.[0-9]+\\.[0-9]+)" "\\1"
43           z3_version "${SRC_OUTPUT}")
44    set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)
45  else()
46    message(NOTICE "${COMPILE_OUTPUT}")
47    message(WARNING "Failed to compile Z3 program that is used to determine library version.")
48  endif()
49endfunction(check_z3_version)
50
51# Looking for Z3 in LLVM_Z3_INSTALL_DIR
52find_path(Z3_INCLUDE_DIR NAMES z3.h
53  NO_DEFAULT_PATH
54  PATHS ${LLVM_Z3_INSTALL_DIR}/include
55  PATH_SUFFIXES libz3 z3
56  )
57
58find_library(Z3_LIBRARIES NAMES z3 libz3
59  NO_DEFAULT_PATH
60  PATHS ${LLVM_Z3_INSTALL_DIR}
61  PATH_SUFFIXES lib bin
62  )
63
64# If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories
65find_path(Z3_INCLUDE_DIR NAMES z3.h
66  PATH_SUFFIXES libz3 z3
67  )
68
69find_library(Z3_LIBRARIES NAMES z3 libz3
70  PATH_SUFFIXES lib bin
71  )
72
73# Searching for the version of the Z3 library is a best-effort task
74unset(Z3_VERSION_STRING)
75
76# First, try to check it dynamically, by compiling a small program that
77# prints Z3's version
78if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND NOT CMAKE_CROSSCOMPILING)
79  # We do not have the Z3 binary to query for a version. Try to use
80  # a small C++ program to detect it via the Z3_get_version() API call.
81  check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES})
82endif()
83
84# If the dynamic check fails, we might be cross compiling: if that's the case,
85# check the version in the headers, otherwise, fail with a message
86if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
87                              Z3_INCLUDE_DIR AND
88                              EXISTS "${Z3_INCLUDE_DIR}/z3_version.h"))
89  # TODO: print message warning that we couldn't find a compatible lib?
90
91  # Z3 4.8.1+ has the version is in a public header.
92  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
93       z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*")
94  string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]+).*$" "\\1"
95         Z3_MAJOR "${z3_version_str}")
96
97  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
98       z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*")
99  string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]+).*$" "\\1"
100         Z3_MINOR "${z3_version_str}")
101
102  file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
103       z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*")
104  string(REGEX REPLACE "^.*Z3_BUILD_NUMBER[\t ]+([0-9]+).*$" "\\1"
105         Z3_BUILD "${z3_version_str}")
106
107  set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD})
108  unset(z3_version_str)
109endif()
110
111if(NOT Z3_VERSION_STRING)
112  # Give up: we are unable to obtain a version of the Z3 library. Be
113  # conservative and force the found version to 0.0.0 to make version
114  # checks always fail.
115  set(Z3_VERSION_STRING "0.0.0")
116  message(WARNING "Failed to determine Z3 library version, defaulting to 0.0.0.")
117endif()
118
119# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
120# all listed variables are TRUE
121include(FindPackageHandleStandardArgs)
122FIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3
123                                  REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
124                                  VERSION_VAR Z3_VERSION_STRING)
125
126mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)
127