#380 support multiple architectures for solver binaries z3 #395
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
This PR is currently blocked by sosy-lab/java-common-lib#43 to test execution on ARM64. // UPDATE: The wording "blocked" is too much. Z3 is still not available for ARM64 on Linux, so local development is not affected and we could merge this PR. |
|
The current state seems to work as expected. I tested:
Z3 is already published in Maven and Ivy, and works well with JavaSMT 5.0.1. As I do not have an ARM-based Apple machine available, maybe @ThomasHaas and @hernanponcedeleon can test whether it works as expected. Thanks. |
|
If there is positive feedback, I will also publish Z3 in its latest version 4.13.2 to Ivy and Maven. The publication of Z3 is even more automated now than it was before. |
|
It seems to work on ARM-based Macs now. Good job :) |
|
Z3 was published to Ant/Ivy and Maven in versions 4.13.2 and 4.13.3. There are some smaller issues that are currently blocking this PR from merging:
|
Not tested, not finished, just a draft.
… for backwards compatibility.
This should keep the existing cache valid and re-usable. Otherwise, we would create a new cache structure within the existing cache, with redundant entries. With this change, we limit the redundancy to arch- or classifier-specific entries.
We could include x64 and ARM64 dependencies for Z3. However, the default stays by only x64.
…rs, but only all other files. This cleanup aligns better with Maven guidelines. This is a small change for all upcoming publications to Maven and the Maven users.
…cture. Additionally, we upload Java sources and JavaDoc for z3 to the Maven repository. We need to test whether the uploaded files work as expected.
Let the user decide what to load, e.g. on a minimal system only load for one specific OS and arch.
See Z3Prover/z3#7419 for details. If required, the Z3 parser automatically converts Boolean formulas `f` to e.g. `ITE(f 1 0)`, which makes them comparable to Integer symbols and numbers 0/1.
kfriedberger
force-pushed
the
380-multi-architecture-solver-binaries-z3
branch
from
208e2c2
to
4a40c32
Compare
…3 v4.13.2 and incompatible msvcp140.dll. See Z3Prover/z3#7420 for details. This update is just a test. If it does not work, we will revert it.
…s with Z3 v4.13.2 and incompatible msvcp140.dll." This reverts commit 07a4015.
… for multiple architectures. We aim for backwards-compatibility and provide the x64-version as default for most public configurations. The solver-specific configuration "runtime-z3" does provide more than x64, and comes with arm64 included.
…ate dependencies. - prepare for distinct architectures x64 and arm64 under Linux. - remove MPIR usage and replace it with GMP headers. MPIR is unmaintained since several years. - update GMP to v6.3.0 and JDK to v17
This reverts commit 07a4015.
…ure-solver-binaries-z3
…Instead, we use a plain Java-based solver as reference.
|
This branch is currently blocked by or waiting for:
|
….04 and 20.04, using only GLIBC_2.27.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This branch / pull request exists for tracking some steps towards supporting multiple architectures. I will use Z3 as example, because it was requested several times. Some explanation can be found in #380 .
I will not yet commit binaries to any public archive (Ivy or Maven) until we can make sure that the new approach is backwards-compatible (e.g. default architecture x86 can be used as before) and we have a maintainable code base (including scripts and documentation for publication and testing).