Replace CVC4 by bitwuzla and CVC5

[schuessf]

We currently still on an old CVC4 build from 2020 (and there is an even older cvc4nyu variant from 2016). CVC4 is now deprecated and suceeded by CVC5, and we mainly use it as a bitvector solver for trace checks. Therefore, this PR makes the following changes:

• bitwuzla replaces CVC4 in all trace checks for bitvectors. Bitwuzla performs better than both CVC4 and CVC5 on bitvectors (see below).
• CVC5 replaces CVC4 for other, non-bitvector use cases (e.g., more general trace checks and various term unit tests). Since this usage isn't required for deployment, I chose to not include CVC5 in the release ZIP.
  CVC5 is also included in the release ZIP.

These changes have the following advantages:

• Both bitwuzla and CVC5 are actively maintained and provide ARM builds, which is also important for Add ARM64 build support for Linux and macOS #772.
• We mainly used CVC4 as a bitvector solver, and bitwuzla specializes in exactly that.
• bitwuzla also supports interpolation for bitvectors (TACAS26), which we could consider using in the future.

I also ran some evaluations on the performance impact of this change for bitvector trace checks (with a timeout of 90s):

• SolverComparison.table.html shows that bitwuzla alone slightly outperforms CVC4, while CVC5 performs worse than CVC4 (quite surprising). Therefore, I chose bitwuzla over CVC5 for bitvector trace checks.
• FoxComparison.table.html shows that bitwuzla and CVC4 perform comparably within our standard Fox strategy, but we could consider another evaluation run with a higher timeout for more representative results.

[danieldietsch]

I overlooked your comment about not including cvc5 in deployment, but I disagree. You should include it, because otherwise, we cannot easily test it. Or is there any other reason for not deploying it?

[schuessf]

I overlooked your comment about not including cvc5 in deployment, but I disagree. You should include it, because otherwise, we cannot easily test it. Or is there any other reason for not deploying it?

I guess, the questions simply is: what is the purpose of the ZIP? If it's meant mainly to run with our default settings, we don't really need to include it, but I can of course also include it.
(Initially I thought that bitwuzla alone could replace CVC4, but since its use isn't limited to bitvectors, we also need CVC5.)

As for the tests, we can still run the nightly tests with CVC5 even without including it in the ZIP, since it's only required within releaseScripts for that purpose.

[danieldietsch]

I think you should be able to run everything with it. Think of it this way: if you write a paper where you use CVC5, future people can just pull the current .zip and use your config to re-run.

[schuessf]

I think you should be able to run everything with it. Think of it this way: if you write a paper where you use CVC5, future people can just pull the current .zip and use your config to re-run.

Good point, I just included CVC5 for the deployment.

[danieldietsch]

Why was update_mathsat removed?

[schuessf]

I simply replaced update_mathsat with update_bitwuzla, as we usually just want to update a single solver and now I wanted to update bitwuzla instead of MathSAT 😉

[schuessf]

I just made a new benchmark run with a timeout of 300s instead of 90s to evaluate the impact on our Fox strategy (see here). It turns out that simply replacing CVC4 with bitwuzla while keeping the original solver order actually causes us to succeed on 10 fewer tasks (see FOX vs. OLDFOX). If, however, we instead place bitwuzla first in the solver order (since it was also shown to be the most successful solver based on the results above) we are able to solve 64 more tasks (FOX_BW; see implementation here). Therefore, I suppose it is reasonable to also change the solver order in the Fox strategy as part of this PR, but we could make this change afterwards instead.