[CMake] Use z3::libz3 as the preferred way to consume Z3 (#10733)

In #10717 we enhanced the CMake package to support multiple build
configurations, so that Z3 could be installed and consumed as either a
static or shared package, or both side by side. This PR dog-foods that
work: the Python bindings and the example projects now consume Z3
through the same installed CMake package that external users rely on,
rather than through separate in-tree plumbing.

To make that possible, we introduce a `z3::libz3` ALIAS that mirrors the
installed target in-tree. In-tree consumers (like the examples and the
Python bindings) and out-of-tree consumers of the installed package now
refer to Z3 the same way, so now there's one blessed interface. The
examples and package-consumer test were updated accordingly, both to
exercise this path and to serve as a model for how downstream projects
should consume Z3 going forward.

Finally, we add test coverage for the reworked Python build, including a
CI job that installs a shared build of libz3 and then builds the Python
bindings against that installed package, confirming the Python-only
build path works end to end.

.github/workflows/ci.yml

@@ -454,6 +454,15 @@ jobs:
           cmake --build build --target libz3 shell
           cmake --install build --prefix "$PWD/install"
 
+      - name: Build Python bindings from installed shared package
+        run: |
+          cmake -S . -B build-python-only -G Ninja \
+            -DZ3_BUILD_LIBZ3_CORE=OFF \
+            -DZ3_BUILD_PYTHON_BINDINGS=ON \
+            -DZ3_INSTALL_PYTHON_BINDINGS=OFF \
+            -DCMAKE_PREFIX_PATH="$PWD/install"
+          cmake --build build-python-only --target build_z3_python_bindings
+
       - name: Setup consumer CMake
         uses: jwlawson/actions-setup-cmake@v2
         with:

CMakeLists.txt

@@ -592,26 +592,26 @@ if (Z3_BUILD_LIBZ3_CORE)
      FILE "${PROJECT_BINARY_DIR}/Z3-${Z3_LIBZ3_VARIANT}-targets.cmake"
   )
 else()
-  # When not building libz3, we need to find it
-  message(STATUS "Not building libz3, will look for pre-installed library")
-  find_library(Z3_LIBRARY NAMES z3 libz3
-    HINTS ${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR}
-    PATH_SUFFIXES lib lib64
-  )
-  if (NOT Z3_LIBRARY)
-    message(FATAL_ERROR "Could not find pre-installed libz3. Please ensure libz3 is installed or set Z3_BUILD_LIBZ3_CORE=ON")
-  endif()
-  message(STATUS "Found libz3: ${Z3_LIBRARY}")
+  message(STATUS "Not building libz3; looking for the installed Z3 package")
+  # CMake 3.16 has no block() scope. Preserve the project version variables
+  # around find_package(), which otherwise writes the same names.
+  set(_z3_project_version "${Z3_VERSION}")
+  set(_z3_project_version_major "${Z3_VERSION_MAJOR}")
+  set(_z3_project_version_minor "${Z3_VERSION_MINOR}")
+  set(_z3_project_version_patch "${Z3_VERSION_PATCH}")
+  find_package(Z3 ${Z3_VERSION} EXACT CONFIG REQUIRED COMPONENTS shared)
+  set(Z3_VERSION "${_z3_project_version}")
+  set(Z3_VERSION_MAJOR "${_z3_project_version_major}")
+  set(Z3_VERSION_MINOR "${_z3_project_version_minor}")
+  set(Z3_VERSION_PATCH "${_z3_project_version_patch}")
+  unset(_z3_project_version)
+  unset(_z3_project_version_major)
+  unset(_z3_project_version_minor)
+  unset(_z3_project_version_patch)
+endif()
 
-  # Create an imported target for the pre-installed libz3
-  add_library(libz3 SHARED IMPORTED)
-  set_target_properties(libz3 PROPERTIES
-    IMPORTED_LOCATION "${Z3_LIBRARY}"
-  )
-  # Set include directories for the imported target
-  target_include_directories(libz3 INTERFACE
-    ${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_INCLUDEDIR}
-  )
+if (TARGET libz3 AND NOT TARGET z3::libz3)
+  add_library(z3::libz3 ALIAS libz3)
 endif()
 
 ################################################################################
