Update CVC5 to version 1.2.0 or newer

[kfriedberger]

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. We need to update the bindings in JavaSMT, because CVC5 has changed the API in some parts.
2. We need to provide the updated library for CVC5.

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:

• OS: Linux, Windows, and MacOS are upported and CVC5 provides releases for them.
• Architecture: x64 and arm64 versions are available (low priority, depends on #380 support multiple architectures for solver binaries z3 #395).
• 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)?

Issues with linking CVC5:

• Number of libraries: The shared libraries for CVC5 require at least 6 files on Linux, including libpoly, libpolyxx, and libgmp, 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 with mathsatj or Z3 with z3 and z3java. The prolematic point might be a collisision on library names in the future, e.g., if more solvers link against their version of gmp.
• Dependencies of shared libraries: We can not directly use the provided/released shared libraries of CVC5 1.2.0 from https://github.com/cvc5/cvc5/releases , because they contain hard-coded paths like $./../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 in dll/dylib files).

[baierd]

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]

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]

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]

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]

Thanks for the hint to the branch. This is a good starting point for further development.

[kfriedberger]

I started a discussion about skolemization: cvc5/cvc5#11331
And a bug report about interpolation: cvc5/cvc5#11332