From 73614abf37feab15d4558cf65d0ab682ecd2e7f7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 3 Mar 2017 19:39:53 +0000 Subject: [PATCH 1/6] [CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses #915 . --- CMakeLists.txt | 78 +++++++++++++++++++++++++++ README-CMake.md | 1 + contrib/cmake/cmake/Z3Config.cmake.in | 30 +++++++++++ contrib/cmake/src/CMakeLists.txt | 1 + 4 files changed, 110 insertions(+) create mode 100644 contrib/cmake/cmake/Z3Config.cmake.in diff --git a/CMakeLists.txt b/CMakeLists.txt index 8788cdaf4..72ea1143d 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -398,10 +398,18 @@ set(CMAKE_INSTALL_PKGCONFIGDIR PATH "Directory to install pkgconfig files" ) + +set(CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR + "${CMAKE_INSTALL_LIBDIR}/cmake/z3" + CACHE + PATH + "Directory to install Z3 CMake package files" +) message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"") message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"") message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"") message(STATUS "CMAKE_INSTALL_PKGCONFIGDIR: \"${CMAKE_INSTALL_PKGCONFIGDIR}\"") +message(STATUS "CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: \"${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}\"") ################################################################################ # Uninstall rule @@ -449,6 +457,76 @@ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_component.cmake) include(${CMAKE_SOURCE_DIR}/cmake/z3_append_linker_flag_list_to_target.cmake) add_subdirectory(src) +################################################################################ +# Create `Z3Config.cmake` and related files for the build tree so clients can +# use Z3 via CMake. +################################################################################ +include(CMakePackageConfigHelpers) +export(EXPORT Z3_EXPORTED_TARGETS + NAMESPACE z3:: + FILE "${CMAKE_BINARY_DIR}/Z3Targets.cmake" +) +set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_BINARY_DIR}/src/api") +set(Z3_SECOND_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api") +set(Z3_CXX_PACKAGE_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/src/api/c++") +set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT") +set(CONFIG_FILE_TYPE "build tree") +configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in" + "Z3Config.cmake" + INSTALL_DESTINATION "${CMAKE_BINARY_DIR}" + PATH_VARS + Z3_FIRST_PACKAGE_INCLUDE_DIR + Z3_SECOND_PACKAGE_INCLUDE_DIR + Z3_CXX_PACKAGE_INCLUDE_DIR + INSTALL_PREFIX "${CMAKE_BINARY_DIR}" +) +unset(Z3_FIRST_PACKAGE_INCLUDE_DIR) +unset(Z3_SECOND_PACKAGE_INCLUDE_DIR) +unset(Z3_CXX_PACKAGE_INCLUDE_DIR) +unset(AUTO_GEN_MSG) +unset(CONFIG_FILE_TYPE) +# TODO: Provide a `Z3Version.cmake` file so that clients can specify the version +# of Z3 they want. + +################################################################################ +# Create `Z3Config.cmake` and related files for install tree so clients can use +# Z3 via CMake. +################################################################################ +install(EXPORT + Z3_EXPORTED_TARGETS + FILE "Z3Targets.cmake" + NAMESPACE z3:: + DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}" +) +set(Z3_INSTALL_TREE_CMAKE_CONFIG_FILE "${CMAKE_BINARY_DIR}/cmake/Z3Config.cmake") +set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_INSTALL_INCLUDEDIR}") +set(Z3_SECOND_INCLUDE_DIR "") +set(Z3_CXX_PACKAGE_INCLUDE_DIR "") +set(AUTO_GEN_MSG "Automatically generated. DO NOT EDIT") +set(CONFIG_FILE_TYPE "install tree") +# We use `configure_package_config_file()` to try and create CMake files +# that are re-locatable so that it doesn't matter if the files aren't placed +# in the original install prefix. +configure_package_config_file("${CMAKE_SOURCE_DIR}/cmake/Z3Config.cmake.in" + "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}" + INSTALL_DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}" + PATH_VARS Z3_FIRST_PACKAGE_INCLUDE_DIR +) +unset(Z3_FIRST_PACKAGE_INCLUDE_DIR) +unset(Z3_SECOND_PACKAGE_INCLUDE_DIR) +unset(Z3_CXX_PACKAGE_INCLUDE_DIR) +unset(AUTO_GEN_MSG) +unset(CONFIG_FILE_TYPE) + +# Add install rule to install ${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE} +install( + FILES "${Z3_INSTALL_TREE_CMAKE_CONFIG_FILE}" + DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}" +) + +# TODO: Provide a `Z3Version.cmake` file so that clients can specify the version +# of Z3 they want. + ################################################################################ # Examples ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index 2a8317890..6a78b5d4c 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -267,6 +267,7 @@ The following useful options can be passed to CMake whilst configuring. * ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``). * ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files. * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute. +* ``CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR`` - STRING. The path to install CMake package files (e.g. ``/usr/lib/cmake/z3``). * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled. * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library. * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples. diff --git a/contrib/cmake/cmake/Z3Config.cmake.in b/contrib/cmake/cmake/Z3Config.cmake.in new file mode 100644 index 000000000..e7f604591 --- /dev/null +++ b/contrib/cmake/cmake/Z3Config.cmake.in @@ -0,0 +1,30 @@ +################################################################################ +# @AUTO_GEN_MSG@ +# +# This file is intended to be consumed by clients who wish to use Z3 from CMake. +# It can be use by doing `find_package(Z3 config)` from within a +# `CMakeLists.txt` file. If CMake doesn't find this package automatically you +# can give it a hint by passing `-DZ3_DIR=` to the CMake invocation where +# `` is the path to the directory containing this file. +# +# This file was built for the @CONFIG_FILE_TYPE@. +################################################################################ + +# Exported targets +include("${CMAKE_CURRENT_LIST_DIR}/Z3Targets.cmake") + +@PACKAGE_INIT@ + +# Version information +set(Z3_VERSION_MAJOR @Z3_VERSION_MAJOR@) +set(Z3_VERSION_MINOR @Z3_VERSION_MINOR@) +set(Z3_VERSION_PATCH @Z3_VERSION_PATCH@) +set(Z3_VERSION_TWEAK @Z3_VERSION_TWEAK@) +set(Z3_VERSION_STRING "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") + +# NOTE: We can't use `set_and_check()` here because this a list of paths. +# List of include directories +set(Z3_C_INCLUDE_DIRS @PACKAGE_Z3_FIRST_PACKAGE_INCLUDE_DIR@ @PACKAGE_Z3_SECOND_PACKAGE_INCLUDE_DIR@) +set(Z3_CXX_INCLUDE_DIRS @PACKAGE_Z3_CXX_PACKAGE_INCLUDE_DIR@ ${Z3_C_INCLUDE_DIRS}) +# List of libraries to link against +set(Z3_LIBRARIES "z3::libz3") diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 65eef8094..548b59053 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -168,6 +168,7 @@ foreach (header ${libz3_public_headers}) endforeach() install(TARGETS libz3 + EXPORT Z3_EXPORTED_TARGETS LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}" ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" # On Windows this installs ``libz3.lib`` which CMake calls the "corresponding import library". Do we want this installed? RUNTIME DESTINATION "${CMAKE_INSTALL_LIBDIR}" # For Windows. DLLs are runtime targets for CMake From d9617841e085f8d62bafb5a6994db96807aacdcd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 4 Mar 2017 13:07:36 +0000 Subject: [PATCH 2/6] [CMake] Python examples should only be copied over if python bindings are being built. --- contrib/cmake/examples/CMakeLists.txt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/contrib/cmake/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt index e596ed3dd..04df6e6b4 100644 --- a/contrib/cmake/examples/CMakeLists.txt +++ b/contrib/cmake/examples/CMakeLists.txt @@ -1,4 +1,6 @@ add_subdirectory(c) add_subdirectory(c++) add_subdirectory(tptp) -add_subdirectory(python) +if (BUILD_PYTHON_BINDINGS) + add_subdirectory(python) +endif() From db5520c71d1dca4354ad82bbed4a7afad240dca1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 4 Mar 2017 16:45:37 +0000 Subject: [PATCH 3/6] [CMake] Build `c_example`, `cpp_example` and `z3_tptp5` as external projects. This works by giving each example it's own CMake build system and then consuming Z3 via the Z3 CMake config package from the build tree. --- contrib/cmake/examples/CMakeLists.txt | 64 +++++++++++++++++++++- contrib/cmake/examples/c++/CMakeLists.txt | 37 ++++++++++--- contrib/cmake/examples/c/CMakeLists.txt | 35 +++++++++--- contrib/cmake/examples/tptp/CMakeLists.txt | 32 +++++++++-- 4 files changed, 144 insertions(+), 24 deletions(-) diff --git a/contrib/cmake/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt index 04df6e6b4..3fa49f9e0 100644 --- a/contrib/cmake/examples/CMakeLists.txt +++ b/contrib/cmake/examples/CMakeLists.txt @@ -1,6 +1,64 @@ -add_subdirectory(c) -add_subdirectory(c++) -add_subdirectory(tptp) +include(ExternalProject) +# Unfortunately `BUILD_ALWAYS` only seems to be supported with the version of ExternalProject +# that shipped with CMake >= 3.1. +if (("${CMAKE_VERSION}" VERSION_EQUAL "3.1") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.1")) + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG BUILD_ALWAYS 1) +else() + set(EXTERNAL_PROJECT_BUILD_ALWAYS_ARG "") +endif() + +################################################################################ +# Build example project using libz3's C API as an external project +################################################################################ +ExternalProject_Add(c_example + DEPENDS libz3 + # Configure step + SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c" + CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + # Build step + ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/c_example_build_dir" + # Install Step + INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command +) +set_target_properties(c_example PROPERTIES EXCLUDE_FROM_ALL TRUE) + + +################################################################################ +# Build example project using libz3's C++ API as an external project +################################################################################ +ExternalProject_Add(cpp_example + DEPENDS libz3 + # Configure step + SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/c++" + CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + # Build step + ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/cpp_example_build_dir" + # Install Step + INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command +) +set_target_properties(cpp_example PROPERTIES EXCLUDE_FROM_ALL TRUE) + +################################################################################ +# Build example tptp5 project using libz3's C++ API as an external project +################################################################################ +ExternalProject_Add(z3_tptp5 + DEPENDS libz3 + # Configure step + SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/tptp" + CMAKE_ARGS "-DZ3_DIR=${CMAKE_BINARY_DIR}" + # Build step + ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG} + BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/tptp_build_dir" + # Install Step + INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command +) +set_target_properties(z3_tptp5 PROPERTIES EXCLUDE_FROM_ALL TRUE) + +################################################################################ +# Build Python examples +################################################################################ if (BUILD_PYTHON_BINDINGS) add_subdirectory(python) endif() diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt index fdc5cf387..b25bea533 100644 --- a/contrib/cmake/examples/c++/CMakeLists.txt +++ b/contrib/cmake/examples/c++/CMakeLists.txt @@ -1,9 +1,28 @@ -# FIXME: We should build this as an external project and consume -# Z3 as `find_package(z3 CONFIG)`. -add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp) -target_link_libraries(cpp_example PRIVATE libz3) -target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") -target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++") -if (NOT BUILD_LIBZ3_SHARED) - z3_append_linker_flag_list_to_target(cpp_example ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) -endif() +################################################################################ +# Example C++ project +################################################################################ +project(Z3_C_EXAMPLE CXX) +cmake_minimum_required(VERSION 2.8.12) +find_package(Z3 + REQUIRED + CONFIG + # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. + # This should prevent us from accidently picking up an installed + # copy of Z3. This is here to benefit Z3's build sytem when building + # this project. When making your own project you probably shouldn't + # use this option. + NO_DEFAULT_PATH +) +message(STATUS "Z3_FOUND: ${Z3_FOUND}") +message(STATUS "Found Z3 ${Z3_VERSION_STRING}") +message(STATUS "Z3_DIR: ${Z3_DIR}") + +add_executable(cpp_example example.cpp) +target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS}) +target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES}) + +# FIXME: The Z3 package does not export information on the link flags +# This is needed for when libz3 is built as a static library +#if (NOT BUILD_LIBZ3_SHARED) +# z3_append_linker_flag_list_to_target(cpp_example ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +#endif() diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt index fc6eaee18..d51503e29 100644 --- a/contrib/cmake/examples/c/CMakeLists.txt +++ b/contrib/cmake/examples/c/CMakeLists.txt @@ -1,9 +1,28 @@ -# FIXME: We should build this as an external project and consume -# Z3 as `find_package(z3 CONFIG)`. -add_executable(c_example EXCLUDE_FROM_ALL test_capi.c) -target_link_libraries(c_example PRIVATE libz3) -target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") +################################################################################ +# Example C project +################################################################################ +project(Z3_C_EXAMPLE C) +cmake_minimum_required(VERSION 2.8.12) +find_package(Z3 + REQUIRED + CONFIG + # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. + # This should prevent us from accidently picking up an installed + # copy of Z3. This is here to benefit Z3's build sytem when building + # this project. When making your own project you probably shouldn't + # use this option. + NO_DEFAULT_PATH +) +message(STATUS "Z3_FOUND: ${Z3_FOUND}") +message(STATUS "Found Z3 ${Z3_VERSION_STRING}") +message(STATUS "Z3_DIR: ${Z3_DIR}") + +add_executable(c_example test_capi.c) +target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS}) +target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES}) + +# FIXME: The Z3 package does not export information on the link flags # This is needed for when libz3 is built as a static library -if (NOT BUILD_LIBZ3_SHARED) - z3_append_linker_flag_list_to_target(c_example ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}) -endif() +#if (NOT BUILD_LIBZ3_SHARED) +# z3_append_linker_flag_list_to_target(c_example ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}) +#endif() diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/contrib/cmake/examples/tptp/CMakeLists.txt index 41fa9cc65..6a2858a9b 100644 --- a/contrib/cmake/examples/tptp/CMakeLists.txt +++ b/contrib/cmake/examples/tptp/CMakeLists.txt @@ -1,4 +1,28 @@ -add_executable(z3_tptp5 EXCLUDE_FROM_ALL tptp5.cpp tptp5.lex.cpp) -target_link_libraries(z3_tptp5 PRIVATE libz3) -target_include_directories(z3_tptp5 PRIVATE "${CMAKE_SOURCE_DIR}/src/api") -target_include_directories(z3_tptp5 PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++") +################################################################################ +# TPTP example +################################################################################ +project(Z3_TPTP5 CXX) +cmake_minimum_required(VERSION 2.8.12) +find_package(Z3 + REQUIRED + CONFIG + # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3. + # This should prevent us from accidently picking up an installed + # copy of Z3. This is here to benefit Z3's build sytem when building + # this project. When making your own project you probably shouldn't + # use this option. + NO_DEFAULT_PATH +) +message(STATUS "Z3_FOUND: ${Z3_FOUND}") +message(STATUS "Found Z3 ${Z3_VERSION_STRING}") +message(STATUS "Z3_DIR: ${Z3_DIR}") + +add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp) +target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS}) +target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES}) + +# FIXME: The Z3 package does not export information on the link flags +# This is needed for when libz3 is built as a static library +#if (NOT BUILD_LIBZ3_SHARED) +# z3_append_linker_flag_list_to_target(z3_tptp5 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +#endif() From b20bf5169a5f9d7c6e235199b081993f210084c6 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 4 Mar 2017 16:49:19 +0000 Subject: [PATCH 4/6] [CMake] Fix typo handling OpenMP flags. --- CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 72ea1143d..6281f951b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -294,11 +294,11 @@ if (OPENMP_FOUND) # flag by MSVC and breaks the build if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) - list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_C_FLAGS}) + list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) endif() if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU")) - list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_CXX_FLAGS}) + list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_C_FLAGS}) endif() unset(CMAKE_REQUIRED_FLAGS) message(STATUS "Using OpenMP") From ac85c68ccb437590c2e6669d892eef146ba87d65 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 4 Mar 2017 19:01:23 +0000 Subject: [PATCH 5/6] [CMake] Fix examples linking against libz3 when it is built as a static library on Linux. --- CMakeLists.txt | 6 ------ contrib/cmake/examples/c++/CMakeLists.txt | 6 ------ contrib/cmake/examples/c/CMakeLists.txt | 12 +++++------- contrib/cmake/examples/tptp/CMakeLists.txt | 6 ------ contrib/cmake/src/CMakeLists.txt | 8 +++++++- contrib/cmake/src/api/java/CMakeLists.txt | 1 - 6 files changed, 12 insertions(+), 27 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 6281f951b..cf46e7012 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -147,7 +147,6 @@ set(Z3_COMPONENT_CXX_FLAGS "") set(Z3_COMPONENT_EXTRA_INCLUDE_DIRS "") set(Z3_DEPENDENT_LIBS "") set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "") -set(Z3_DEPENDENT_EXTRA_C_LINK_FLAGS "") ################################################################################ # Build type @@ -296,10 +295,6 @@ if (OPENMP_FOUND) ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) endif() - if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR - ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU")) - list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_C_FLAGS}) - endif() unset(CMAKE_REQUIRED_FLAGS) message(STATUS "Using OpenMP") else() @@ -386,7 +381,6 @@ message(STATUS "Z3_COMPONENT_CXX_FLAGS: ${Z3_COMPONENT_CXX_FLAGS}") message(STATUS "Z3_DEPENDENT_LIBS: ${Z3_DEPENDENT_LIBS}") message(STATUS "Z3_COMPONENT_EXTRA_INCLUDE_DIRS: ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}") message(STATUS "Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}") -message(STATUS "Z3_DEPENDENT_EXTRA_C_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}") ################################################################################ # Z3 installation locations diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt index b25bea533..c37aa475d 100644 --- a/contrib/cmake/examples/c++/CMakeLists.txt +++ b/contrib/cmake/examples/c++/CMakeLists.txt @@ -20,9 +20,3 @@ message(STATUS "Z3_DIR: ${Z3_DIR}") add_executable(cpp_example example.cpp) target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS}) target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES}) - -# FIXME: The Z3 package does not export information on the link flags -# This is needed for when libz3 is built as a static library -#if (NOT BUILD_LIBZ3_SHARED) -# z3_append_linker_flag_list_to_target(cpp_example ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) -#endif() diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt index d51503e29..5ca985845 100644 --- a/contrib/cmake/examples/c/CMakeLists.txt +++ b/contrib/cmake/examples/c/CMakeLists.txt @@ -1,7 +1,11 @@ ################################################################################ # Example C project ################################################################################ -project(Z3_C_EXAMPLE C) +# NOTE: Even though this is a C project, libz3 uses C++. When using libz3 +# as a static library if we don't configure this project to also support +# C++ we will use the C linker rather than the C++ linker and will not link +# the C++ standard library in resulting in a link failure. +project(Z3_C_EXAMPLE C CXX) cmake_minimum_required(VERSION 2.8.12) find_package(Z3 REQUIRED @@ -20,9 +24,3 @@ message(STATUS "Z3_DIR: ${Z3_DIR}") add_executable(c_example test_capi.c) target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS}) target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES}) - -# FIXME: The Z3 package does not export information on the link flags -# This is needed for when libz3 is built as a static library -#if (NOT BUILD_LIBZ3_SHARED) -# z3_append_linker_flag_list_to_target(c_example ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}) -#endif() diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/contrib/cmake/examples/tptp/CMakeLists.txt index 6a2858a9b..6cd814487 100644 --- a/contrib/cmake/examples/tptp/CMakeLists.txt +++ b/contrib/cmake/examples/tptp/CMakeLists.txt @@ -20,9 +20,3 @@ message(STATUS "Z3_DIR: ${Z3_DIR}") add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp) target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS}) target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES}) - -# FIXME: The Z3 package does not export information on the link flags -# This is needed for when libz3 is built as a static library -#if (NOT BUILD_LIBZ3_SHARED) -# z3_append_linker_flag_list_to_target(z3_tptp5 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) -#endif() diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 548b59053..66e34790a 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -143,7 +143,13 @@ endif() # so that if those are also shared libraries they are referenced by `libz3.so`. target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS}) -z3_append_linker_flag_list_to_target(libz3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +# This is currently only for the OpenMP flags. It needs to be set +# via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()` +# because when building the `libz3` as a static library when the target is exported +# the link dependencies need to be exported too. +foreach (flag_name ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) + target_link_libraries(libz3 PRIVATE ${flag_name}) +endforeach() # Declare which header file are the public header files of libz3 # these will automatically installed when the libz3 target is installed diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/contrib/cmake/src/api/java/CMakeLists.txt index b34277266..dce2bc4ea 100644 --- a/contrib/cmake/src/api/java/CMakeLists.txt +++ b/contrib/cmake/src/api/java/CMakeLists.txt @@ -44,7 +44,6 @@ target_link_libraries(z3java PRIVATE libz3) # Z3's components to build ``Native.cpp`` lets do the same for now. target_compile_options(z3java PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_compile_definitions(z3java PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) -z3_append_linker_flag_list_to_target(z3java ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) target_include_directories(z3java PRIVATE "${CMAKE_SOURCE_DIR}/src/api" "${CMAKE_BINARY_DIR}/src/api" From 28493622c25e033a2db48bb99a4fba7d12e2fb7e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 13 Mar 2017 12:37:29 +0000 Subject: [PATCH 6/6] [CMake] On Windows when building the examples copy the Z3 library into the directory of the example executable so that it works "out of the box". --- contrib/cmake/examples/c++/CMakeLists.txt | 16 ++++++++++++++++ contrib/cmake/examples/c/CMakeLists.txt | 16 ++++++++++++++++ contrib/cmake/examples/tptp/CMakeLists.txt | 17 +++++++++++++++++ 3 files changed, 49 insertions(+) diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt index c37aa475d..d60604924 100644 --- a/contrib/cmake/examples/c++/CMakeLists.txt +++ b/contrib/cmake/examples/c++/CMakeLists.txt @@ -20,3 +20,19 @@ message(STATUS "Z3_DIR: ${Z3_DIR}") add_executable(cpp_example example.cpp) target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS}) target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES}) + +if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") + # On Windows we need to copy the Z3 libraries + # into the same directory as the executable + # so that they can be found. + foreach (z3_lib ${Z3_LIBRARIES}) + message(STATUS "Adding copy rule for ${z3_lib}") + add_custom_command(TARGET cpp_example + POST_BUILD + COMMAND + ${CMAKE_COMMAND} -E copy_if_different + $ + $ + ) + endforeach() +endif() diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt index 5ca985845..dd8fa6328 100644 --- a/contrib/cmake/examples/c/CMakeLists.txt +++ b/contrib/cmake/examples/c/CMakeLists.txt @@ -24,3 +24,19 @@ message(STATUS "Z3_DIR: ${Z3_DIR}") add_executable(c_example test_capi.c) target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS}) target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES}) + +if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") + # On Windows we need to copy the Z3 libraries + # into the same directory as the executable + # so that they can be found. + foreach (z3_lib ${Z3_LIBRARIES}) + message(STATUS "Adding copy rule for ${z3_lib}") + add_custom_command(TARGET c_example + POST_BUILD + COMMAND + ${CMAKE_COMMAND} -E copy_if_different + $ + $ + ) + endforeach() +endif() diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/contrib/cmake/examples/tptp/CMakeLists.txt index 6cd814487..8e8dfb8ea 100644 --- a/contrib/cmake/examples/tptp/CMakeLists.txt +++ b/contrib/cmake/examples/tptp/CMakeLists.txt @@ -20,3 +20,20 @@ message(STATUS "Z3_DIR: ${Z3_DIR}") add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp) target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS}) target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES}) + +if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows") + # On Windows we need to copy the Z3 libraries + # into the same directory as the executable + # so that they can be found. + foreach (z3_lib ${Z3_LIBRARIES}) + message(STATUS "Adding copy rule for ${z3_lib}") + add_custom_command(TARGET z3_tptp5 + POST_BUILD + COMMAND + ${CMAKE_COMMAND} -E copy_if_different + $ + $ + ) + endforeach() +endif() +