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