3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-19 15:04:42 +00:00
Commit graph

19 commits

Author SHA1 Message Date
bu99ed
cea0f7c427 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-02-18 20:57:04 -08:00
Copilot
df816cab07
Add finite set API support for C# and Java bindings (#8003)
* Initial plan

* Add finite set API support for Java and C#

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

* Add documentation and examples for finite set APIs

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

* Delete FINITE_SET_API_EXAMPLES.md

* Add FiniteSetSort files to CMakeLists.txt build configurations

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>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-11-04 15:57:55 -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)