Update OpenSMT to version 2.8.0 #426
Conversation
…mtjava.so and opensmt.so into a single library
| <arg value="/dependencies/gmp-6.2.1/.libs/libgmp.a"/> | ||
| <arg value="/dependencies/gmp-6.2.1/.libs/libgmpxx.a"/> |
There was a problem hiding this comment.
These paths will only work when using the docker image to build the bindings. We could use a property -Dopensmt.gmp.path=XXX to let the user set the path. Alternatively we could also download (and build) GMP in the ant script itself.
There was a problem hiding this comment.
Personally, I do not like using dependencies from the Docker image. Other solvers include GMP from separate build directories, where the developer can exchange the files directly. The only benefit is a "constant" version from the Docker image.
Using an option would be a good step towards a more flexible solution.
There was a problem hiding this comment.
Well, it works quite well for now. I see no problem in mergin this and improving it later.
| // TODO These were also added recently. Are they useful to us? | ||
| %ignore MainSolver::printResolutionProofSMT2() const; | ||
| %ignore MainSolver::printResolutionProofSMT2(std::ostream &) const; |
There was a problem hiding this comment.
If these are interesting to use they can still be included
There was a problem hiding this comment.
It does not hurt to have a full API available. Then it is simpler to add new features later.
| @@ -0,0 +1,416 @@ | |||
| diff --git a/lib/native/source/opensmt/opensmt-wrap.cpp b/lib/native/source/opensmt/opensmt-wrap.cpp | |||
There was a problem hiding this comment.
OpenSMT is licensed with MIT license.
Should we publish all the JavaSMT bindings for OpenSMT as Apache2.0 OR MIT, or only the C files?
| @@ -0,0 +1,416 @@ | |||
| diff --git a/lib/native/source/opensmt/opensmt-wrap.cpp b/lib/native/source/opensmt/opensmt-wrap.cpp | |||
| index cfe601cd2..70df21180 100644 | |||
There was a problem hiding this comment.
This file is funny: a patch file for license headers, and it has a separate license file for itself.
Good idea and valid solution.
PS: You could also have created a separate license file FILE.i.license per source file FILE.i.
Ubuntu 18.04 does not provide the required compiler version for c++20, so we use Ubuntu 22.04.
|
Thanks for merging! I'll keep your comments in mind for the next OpenSMT update. |
Hello everyone,
this pull request will update OpenSMT to version 2.8.0. We're currently using a fairly recent version of OpenSMT 2.6.X and there have been few larger changes since. However, since there was some internal refactoring, and all the code has been moved into the
opensmtnamespace, some changes to the SWIG headers are needed. We use this opportunity to also update out own build scripts and will now include all the auto-generated SWIG code in the repository. This is already done for Bitwuzla and should make it easier for us to spot any unintended changes when the JNI bindings are again updated. In addition to that we changed the build process to only produce a single library that can be included more easily from Java and doesn't require us to patch therpath.Since this update isn't too urgent we might want to wait for #395 before committing it.