* 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>
* Initial plan
* Build Z3 for ubuntu x64 and invoke JS build scripts in docs workflow
- Modified docs.yml to build Z3 natively for ubuntu-latest x64 before documentation generation
- Removed default working directory to allow explicit working-directory per step
- Added step to build Z3 using python scripts/mk_make.py
- Kept emscripten setup as required for wasm build
- Modified mk_api_doc.py to invoke npm run build:ts and npm run build:wasm as described in src/api/js/README.md
- mk_api_doc.py now runs the full build process (TypeScript + wasm) before generating documentation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Source emsdk environment before generating documentation
- Added source command to ensure emscripten tools are in PATH when mk_api_doc.py runs npm scripts
- This ensures emcc and other emscripten tools are available for npm run build:wasm
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert changes to mk_api_doc.py
- Removed npm run build:ts and npm run build:wasm calls from mk_api_doc.py
- Reverted to only calling npm run docs as before
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Fix DEL character encoding in string literals
Change condition from `ch >= 128` to `ch >= 127` to include the DEL
character (U+007F, 127) in escaped output. This ensures that the
non-printable DEL control character is properly escaped as \u{7f}
instead of being printed directly.
Also add test cases for DEL and other control characters.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960)
* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet
* adding comments
* fix bug about needing to bubble resolvent upwards to highest ancestor
* fix bug where we need to cover the whole resolvent in the path when bubbling up
* clean up comments
* close entire tree when sibling resolvent is empty
* integrate asms directly into cube tree, remove separate tracking
* try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function
* separate the logic again to avoid mutual recursion
* Refactor search tree closure and resolution logic
Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity.
* apply formatting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Refactor close_with_core to use current node in lambda
* Fix formatting issues in search_tree.h
* fix build issues
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Update smt_parallel.cpp
* Change loop variable type in unsat core processing
* Change method to retrieve unsat core from root
---------
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* Initial plan
* Disable C++98 compatibility warnings for Clang to fix vcpkg build freeze
Add -Wno-c++98-compat and -Wno-c++98-compat-pedantic flags to prevent
excessive warning output when building with clang-cl or when -Weverything
is enabled. These warnings are not useful for Z3 since it requires C++20.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation.
To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
