Add CMake option to build only Python bindings without rebuilding libz3

Introduce Z3_BUILD_LIBZ3_CORE option (default ON) to control whether libz3 is built.
When set to OFF with Z3_BUILD_PYTHON_BINDINGS=ON, only Python bindings are built
using a pre-installed libz3 library. This is useful for package managers like
conda-forge to avoid rebuilding libz3 for each Python version.

Changes:
- Add Z3_BUILD_LIBZ3_CORE option in src/CMakeLists.txt
- When OFF, find and use pre-installed libz3 as imported target
- Update Python bindings CMakeLists.txt to handle both built and imported libz3
- Add documentation in README-CMake.md with usage examples

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

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

src/CMakeLists.txt

@@ -106,6 +106,9 @@ add_subdirectory(api/dll)
 ################################################################################
 # libz3
 ################################################################################
+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})
@@ -300,6 +303,29 @@ 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
 ################################################################################
@@ -330,10 +356,17 @@ endif()
 ################################################################################
 option(Z3_BUILD_PYTHON_BINDINGS "Build Python bindings for Z3" OFF)
 if (Z3_BUILD_PYTHON_BINDINGS)
+  # 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()
 

src/api/python/CMakeLists.txt

@@ -70,13 +70,32 @@ else()
 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}"
     COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
-    "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+      "${LIBZ3_SOURCE_PATH}"
       "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
-  DEPENDS libz3
+    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