Update CVC5 to 1.2.X

[daniel-raffler]

Hello everyone,
this PR will update CVC5 to the latest version and rewrites the solver backend to use the new TermManager interface. It also changes the build process so that only a single library is produced and all dependencies are statically linked. In addition we added multi-arch support for linux on arm64 and windows on x64.

There were some issues in CVC5 that had to be fixed and we're still waiting on cvc5/cvc5#11730 before this can be merged.

[daniel-raffler]

@kfriedberger: Could you have a look at the last commit that adds multi-arch support? I've tried it for arm64 with qemu, but I don't have a windows machine to test the binaries. (You'll have to use the repository from the CVC5 pull request here if you want to build the binaries yourself)

[daniel-raffler]

The missing pull request for CVC5 has now been merged and we can build from main

[kfriedberger]

On first look, this is an impressive PR, and it looks quite good:

• version update of CVC5 ✔️
• arm64-support for CVC5 ✔️
• x64-support for WIndows ❔ (does not yet work)

I will test compilation and different OS soon.

[baierd]

The proof generation/traversal API has changed compared to older versions. Do we include the new API and maybe even a native test for it?

If not, can we add that in this PR? It would be helpful for @gcarpio21 s proof interface.
(I can also do it, but probably in the later half of next week)

[kfriedberger]

We compile the "full" API of CVC5, including all new features. I assume that the API changes from your comment refer to plain Java API. This should be done outside of this PR, as it might be independent of native code and low-level bindings. A separate PR would also allow to integrate this PR here soonish, and work on proofs later.

[gcarpio21]

The proof generation/traversal API has changed compared to older versions. Do we include the new API and maybe even a native test for it?

If not, can we add that in this PR? It would be helpful for @gcarpio21 s proof interface. (I can also do it, but probably in the later half of next week)

For the purposes of correctly retrieving proofs from CVC5 I have written a test in the CVC5NativeAPITest class using some of the methods exposed in this version of CVC5 to handle proofs. I could add the test to this PR.

[kfriedberger]

If there is just one additional test, then feel free to add it within this PR.

[kfriedberger]

Update for the Windows build artifact:
There are remaining non-static dependencies to GCC-specific libraries. CVC5 packages them as additional libraries into the released archive:
https://github.com/cvc5/cvc5/blob/7bf5d3e457aa5c40b325b0e687de5a972b0dad4e/.github/actions/add-package/action.yml#L40-L42
We can do the same, and add those dependencies into Ivy and Maven. We would need to load those libraries before loading CVC5.

Alternative (maybe future work, not part of this PR):
CVC5 has already a fully running build-system that publishes (nearly) static binaries for more platforms (see https://github.com/cvc5/cvc5/releases ). For other solvers, like Z3, we use the direct release instead of building our own binaries. This would only require to download several archives, and then repackage them according to our needs. This might allow us to even support MacOS on x64 and arm64 platform without any compilation overhead.