Update OpenSMT to 2.9.0 and include support for proofs in the JNI bindings #479
Conversation
This file contains hidden or 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
…s is aborted with an error
kfriedberger
previously approved these changes
Apr 25, 2025
There was a problem hiding this comment.
Overall, good work.
The commits are clearly structured and the code changes are good.
Personally, I would prefer to not include dependencies like GMP or JDK in the Docker image as they cannot be easily updated or exchanged, but require a rebuild of the image. In this PR, there still is the comand line option to set them, which is nice and a valid solution.
I will test the overall build chain the next days.
This step includes a dependency in the image that would need to be downloaded from developers to compile some solvers or their bindings, such as OpenSMT.
We still require the same basic structure, such that external dependencies are available in the same directory as the JavaSMT checkout.
|
JavaDoc publication fails for several weeks. We will investigate and address this CI issue separately. The rest looks very good. @daniel-raffler Thanks for the PR. |
|
Thanks for the review! 👍 |
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.
Hello everyone,
this PR will update OpenSMT to version 2.9.0 while also adding the method
MainSolver.printResolutionProofSMT2to the JNI bindings in preparation for #458. There are also some minor simplifications to the build process and the binaries for GMP on x86-linux and arm64-linux are now included in the build container and no longer have to be provided by the maintainer when updating the binaries.