Open kfriedberger opened 5 days ago
baierd
commented
5 days ago I don't think that keeping our own bindings is worth it. There will be changes to the API in the future and we need to update our bindings and our code every time. Switching to the provided bindings is a little more work now, but worth it in the future in my opinion.
kfriedberger
commented
5 days ago I am unsure about the intent of your comment. I am in favour of using official release versions, too, because we do not require to compile anything and simply depend on a build pipeline from the solver's authors. The changes required in Java code are minimal (e.g., some fixes for a minor update), beause we already use the Java bindings (and thus the denoted API) from CVC5 directly. The only question is packaging and publication of shared libraries, and the CVC5 release is currently not usable in the way we would like it. We will automate that step anyway, as it is done for other solvers as well.
baierd
commented
5 days ago Oh my bad. I thought we have our own bindings for CVC5 currently. Sorry.
Self-build vs. original version: Should JavaSMT compile its own bindings from scratch (like we do for some other solvers) or use the original release version (as we do for Z3)?
Well then it depends on the benefits we get by compiling it ourselfs. I agree that we can automate most of it anyway. We could also ask the CVC5 devs for changes in regards to how they build/link their libraries? We will not be the only ones facing this problem i guess.
daniel-raffler
commented
5 days ago We need to update the bindings in JavaSMT, because CVC5 has changed the API in some parts.
I've started a new branch to update the bindings when they introduced the new TermManager interface. It was never merged as #310 is still not quite fixed, but maybe this could be a starting point for an upgrade?
The branch can be found here: https://github.com/sosy-lab/java-smt/tree/310-cvc5-termmanager-update
kfriedberger
commented
5 days ago Thanks for the hint to the branch. This is a good starting point for further development.
kfriedberger
commented
3 days ago I started a discussion about skolemization: https://github.com/cvc5/cvc5/discussions/11331 And a bug report about interpolation: https://github.com/cvc5/cvc5/issues/11332
CVC5 has released several new versions since it was integrated into JavaSMT: https://github.com/cvc5/cvc5/releases . We should provide an up-to-date version.
The update of CVC5 consists of two major parts:
1. Java code
The update of JavaSMT's internal bindings should be straight forward. The update can be started locally without publishing a new library of CVC5, by just providing the latest release version of CVC5 in some PATH directory.
2. Library update
With the library update, we need to consider the following points:
Issues with linking CVC5:
libpoly,libpolyxx, andlibgmp, even more on Windows. This is not an issue during the runtime of an application, but makes developement and publication/distribution complex and errorprone. Other solvers provide or build only one or two files, like MathSAT withmathsatjor Z3 withz3andz3java. The prolematic point might be a collisision on library names in the future, e.g., if more solvers link against their version ofgmp.$./../lib/<name>and version numbers when accessing their dependencies. This directory structure is not available in JavaSMT. Up to now, we compiled the library on our own and patched the paths as needed for JavaSMT. With more operating systems, this issue grows (and I do currently not know how to patch such references indll/dylibfiles).