mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-25 13:36:53 +00:00
Code Activity
z3/src
History
h-vetinari 429771e5b7
BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088) 
* 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>

* Fix CMake export issues when building only Python bindings

Conditionally export Z3_EXPORTED_TARGETS only when Z3_BUILD_LIBZ3_CORE=ON
to avoid errors when building Python bindings without building libz3.

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

* Disable executable and test builds when not building libz3 core

When Z3_BUILD_LIBZ3_CORE=OFF, automatically disable Z3_BUILD_EXECUTABLE
and Z3_BUILD_TEST_EXECUTABLES to avoid build/install errors.

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

* only build src/ folder if Z3_BUILD_LIBZ3_CORE is TRUE

* move z3 python bindings to main CMake

* move more logic to main CMakeLists.txt

* move Z3_API_HEADER_FILES_TO_SCAN to main CMakeLists.txt

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2025-12-16 17:50:37 +00:00
..
ackermannization Centralize and document TRACE tags using X-macros (#7657) 2025-05-28 14:31:25 +01:00
api BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088) 2025-12-16 17:50:37 +00:00
ast don't unfold recursive defs if there is an uninterpreted subterm, #7671 2025-12-10 00:26:21 -08:00
cmd_context allow parsing declared arrays without requiring explicit select 2025-12-06 18:02:15 -08:00
math fix #8054 2025-11-30 07:51:06 -08:00
model Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985) 2025-10-16 13:18:35 +02:00
muz fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables 2025-09-30 15:58:48 -07:00
nlsat remove unused *_signed_project() methods 2025-12-02 18:46:16 -10:00
opt Implement Z3_optimize_translate for context translation (#8072) 2025-12-13 05:12:08 +00:00
params remove stale experimental code #8063 2025-12-12 05:49:05 +00:00
parsers fix #7956 2025-09-30 15:41:49 -07:00
qe remove unused *_signed_project() methods 2025-12-02 18:46:16 -10:00
sat remove stale experimental code #8063 2025-12-12 05:49:05 +00:00
shell move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00
smt Search tree core resolution optimization (#8066) 2025-12-13 12:06:56 +00:00
solver Add commands for forcing preferences during search 2025-10-02 10:47:10 -07:00
tactic remove model converter operator on expr_ref& 2025-09-07 16:42:20 -07:00
test Fix DEL character (0x7F) not being escaped in string literals (#8080) 2025-12-15 22:23:49 +00:00
util Fix DEL character (0x7F) not being escaped in string literals (#8080) 2025-12-15 22:23:49 +00:00
CMakeLists.txt BLD: Add CMake option to build Python bindings without rebuilding libz3 (redux) (#8088) 2025-12-16 17:50:37 +00:00