@@ -671,13 +671,12 @@ configure_file(
 unset(Z3_FIND_GMP_MODULE_DIR)
 
 configure_file("${CMAKE_CURRENT_SOURCE_DIR}/z3.pc.cmake.in"
-	"${CMAKE_CURRENT_BINARY_DIR}/z3.pc" @ONLY)
+  "${CMAKE_CURRENT_BINARY_DIR}/z3.pc" @ONLY)
 
 ################################################################################
 # Create `Z3Config.cmake` and related files for install tree so clients can use
 # Z3 via CMake.
 ################################################################################
-# Only install targets if we built libz3
 if (Z3_BUILD_LIBZ3_CORE)
   install(EXPORT
     Z3_EXPORTED_TARGETS
@@ -718,30 +717,32 @@ 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}"
-)
+if (Z3_BUILD_LIBZ3_CORE)
+  # 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}"
+  )
 
-# Add install rule to install ${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake
-install(
-  FILES "${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake"
-  DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
-)
+  # Add install rule to install ${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake
+  install(
+    FILES "${PROJECT_BINARY_DIR}/Z3ConfigVersion.cmake"
+    DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
+  )
 
-# Add install rule to install ${PROJECT_BINARY_DIR}/z3.pc
-install(
-  FILES "${PROJECT_BINARY_DIR}/z3.pc"
-  DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}"
-)
+  # Add install rule to install ${PROJECT_BINARY_DIR}/z3.pc
+  install(
+    FILES "${PROJECT_BINARY_DIR}/z3.pc"
+    DESTINATION "${CMAKE_INSTALL_PKGCONFIGDIR}"
+  )
+endif()
 
 ################################################################################
 # Examples
 ################################################################################
 cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS
     "Build Z3 api examples" ON
-    "CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
+    "CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR;Z3_BUILD_LIBZ3_CORE" OFF)
 if (Z3_ENABLE_EXAMPLE_TARGETS)
   add_subdirectory(examples)
 endif()

cmake/tests/package/CMakeLists.txt

@@ -1,6 +1,6 @@
 cmake_minimum_required(VERSION 3.5)
 
-project(Z3_PACKAGE_TEST LANGUAGES CXX)
+project(Z3_PACKAGE_TEST LANGUAGES C CXX)
 
 set(Z3_TEST_COMPONENT "" CACHE STRING
   "Z3 package component to request (static or shared)")
@@ -33,6 +33,14 @@ if (Z3_TEST_CONFLICTING_COMPONENT)
     message(FATAL_ERROR "A conflicting package request replaced z3::libz3")
   endif()
 endif()
+
+get_target_property(_z3_compile_features
+  z3::libz3 INTERFACE_COMPILE_FEATURES)
+list(FIND _z3_compile_features cxx_noexcept _z3_cxx11_feature_index)
+if (_z3_cxx11_feature_index EQUAL -1)
+  message(FATAL_ERROR "z3::libz3 does not require C++11")
+endif()
+
 if (Z3_TEST_EXPECTED_TYPE)
   get_target_property(_z3_actual_type z3::libz3 TYPE)
   if (NOT _z3_actual_type STREQUAL Z3_TEST_EXPECTED_TYPE)
@@ -50,5 +58,9 @@ endif()
 add_executable(z3_package_test package_test.cpp)
 target_link_libraries(z3_package_test PRIVATE z3::libz3)
 
+add_executable(z3_package_c_test package_test.c)
+target_link_libraries(z3_package_c_test PRIVATE z3::libz3)
+
 enable_testing()
 add_test(NAME z3_package_test COMMAND z3_package_test)
+add_test(NAME z3_package_c_test COMMAND z3_package_c_test)

cmake/tests/package/package_test.c

@@ -0,0 +1,7 @@
+#include <z3.h>
+
+int main(void) {
+    unsigned major, minor, build, revision;
+    Z3_get_version(&major, &minor, &build, &revision);
+    return 0;
+}

examples/c++/CMakeLists.txt

@@ -1,8 +1,8 @@
 ################################################################################
 # Example C++ project
 ################################################################################
-project(Z3_C_EXAMPLE CXX)
-cmake_minimum_required(VERSION 3.4)
+cmake_minimum_required(VERSION 3.5)
+project(Z3_CXX_EXAMPLE CXX)
 find_package(Z3
   REQUIRED
   CONFIG
@@ -14,34 +14,18 @@ find_package(Z3
   NO_DEFAULT_PATH
 )
 
-################################################################################
-# Z3 C++ API bindings require C++11
-################################################################################
-set(CMAKE_CXX_STANDARD 11)
-set(CMAKE_CXX_STANDARD_REQUIRED ON)
-
 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})
