* 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>
* Enabling Control Flow Guard by default for MSVC on Windows, with options to disable it.
* Fix configuration error for non-MSVC compilers.
* Reviewed and updated configuration for Python build and added comment for CFG.
* Initial plan
* Create VERSION.txt and update CMakeLists.txt to read version from file
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Complete centralized version management system
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix version update script and finalize implementation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Create centralized version management with VERSION.txt
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>
The scoped_timer uses a std::therad. Spawning this thread fails in cases of WASM.
Instead of adapting builds and using async features at the level of WASM and the client, we expose a specialized version of z3 that doesn't use threads at all, neither for solvers nor for timers.
The tradeoff is that the periodic poll that checks for timeout directly queries the global clock each time.
We characterize it as based on polling.
`FindPythonInterp` has been deprecated for a long time and is more
verbal about that deprecation now.
The build system no longer uses `PYTHON_EXECUTABLE` but instead uses
`Python3_EXECUTABLE`.
Support for requiring cmake < 3.4 may go away soon (according to
a deprecation notice when building).
Ubuntu 20.04 provides cmake 3.16 and current is 3.27, so that seems
like a reasonable version to require.
- increase build version to 4.12.1. This prepares updated release for MacOs-11 build on x86
- move literal propagation mode in euf-egraph to a callback and traversal of equivalence class. Track antecedent by newest equality instead of root. This makes equality propagation to literals have similar behavior as in legacy solver and appears to result in a speedup (10% fewer conflicts on QF_UF/QG-classification/qg5/iso_icl478.smt2 in preliminary testing)
- fix interaction of pre-processing and assumptions. Pre-processing has to freeze assumption literals so they don't get eliminated. This is similar to dependencies that are already frozen.
These are all unused and shouldn't be needed. Mostly we need
something for differentiating between POSIX and non-POSIX
(until we can reduce some of those differences as well).
We shouldn't need to modify the build system to build on a new
OS if it is basically a Unix and is supported by cmake.
This also removes a duplicated branch since the Intel compiler
is already handled at the same time as GCC and Clang, so it
doesn't need its own block as well.
This was only being enabled on Windows, Linux, and FreeBSD. (FreeBSD
only had it enabled in the legacy build system, not in cmake.)
`thread_local` is part of C++11, so now that we require C++17
or later and more recent compilers, this should work everywhere
that threading does, so only disable it within a `SINGLE_THREAD`
build.
* Fix finding Python on Mac
On Mac you have to specify the version.
It also works well on other platforms this way.
* Ignore CMake build directories from index
* Fix warning about unused variable in release
The variable is used in debug only,
but it's legit that the compiler does not warn us for that in release.
