Merge 74501e2c48 into 62cd39729f

2025-11-22 13:41:27 +00:00 · 2025-11-16 20:07:47 +00:00 · 2025-11-16 20:07:47 +00:00 · 04fc752d3b
commit 04fc752d3b
parent 62cd39729f 74501e2c48
4 changed files with 137 additions and 33 deletions
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@ -559,10 +559,15 @@ add_subdirectory(src)
 # use Z3 via CMake.
 ################################################################################
 include(CMakePackageConfigHelpers)
-export(EXPORT Z3_EXPORTED_TARGETS
-   NAMESPACE z3::
-   FILE "${PROJECT_BINARY_DIR}/Z3Targets.cmake"
-)
+
+# Only export targets if we built libz3
+if (Z3_BUILD_LIBZ3_CORE)
+  export(EXPORT Z3_EXPORTED_TARGETS
+     NAMESPACE z3::
+     FILE "${PROJECT_BINARY_DIR}/Z3Targets.cmake"
+  )
+endif()
+
 set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${PROJECT_BINARY_DIR}/src/api")
 set(Z3_SECOND_PACKAGE_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/src/api")
 set(Z3_CXX_PACKAGE_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/src/api/c++")
@ -593,12 +598,15 @@ configure_file("${CMAKE_CURRENT_SOURCE_DIR}/z3.pc.cmake.in"
 # 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}"
-)
+# Only install targets if we built libz3
+if (Z3_BUILD_LIBZ3_CORE)
+  install(EXPORT
+    Z3_EXPORTED_TARGETS
+    FILE "Z3Targets.cmake"
+    NAMESPACE z3::
+    DESTINATION "${CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR}"
+  )
+endif()
 set(Z3_INSTALL_TREE_CMAKE_CONFIG_FILE "${PROJECT_BINARY_DIR}/cmake/Z3Config.cmake")
 set(Z3_FIRST_PACKAGE_INCLUDE_DIR "${CMAKE_INSTALL_INCLUDEDIR}")
 set(Z3_SECOND_INCLUDE_DIR "")
--- a/README-CMake.md
+++ b/README-CMake.md
@ -410,9 +410,10 @@ The following useful options can be passed to CMake whilst configuring.
 * ``Python3_EXECUTABLE`` - STRING. The python executable to use during the build.
 * ``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.
 * ``Z3_BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library.
+* ``Z3_BUILD_LIBZ3_CORE`` - BOOL. If set to ``TRUE`` (default) build the core libz3 library. If set to ``FALSE``, skip building libz3 and look for a pre-installed library instead. This is useful when building only Python bindings on top of an already-installed libz3.
 * ``Z3_ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples.
 * ``Z3_USE_LIB_GMP`` - BOOL. If set to ``TRUE`` use the GNU multiple precision library. If set to ``FALSE`` use an internal implementation.
-* ``Z3_BUILD_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's python bindings will be built.
+* ``Z3_BUILD_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's python bindings will be built. When ``Z3_BUILD_LIBZ3_CORE`` is ``FALSE``, this will build only the Python bindings using a pre-installed libz3.
 * ``Z3_INSTALL_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_PYTHON_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Python bindings.
 * ``Z3_BUILD_DOTNET_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's .NET bindings will be built.
 * ``Z3_INSTALL_DOTNET_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_DOTNET_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's .NET bindings.
@ -464,6 +465,49 @@ cmake -DCMAKE_BUILD_TYPE=Release -DZ3_ENABLE_TRACING_FOR_NON_DEBUG=FALSE ../
 Z3 exposes various language bindings for its API. Below are some notes on building
 and/or installing these bindings when building Z3 with CMake.

+### Python bindings
+
+#### Building Python bindings with libz3
+
+The default behavior when ``Z3_BUILD_PYTHON_BINDINGS=ON`` is to build both the libz3 library
+and the Python bindings together:
+
+```
+mkdir build
+cd build
+cmake -DZ3_BUILD_PYTHON_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ../
+make
+```
+
+#### Building only Python bindings (using pre-installed libz3)
+
+For package managers like conda-forge that want to avoid rebuilding libz3 for each Python version,
+you can build only the Python bindings by setting ``Z3_BUILD_LIBZ3_CORE=OFF``. This assumes
+libz3 is already installed on your system:
+
+```
+# First, build and install libz3 (once)
+mkdir build-libz3
+cd build-libz3
+cmake -DZ3_BUILD_LIBZ3_SHARED=ON -DCMAKE_INSTALL_PREFIX=/path/to/prefix ../
+make
+make install
+
+# Then, build Python bindings for each Python version (quickly, without rebuilding libz3)
+cd ..
+mkdir build-py310
+cd build-py310
+cmake -DZ3_BUILD_LIBZ3_CORE=OFF \
+      -DZ3_BUILD_PYTHON_BINDINGS=ON \
+      -DCMAKE_INSTALL_PREFIX=/path/to/prefix \
+      -DPython3_EXECUTABLE=/path/to/python3.10 ../
+make
+make install
+```
+
+This approach significantly reduces build time when packaging for multiple Python versions,
+as the expensive libz3 compilation happens only once.
+
 ### Java bindings

 The CMake build uses the ``FindJava`` and ``FindJNI`` cmake modules to detect the
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@ -106,16 +106,19 @@ add_subdirectory(api/dll)
 ################################################################################
 # libz3
 ################################################################################
-get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
-set (object_files "")
-foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
-  list(APPEND object_files $<TARGET_OBJECTS:${component}>)
-endforeach()
-if (Z3_BUILD_LIBZ3_SHARED)
-  set(lib_type "SHARED")
-else()
-  set(lib_type "STATIC")
-endif()
+option(Z3_BUILD_LIBZ3_CORE "Build the core libz3 library" ON)
+
+if (Z3_BUILD_LIBZ3_CORE)
+  get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
+  set (object_files "")
+  foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
+    list(APPEND object_files $<TARGET_OBJECTS:${component}>)
+  endforeach()
+  if (Z3_BUILD_LIBZ3_SHARED)
+    set(lib_type "SHARED")
+  else()
+    set(lib_type "STATIC")
+  endif()
 # Enable static msvc runtime.
 if (MSVC AND Z3_BUILD_LIBZ3_MSVC_STATIC)
    set(CompilerFlags
@ -300,12 +303,35 @@ if (MSVC)
  z3_append_linker_flag_list_to_target(libz3 "/DEF:${dll_module_exports_file}")
 endif()

+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}")
+  
+  # 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}
+  )
+endif()
+
 ################################################################################
 # Z3 executable
 ################################################################################
 cmake_dependent_option(Z3_BUILD_EXECUTABLE
    "Build the z3 executable" ON
-    "CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
+    "CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR;Z3_BUILD_LIBZ3_CORE" OFF)

 if (Z3_BUILD_EXECUTABLE)
    add_subdirectory(shell)
@ -317,7 +343,7 @@ endif()

 cmake_dependent_option(Z3_BUILD_TEST_EXECUTABLES
    "Build test executables" ON
-    "CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
+    "CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR;Z3_BUILD_LIBZ3_CORE" OFF)


 if (Z3_BUILD_TEST_EXECUTABLES)
@ -330,9 +356,16 @@ endif()
 ################################################################################
 option(Z3_BUILD_PYTHON_BINDINGS "Build Python bindings for Z3" OFF)
 if (Z3_BUILD_PYTHON_BINDINGS)
-  if (NOT Z3_BUILD_LIBZ3_SHARED)
-    message(FATAL_ERROR "The python bindings will not work with a static libz3. "
-            "You either need to disable Z3_BUILD_PYTHON_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED")
+  # Validate configuration for Python bindings
+  if (Z3_BUILD_LIBZ3_CORE)
+    # Building libz3 together with Python bindings
+    if (NOT Z3_BUILD_LIBZ3_SHARED)
+      message(FATAL_ERROR "The python bindings will not work with a static libz3. "
+              "You either need to disable Z3_BUILD_PYTHON_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED")
+    endif()
+  else()
+    # Using pre-installed libz3 for Python bindings
+    message(STATUS "Building Python bindings with pre-installed libz3")
  endif()
  add_subdirectory(api/python)
 endif()
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@ -70,13 +70,32 @@ else()
 endif()

 # Link libz3 into the python directory so bindings work out of the box
-add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
-  COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
-    "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
-    "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
-  DEPENDS libz3
-  COMMENT "Linking libz3 into python directory"
-)
+# 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}"
+    COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
+      "${LIBZ3_SOURCE_PATH}"
+      "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+    DEPENDS ${LIBZ3_DEPENDS}
+    COMMENT "Linking libz3 into python directory"
+  )
+else()
+  message(FATAL_ERROR "libz3 target not found. Cannot build Python bindings.")
+endif()
+

 # Convenient top-level target
 add_custom_target(build_z3_python_bindings