-
-target_compile_options(cpp_example PRIVATE ${Z3_COMPONENT_CXX_FLAGS})
+target_link_libraries(cpp_example PRIVATE z3::libz3)
 
 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
-        $<TARGET_FILE:${z3_lib}>
-        $<TARGET_FILE_DIR:cpp_example>
-    )
-  endforeach()
+  add_custom_command(TARGET cpp_example POST_BUILD
+    COMMAND ${CMAKE_COMMAND} -E copy_if_different
+      $<TARGET_FILE:z3::libz3> $<TARGET_FILE_DIR:cpp_example>)
 endif()

examples/c/CMakeLists.txt

@@ -5,8 +5,8 @@
 # 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.
+cmake_minimum_required(VERSION 3.5)
 project(Z3_C_EXAMPLE C CXX)
-cmake_minimum_required(VERSION 3.4)
 set(CMAKE_C_STANDARD_REQUIRED ON)
 set(CMAKE_C_STANDARD 99)
 set(CMAKE_C_EXTENSIONS OFF)
@@ -37,21 +37,13 @@ if (FORCE_CXX_LINKER)
   )
 endif()
 
-target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
-target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})
+target_link_libraries(c_example PRIVATE z3::libz3)
 
 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
-        $<TARGET_FILE:${z3_lib}>
-        $<TARGET_FILE_DIR:c_example>
-    )
-  endforeach()
+  add_custom_command(TARGET c_example POST_BUILD
+    COMMAND ${CMAKE_COMMAND} -E copy_if_different
+      $<TARGET_FILE:z3::libz3> $<TARGET_FILE_DIR:c_example>)
 endif()

examples/maxsat/CMakeLists.txt

@@ -5,8 +5,8 @@
 # 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.
+cmake_minimum_required(VERSION 3.5)
 project(Z3_C_MAXSAT_EXAMPLE C CXX)
-cmake_minimum_required(VERSION 3.4)
 find_package(Z3
   REQUIRED
   CONFIG
@@ -22,8 +22,7 @@ message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
 message(STATUS "Z3_DIR: ${Z3_DIR}")
 
 add_executable(c_maxsat_example maxsat.c)
-target_include_directories(c_maxsat_example PRIVATE ${Z3_C_INCLUDE_DIRS})
-target_link_libraries(c_maxsat_example PRIVATE ${Z3_LIBRARIES})
+target_link_libraries(c_maxsat_example PRIVATE z3::libz3)
 
 option(FORCE_CXX_LINKER "Force linker with C++ linker" OFF)
 if (FORCE_CXX_LINKER)
@@ -39,14 +38,7 @@ 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_maxsat_example
-      POST_BUILD
-      COMMAND
-        ${CMAKE_COMMAND} -E copy_if_different
-        $<TARGET_FILE:${z3_lib}>
-        $<TARGET_FILE_DIR:c_maxsat_example>
-    )
-  endforeach()
+  add_custom_command(TARGET c_maxsat_example POST_BUILD
+    COMMAND ${CMAKE_COMMAND} -E copy_if_different
+      $<TARGET_FILE:z3::libz3> $<TARGET_FILE_DIR:c_maxsat_example>)
 endif()

examples/userPropagator/CMakeLists.txt

@@ -1,8 +1,8 @@
 ################################################################################
 # Example C++ project
 ################################################################################
+cmake_minimum_required(VERSION 3.12)
 project(Z3_USER_PROPAGATOR_EXAMPLE CXX)
