The generated Python bindings loaded `libz3.so` without a soversion,
which could bind to an ABI-incompatible shared library when multiple Z3
versions are present. This change makes Linux bindings prefer the
versioned soname while leaving other platforms on the existing lookup
path.
- **Python loader generation**
- Thread a `z3py_soversion` parameter through `scripts/update_api.py`.
- Generate `_lib_name` as `libz3.so.<major>.<minor>` on Linux, and keep
`libz3.<ext>` elsewhere.
- Reuse `_lib_name` consistently for directory probing, system fallback,
and error messages.
- **Build-system wiring**
- Pass the current `SOVERSION` from the CMake Python bindings build on
Linux.
- Pass the same value through the `mk_make`/`mk_util.py` generation path
so both build systems emit the same loader behavior.
- **In-tree Python bindings layout**
- Add the matching `libz3.so.<major>.<minor>` link in `build/python/` on
Linux so the generated bindings work directly from the build tree.
- **Regression coverage**
- Add a focused script-level test for the generated loader preamble to
check:
- Linux uses the versioned soname when provided.
- Non-versioned fallback remains available when no soversion is
supplied.
Example of the generated Linux loader behavior:
```python
_sover = '5.0'
_ext = 'so'
_lib_name = 'libz3.%s.%s' % (_ext, _sover) if sys.platform.startswith('linux') and _sover else 'libz3.%s' % _ext
_lib = ctypes.CDLL(_lib_name)
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#7518
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
On macOS, libz3java.dylib was built without an rpath to find libz3.dylib
in the same directory. When Java loaded the JNI library, the dynamic
linker could not resolve the libz3 dependency, causing
UnsatisfiedLinkError.
Three fixes:
- mk_util.py: add -Wl,-rpath,@loader_path to the macOS JNI link command
- CMakeLists.txt: set MACOSX_RPATH, BUILD_RPATH, INSTALL_RPATH for
z3java target; remove duplicate headerpad block
- update_api.py: improve Native.java error message to show the root
cause from both load attempts instead of only the fallback error
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The underlying `mpf_manager::sgn` function returns a `bool`, and functions
such as `Z3_mk_fpa_numeral_int_uint` take the sign as a `bool`.
Signed-off-by: Josh Berdine <josh@berdine.net>
Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation
* Fixed decide callback for Java user propagators
* Java User Prop:
- Added return value to conflict
- Added consequence method
- Added missing access modifier to decideWrapper
* Removed type parameters of expressions in UserPropagatorBase
* Renamed propagateConflict to propagateConsequence
Use built-in `importlib.resources` module rather than the external
`importlib_resources` package on Python 3.9 and newer. The latter
is only intended as a backport for old Python versions, and since modern
Linux distributions may no longer support such old Python versions,
they also no longer provide importlib_resources (this is the case
on Gentoo).
This happens when generating the Python API and you are using
Python 3.12 in the build environment:
```
.../z3/scripts/update_api.py:1828: SyntaxWarning: invalid escape sequence '\#'
```
This was a `DeprecationWarning` previously, but Python 3.12 changed
it to a `SyntaxWarning` to make it more visible. The release notes
indicate that this will be a syntax error in the future.
* Use int64 for ocaml api functions that require it
Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
* Use elif
Signed-off-by: Stefan Muenzel <source@s.muenzel.net>
Make it easier to add native methods for callbacks (for user propagator) #6097
The Java User propagator wrapper should define a base class with virtual methods that can be invoked from functions defined in NativeStatic.txt
