BLD: Add CMake option to build Python bindings without rebuilding libz3

[Copilot]

Conda-forge builds z3-solver for 5 Python versions (3.10-3.14), currently rebuilding the Python-version-independent libz3 library each time. This wastes 3-5 hours rebuilding identical C++ code.

Changes

New CMake option Z3_BUILD_LIBZ3_CORE (default ON):

• When OFF, skips building libz3 and links Python bindings to pre-installed library
• Uses find_library() to locate existing libz3 and creates imported CMake target
• Automatically disables executable/test builds to avoid install failures

Modified build logic:

• src/api/python/CMakeLists.txt: Detects imported vs regular libz3 target, adjusts source paths and dependencies accordingly
• CMakeLists.txt: Conditionally exports Z3_EXPORTED_TARGETS only when building libz3 to prevent CMake errors

Documentation: Added usage example to README-CMake.md

Usage

# Build libz3 once
cmake -DZ3_BUILD_LIBZ3_SHARED=ON -DCMAKE_INSTALL_PREFIX=$PREFIX ..
make install

# Build Python bindings for each Python version (fast, no C++ compilation)
cmake -DZ3_BUILD_LIBZ3_CORE=OFF \
      -DZ3_BUILD_PYTHON_BINDINGS=ON \
      -DCMAKE_INSTALL_PREFIX=$PREFIX \
      -DPython3_EXECUTABLE=/path/to/python3.X \
      ..
make install

Reduces conda-forge build time from 3-5h to ~1h.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>BLD: provide CMake option to install only python bindings</issue_title>
<issue_description>Hi!

I help run conda-forge, a big packaging ecosystem for python and many more languages. For almost a year, we've providing z3 as a package that can be installed also through conda install -c conda-forge z3-solver.

Conda as a paradigm is strictly more powerful than what PyPI and wheels can offer, namely, we can package native C/C++/Fortran libraries and binaries for linux/osx/win just as well as python libraries.

Unsurprisingly, the C++ library underlying z3-solver is independent of the python version being used. This is a very common pattern, and we like to package things in a way that reduces vendoring and other redundancies; in other words, there's a python-independent libz3, which z3-solver can then depend on, and everything works fine.

However, there's a limitation in building the package at the moment; due to the very bespoke python scripts/mk_make.py setup, I've preferred to go with the CMake-based builds; the problem with this is just that we're very inefficiently building the library portion 6 times, rather than once, namely (indentation indicates dependence):

• libz3 - necessary ✅
  • z3-solver (py3.10) - rebuilds library, discards it because it matches what libz3 provides ❌
  • z3-solver (py3.11) - rebuilds library, discards it because it matches what libz3 provides ❌
  • z3-solver (py3.12) - rebuilds library, discards it because it matches what libz3 provides ❌
  • z3-solver (py3.13) - rebuilds library, discards it because it matches what libz3 provides ❌
  • z3-solver (py3.14) - rebuilds library, discards it because it matches what libz3 provides ❌

If there was an easy way to install just the python bindings on top of an already-installed libz3 (everything for us is happens in one central but relocatable $PREFIX), that would allow us to cut this down to building the library once, and then do only very quick installs for the python bindings. This would cut the build time from 3-5h down to ~1h.

I have enough experience with this that I could probably hack something together (and we do test our packages before publishing), but then it would be me who has to maintain it, and I was hoping that this is a reasonable request that the project would be willing to accommodate. 😅🙃 </issue_description>

Comments on the Issue (you are @copilot in this section)

@NikolajBjorner is this for updating cmakefiles.txt or setup.py? Either way, you can add a PR. Not sure what maintenance overhead you refer to: I can't maintain other packages outside of z3prover. If the package managers change and their use in z3 bit-rots beyond simple repair I disable them (for example, I don't upload nuget packages any longer because of enterprise signing obstacles and changed requirements for readme files). @NikolajBjorner I don't have competence or bandwidth to dig into cmake details. You are welcome to add a PR, I can assign this to copilot too and see what it comes up with.

• Fixes BLD: provide CMake option to install only python bindings #8016

---

💬 We'd love your input! Share your thoughts on Copilot coding agent in our 2 minute survey.