From db5520c71d1dca4354ad82bbed4a7afad240dca1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 4 Mar 2017 16:45:37 +0000 Subject: [PATCH] [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()