3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-10 02:50:55 +00:00
Commit graph

20 commits

Author SHA1 Message Date
copilot-swe-agent[bot]
a08e8a99f9 Add -headerpad_max_install_names flag for macOS dylib builds
This fixes the install_name_tool issue on macOS where the tool fails
with "larger updated load commands do not fit". The linker flag
-Wl,-headerpad_max_install_names ensures sufficient header padding
in the Mach-O binary for install_name_tool to modify install names.

Changes made:
- CMake: Added flag to libz3, z3java, z3jl shared libraries on Darwin
- Python build: Changed flag from ML-only to all macOS builds
- OCaml CMake: Added flag to OCaml stublib build on APPLE

Fixes #7623 (regression in 4.15.5)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
2026-02-08 03:26:13 +00:00
Copilot
db6e15361b
Add Java APIs for polymorphic datatypes (#8438)
* Initial plan

* Add Java APIs for polymorphic datatypes and type variables

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

* Fix code review issue and add documentation

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

* Add TypeVarSort.java to CMakeLists.txt for Java bindings

The CMake build was failing because TypeVarSort.java was not included in the Z3_JAVA_JAR_SOURCE_FILES list in src/api/java/CMakeLists.txt. Added it in alphabetical order between TupleSort.java and UninterpretedSort.java.

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>
2026-01-31 15:31:36 -08:00
bu99ed
ff7d0fb501
set source & target version java compile flags in cmake build to match the python/make build for consistent bytecode generation (#8112)
Co-authored-by: bu99ed <bu99ed@localhost>
2026-01-03 15:26:40 -08:00
Thomas Haas
a3d00ce356
Improved Java phantom references (#7131)
* Reworked phantom reference handling.
 - Replaced IDecRefQueue with a new Z3ReferenceQueue class
 - Z3ReferenceQueue manages custom subclasses of phantom references in a doubly-linked list
 - Replaced all subclasses of IDecRefQueue with subclasses of Z3ReferenceQueue.Reference. These custom reference classes are embedded in the class they reference count.
 - Context now owns a single Z3ReferenceQueue for all types of references.

* Made Statistics.Entry a static subclass

* Made Context.close idempotent (as recommended)

* Update CMakeLists.txt for building the Java API.

* Updated CMakeLists.txt again.

* Use correct SuppressWarning annotation to silence the compiler

* Formatting
2024-02-21 08:39:58 -08:00
Nikolaj Bjorner
2af1cff11f updating java cmake scrip
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-01-27 16:29:19 -08:00
Bruce Mitchener
9d1ceab1f2
cmake: Use FindPython3. (#7019)
`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`.
2023-11-27 11:20:21 +01:00
ditto
11264c38d8
Java user propagator interface (#6733)
* Java API: user propagator interface

* Java API: improved user propagator interface

* Java API: Add UserPropagatorBase.java

* Remove redundant header file

* Initialize `JavaInfo` object and error handling

* Native.UserPropagatorBase implements AutoCloseable

* Add Override annotation
2023-05-24 18:27:28 +01:00
Nikolaj Bjorner
2c21072c99 remove stub class, it may as well go into NativeStatic.txt as C++
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-22 18:23:10 +01:00
Nikolaj Bjorner
7963ecaf63 stubs for #6097
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-22 16:21:34 +01:00
Nikolaj Bjorner
4143c54257 add simplifier to java API 2023-02-02 19:06:26 -08:00
Bruce Mitchener
8a3556e5ba cmake: Remove dep on mk_util.py for update_api.py calls.
update_api.py doesn't depend on mk_util.py any longer, so these
dependencies can go away.
2022-08-04 07:54:26 +03:00
Bruce Mitchener
42f5047463 cmake: Cleanup remnants of workaround for USES_TERMINAL.
In older versions, this was dependent upon the version of cmake,
but when it was updated for newer cmake, these remnants were
left.
2022-08-02 17:39:10 +03:00
Nikolaj Bjorner
b254f4086b Separate out native static content for Java
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
2022-06-21 09:09:42 -07:00
Nikolaj Bjorner
7ae78da850 adding access to characters over API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-07-13 15:56:08 +02:00
Nikolaj Bjorner
53a01a07bd rename additional build options #2709
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-11-18 21:32:35 -08:00
Charlie Barto
167f968fa8 Change from BINARY_DIR to PROJECT_BINARY_DIR 2019-05-15 11:25:40 -07:00
Bruce Mitchener
51a947b73d Change how 64 bit builds are detected.
Instead of doing this at configure time, we look at the actual
compile time status. This also avoids hardcoding checks based on
what CPU architecture is present, which doesn't work when Z3 is
being built on non-x86_64 platforms.
2018-12-09 16:16:20 +07:00
Nikolaj Bjorner
520ce9a5ee integrate lambda expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-26 07:23:04 -07:00
Nikolaj Bjorner
4f5775c531 remove interpolation and duality dependencies
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-24 08:33:48 -07:00
Dan Liew
4b517b96df [CMake] Move CMake files into their intended location so the
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
2017-06-12 11:59:00 +01:00
Renamed from contrib/cmake/src/api/java/CMakeLists.txt (Browse further)