Remove support for cvc4

[podhrmic]

In support of GaloisInc/cryptol#1806

• update documentation to use cvc5
• remove cvc4 related functions from the codebase
• update tests to use cvc5

Created with Claude Code and manually reviewed and edited.

[RyanGlScott]

Thanks! For posterity's sake, see also GaloisInc/cryptol#1967 for the Cryptol-side changes.

(We will also want to drop CVC4 support in Crux as well.)

[RyanGlScott]

Happily, cvc5 does seem to do a little better than cvc4 on this problem. On my machine, it wasn't until around n = 18 where cvc5 started to chug noticeably.

[podhrmic]

Done

[RyanGlScott]

Perhaps this should say "not supported" rather than "not currently supported", given that we don't plan on re-adding cvc4 support in the future.

[podhrmic]

Done

[sauclovian-g]

We shouldn't drop CVC4 support entirely until it's been deprecated in at least one and ideally two releases (once to warn, once to hide by default) so most of this seems premature. It is going to be marked warn-deprecated in the release currently under way (1.5) so in principle we can remove it entirely after we release 1.6.

[podhrmic]

Right on. In that case we can either keep this MR here and update it later, or drop it entirely. This sort of work (removing small bits of code throughout the codebase) is something Claude is good at, so it is easy to recreate.

[sauclovian-g]

My inclination would be to keep it, although it'll need to be rebased occasionally. If you like, I can take charge of it and attend to that in the future...

[podhrmic]

Sure thing, happy to hand it over!

[sauclovian-g]

Ok, I rebased it (since it conflicted with last night's deprecation changes) and stuck on a commit to avoid the use of error.

I'm going to mark it as a draft until the necessary deprecation cycle steps happen so it doesn't get merged by accident.

[sauclovian-g]

Hmm, intriguing, looks like maybe we can't fail on certain cvc4 triggers? Will look into it

[RyanGlScott]

9d815fb subtly changed SAW's behavior vis-à-vis exception handling. Before, args would be evaluated lazily, which meant that by the time that their values are forced, they are within a try expression, and there is a catch-all Left (_ :: SomeException) case to ensure that any errors thrown during the evaluation of args would be caught.

After 9d815fb, args is no longer defined in a let binding, but instead in a monadic bind. As a result, it is now evaluated eagerly rather than lazily, which means that errors thrown during args' evaluation are thrown outside of the try expression. This is what causes the errors seen in CI.

Why is the cvc4 not supported error being thrown in the first place? It's because when you invoke saw with caching enabled (as the CI does), one of the first things SAW does is check for mismatched solver versions in the cache. As a result, it will query the versions of all SMT solvers. CVC4's version check happens to be the first one that falls down (even if we still supported CVC4, I would expect that the error in the OpenSMT case below it would also trigger).

My suggestion would be to refactor the code which defines args to avoid using errors at all, as I don't think this code was ever intended to throw any sort of exception.

[sauclovian-g]

It had previously been using error for OpenSMT. But I think the problem is that we shouldn't be asking for the version of solvers we don't support. This arises from the SolverBackend enumeration in SolverCache including (now) three solvers we don't support, just because SBV mentions them, and the allBackends definition including everything in the enumeration.

However, it also looks like the id numbers arising from that enumeration appear in the on-disk solver cache, so changing it will cause existing solver caches to come unstuck. (Is that right? It sure appears that SolverCacheValue is stored in LMDB, anyway. How does LMDB encode data it writes to disk?)

Therefore I think we should change allBackends to list only the supported backends. And cleanMismatchedVersionsSolverCache should be extended to check if entries contain a version for a solver that we don't know, and treat such entries as stale. Plus SolverBackend should get a comment warning that it has to be stable.

(I also note in passing that the cleanMismatched code generates a separate write transaction for every entry it's removing; this is clearly silly...)

[RyanGlScott]

However, it also looks like the id numbers arising from that enumeration appear in the on-disk solver cache, so changing it will cause existing solver caches to come unstuck. [...] Is that right?

I believe so, yes. A bit unfortunate, but probably not much we can do there, short of a cache migration strategy. I'm not particularly excited about doing that, so I say we just accept the fact that we'll incur cache misses on old caches going forward.

How does LMDB encode data it writes to disk?

At a high level, each SolverCacheValue is translated to JSON, converted into a CBOR-based representation, and then writes the CBOR (represented as a ByteString) to disk using LMDB.

Therefore I think we should change allBackends to list only the supported backends. And cleanMismatchedVersionsSolverCache should be extended to check if entries contain a version for a solver that we don't know, and treat such entries as stale.

This all sounds reasonable to me.

[sauclovian-g]

JSON ... CBOR ...

If I follow the docs, I think that means the constructors of SolverBackend end up in the on-disk cache as strings rather than as integers. In which case we can reorder it, just not remove old names...

[sauclovian-g]

The version probe stuff has been merged in #3082, and I've rebased over that.

[RyanGlScott]

FYI: I have opened GaloisInc/crucible#1766 to drop CVC4 support on the Crucible side. We should make sure to include these changes here as a submodule bump when we decide to pull the trigger on removing CVC4 support.

[sauclovian-g]

Properly speaking, that shouldn't be until after the next SAW release; in the last release the CVC4 ops were warn-deprecated, and at least in principle they should go out in one release as hide-deprecated before they're removed entirely.