-cmake_minimum_required(VERSION 3.4)
 find_package(Z3
   REQUIRED
   CONFIG
@@ -14,12 +14,6 @@ find_package(Z3
   NO_DEFAULT_PATH
 )
 
-################################################################################
-# Z3 C++ API bindings require C++11, but this code needs later.
-################################################################################
-set(CMAKE_CXX_STANDARD 20)
-set(CMAKE_CXX_STANDARD_REQUIRED ON)
-
 message(STATUS "Z3_FOUND: ${Z3_FOUND}")
 message(STATUS "Found Z3 ${Z3_VERSION_STRING}")
 message(STATUS "Z3_DIR: ${Z3_DIR}")
@@ -33,21 +27,14 @@ add_executable(user_propagator_example
         user_propagator_internal_maximisation.h
         user_propagator_created_maximisation.h)
 
-target_include_directories(user_propagator_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
-target_link_libraries(user_propagator_example PRIVATE ${Z3_LIBRARIES})
+target_compile_features(user_propagator_example PRIVATE cxx_std_20)
+target_link_libraries(user_propagator_example PRIVATE z3::libz3)
 
 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 user_propagator_example
-      POST_BUILD
-      COMMAND
-        ${CMAKE_COMMAND} -E copy_if_different
-        $<TARGET_FILE:${z3_lib}>
-        $<TARGET_FILE_DIR:user_propagator_example>
-    )
-  endforeach()
+  add_custom_command(TARGET user_propagator_example POST_BUILD
+    COMMAND ${CMAKE_COMMAND} -E copy_if_different
+      $<TARGET_FILE:z3::libz3> $<TARGET_FILE_DIR:user_propagator_example>)
 endif()

src/CMakeLists.txt

@@ -112,8 +112,16 @@ if (MSVC AND Z3_BUILD_LIBZ3_MSVC_STATIC)
     endforeach()
 endif()
 add_library(libz3 ${lib_type} ${object_files})
+if (NOT TARGET z3::libz3)
+  add_library(z3::libz3 ALIAS libz3)
+endif()
+# z3++.h requires C++11. Use a granular feature because the cxx_std_11
+# meta-feature is newer than the minimum CMake version for package consumers.
+target_compile_features(libz3 INTERFACE cxx_noexcept)
 target_include_directories(libz3 INTERFACE
   $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/api>
+  # z3++.h lives in a separate directory from the C headers.
+  $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/api/c++>
   $<INSTALL_INTERFACE:${CMAKE_INSTALL_INCLUDEDIR}>)
 set_target_properties(libz3 PROPERTIES
   # VERSION determines the version in the filename of the shared library.

src/api/python/CMakeLists.txt

@@ -78,42 +78,28 @@ else()
   set(LINK_COMMAND "copy")
 endif()
 
-# Link libz3 into the python directory so bindings work out of the box
-# Handle both built libz3 and pre-installed libz3
-if (TARGET libz3)
-  # Get the libz3 location - handle both regular and imported targets
-  get_target_property(LIBZ3_IS_IMPORTED libz3 IMPORTED)
-  if (LIBZ3_IS_IMPORTED)
-    # For imported targets, get the IMPORTED_LOCATION
-    get_target_property(LIBZ3_SOURCE_PATH libz3 IMPORTED_LOCATION)
-    # No dependency on libz3 target since it's pre-built
-    set(LIBZ3_DEPENDS "")
-  else()
-    # For regular targets, use the build output location
-    set(LIBZ3_SOURCE_PATH "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}")
-    set(LIBZ3_DEPENDS libz3)
-  endif()
-
-  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+# Link libz3 into the python directory so bindings work out of the box.
+if (TARGET z3::libz3)
+  add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_LIBRARY_SUFFIX}"
     COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
-      "${LIBZ3_SOURCE_PATH}"
-      "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
-    DEPENDS ${LIBZ3_DEPENDS}
+      "$<TARGET_FILE:z3::libz3>"
+      "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_LIBRARY_SUFFIX}"
+    DEPENDS "$<TARGET_FILE:z3::libz3>"
     COMMENT "Linking libz3 into python directory"
   )
   if (CMAKE_SYSTEM_NAME STREQUAL "Linux")
-    add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}"
+    add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_LIBRARY_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}"
       COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
-        "${LIBZ3_SOURCE_PATH}"
-        "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}"
-      DEPENDS ${LIBZ3_DEPENDS}
+        "$<TARGET_FILE:z3::libz3>"
+        "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_LIBRARY_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}"
+      DEPENDS "$<TARGET_FILE:z3::libz3>"
       COMMENT "Linking versioned libz3 into python directory"
     )
     list(APPEND build_z3_python_bindings_target_depends
-      "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}")
+      "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_LIBRARY_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}")
   endif()
 else()
-  message(FATAL_ERROR "libz3 target not found. Cannot build Python bindings.")
+  message(FATAL_ERROR "z3::libz3 target not found. Cannot build Python bindings.")
 endif()
 
 
@@ -122,7 +108,7 @@ add_custom_target(build_z3_python_bindings
   ALL
   DEPENDS
     ${build_z3_python_bindings_target_depends}
-    "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+    "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_LIBRARY_SUFFIX}"
 )
 
 ###############################################################################