106f32e7eSjoergINCLUDE(CheckCXXSourceRuns) 206f32e7eSjoerg 306f32e7eSjoerg# Function to check Z3's version 406f32e7eSjoergfunction(check_z3_version z3_include z3_lib) 506f32e7eSjoerg # The program that will be executed to print Z3's version. 606f32e7eSjoerg file(WRITE ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c 706f32e7eSjoerg "#include <assert.h> 806f32e7eSjoerg #include <z3.h> 906f32e7eSjoerg int main() { 1006f32e7eSjoerg unsigned int major, minor, build, rev; 1106f32e7eSjoerg Z3_get_version(&major, &minor, &build, &rev); 1206f32e7eSjoerg printf(\"%u.%u.%u\", major, minor, build); 1306f32e7eSjoerg return 0; 1406f32e7eSjoerg }") 1506f32e7eSjoerg 1606f32e7eSjoerg # Get lib path 1706f32e7eSjoerg get_filename_component(z3_lib_path ${z3_lib} PATH) 1806f32e7eSjoerg 1906f32e7eSjoerg try_run( 2006f32e7eSjoerg Z3_RETURNCODE 2106f32e7eSjoerg Z3_COMPILED 2206f32e7eSjoerg ${CMAKE_BINARY_DIR} 2306f32e7eSjoerg ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c 2406f32e7eSjoerg COMPILE_DEFINITIONS -I"${z3_include}" 2506f32e7eSjoerg LINK_LIBRARIES -L${z3_lib_path} -lz3 2606f32e7eSjoerg RUN_OUTPUT_VARIABLE SRC_OUTPUT 2706f32e7eSjoerg ) 2806f32e7eSjoerg 2906f32e7eSjoerg if(Z3_COMPILED) 30*da58b97aSjoerg string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*)" "\\1" 3106f32e7eSjoerg z3_version "${SRC_OUTPUT}") 3206f32e7eSjoerg set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE) 3306f32e7eSjoerg endif() 3406f32e7eSjoergendfunction(check_z3_version) 3506f32e7eSjoerg 3606f32e7eSjoerg# Looking for Z3 in LLVM_Z3_INSTALL_DIR 3706f32e7eSjoergfind_path(Z3_INCLUDE_DIR NAMES z3.h 3806f32e7eSjoerg NO_DEFAULT_PATH 3906f32e7eSjoerg PATHS ${LLVM_Z3_INSTALL_DIR}/include 4006f32e7eSjoerg PATH_SUFFIXES libz3 z3 4106f32e7eSjoerg ) 4206f32e7eSjoerg 4306f32e7eSjoergfind_library(Z3_LIBRARIES NAMES z3 libz3 4406f32e7eSjoerg NO_DEFAULT_PATH 4506f32e7eSjoerg PATHS ${LLVM_Z3_INSTALL_DIR} 4606f32e7eSjoerg PATH_SUFFIXES lib bin 4706f32e7eSjoerg ) 4806f32e7eSjoerg 4906f32e7eSjoerg# If Z3 has not been found in LLVM_Z3_INSTALL_DIR look in the default directories 5006f32e7eSjoergfind_path(Z3_INCLUDE_DIR NAMES z3.h 5106f32e7eSjoerg PATH_SUFFIXES libz3 z3 5206f32e7eSjoerg ) 5306f32e7eSjoerg 5406f32e7eSjoergfind_library(Z3_LIBRARIES NAMES z3 libz3 5506f32e7eSjoerg PATH_SUFFIXES lib bin 5606f32e7eSjoerg ) 5706f32e7eSjoerg 5806f32e7eSjoerg# Searching for the version of the Z3 library is a best-effort task 5906f32e7eSjoergunset(Z3_VERSION_STRING) 6006f32e7eSjoerg 6106f32e7eSjoerg# First, try to check it dynamically, by compiling a small program that 6206f32e7eSjoerg# prints Z3's version 6306f32e7eSjoergif(Z3_INCLUDE_DIR AND Z3_LIBRARIES) 6406f32e7eSjoerg # We do not have the Z3 binary to query for a version. Try to use 6506f32e7eSjoerg # a small C++ program to detect it via the Z3_get_version() API call. 6606f32e7eSjoerg check_z3_version(${Z3_INCLUDE_DIR} ${Z3_LIBRARIES}) 6706f32e7eSjoergendif() 6806f32e7eSjoerg 6906f32e7eSjoerg# If the dynamic check fails, we might be cross compiling: if that's the case, 7006f32e7eSjoerg# check the version in the headers, otherwise, fail with a message 7106f32e7eSjoergif(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND 7206f32e7eSjoerg Z3_INCLUDE_DIR AND 7306f32e7eSjoerg EXISTS "${Z3_INCLUDE_DIR}/z3_version.h")) 7406f32e7eSjoerg # TODO: print message warning that we couldn't find a compatible lib? 7506f32e7eSjoerg 7606f32e7eSjoerg # Z3 4.8.1+ has the version is in a public header. 7706f32e7eSjoerg file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" 7806f32e7eSjoerg z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*") 7906f32e7eSjoerg string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]).*$" "\\1" 8006f32e7eSjoerg Z3_MAJOR "${z3_version_str}") 8106f32e7eSjoerg 8206f32e7eSjoerg file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" 8306f32e7eSjoerg z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*") 8406f32e7eSjoerg string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]).*$" "\\1" 8506f32e7eSjoerg Z3_MINOR "${z3_version_str}") 8606f32e7eSjoerg 8706f32e7eSjoerg file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" 8806f32e7eSjoerg z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*") 8906f32e7eSjoerg string(REGEX REPLACE "^.*Z3_BUILD_VERSION[\t ]+([0-9]).*$" "\\1" 9006f32e7eSjoerg Z3_BUILD "${z3_version_str}") 9106f32e7eSjoerg 9206f32e7eSjoerg set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD}) 9306f32e7eSjoerg unset(z3_version_str) 9406f32e7eSjoergendif() 9506f32e7eSjoerg 9606f32e7eSjoergif(NOT Z3_VERSION_STRING) 9706f32e7eSjoerg # Give up: we are unable to obtain a version of the Z3 library. Be 9806f32e7eSjoerg # conservative and force the found version to 0.0.0 to make version 9906f32e7eSjoerg # checks always fail. 10006f32e7eSjoerg set(Z3_VERSION_STRING "0.0.0") 10106f32e7eSjoergendif() 10206f32e7eSjoerg 10306f32e7eSjoerg# handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if 10406f32e7eSjoerg# all listed variables are TRUE 10506f32e7eSjoerginclude(FindPackageHandleStandardArgs) 10606f32e7eSjoergFIND_PACKAGE_HANDLE_STANDARD_ARGS(Z3 10706f32e7eSjoerg REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR 10806f32e7eSjoerg VERSION_VAR Z3_VERSION_STRING) 10906f32e7eSjoerg 11006f32e7eSjoergmark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES) 111