Define native solver packaging for CVC5 and Z3

[thpani]

Apalache may be gaining support for CVC5 as an additional SMT solver backend. Both CVC5 and Z3 expose Java APIs that rely on native solver libraries, so we should make an explicit packaging decision instead of relying on ad hoc dependency wiring.

Context

Options for CVC5:

• CVC5 publishes the Java API as the base artifact (Java classes) and native libraries separately with platform classifiers (e.g., linux-aarch_64 and linux-x86_64)
• The cvc5 POM does not pull those native classifier jars transitively, so builds that want CVC5 must add the appropriate native classifier explicitly.
• A single native library JAR is ~11MB, all published native libraries ({linux,osx,windows} x {aarch64,x86_64}) would be ~66MB.
• Adding multiple CVC5 native classifiers to the default build works as a development shortcut, but it is not a clean release strategy.

State of Z3:

• Apalache currently uses https://github.com/tudo-aqua/z3-turnkey for Z3.
• z3-turnkey is an all-in-one native bundle. The 4.14.1 jar contains the Java classes plus native libraries as above; the jar is about 60MB.
• Upstream Z3 4.16.0 is available, but its release artifacts are platform-classified GitHub release archives rather than normal Maven Central artifacts.
  For example, the Z3 4.16.0 release includes classified archives such as z3-4.16.0-arm64-glibc-2.38.zip, which contains the Java jar.

We should decide:

• Should Apalache publish platform-classified distributions, e.g. Linux x86_64, Linux aarch64, macOS aarch64, etc., pulling in only the native solver backends needed?
• Should the default distribution bundle all supported solver natives, or only the "default" solver (CVC5 treated as an optional runtime dependency where users provide the matching native jar/library themselves)?
• What should replace z3-turnkey if we want a consistent solver packaging strategy across Z3 and CVC5?

Desired outcomes

• Build wiring that selects or packages the correct native solver artifacts deliberately.
• A migration plan away from z3-turnkey (lower priority).

[konnov]

Should Apalache publish platform-classified distributions, e.g. Linux x86_64, Linux aarch64, macOS aarch64, etc., pulling in only the native solver backends needed?

This would be a nice approach to the issue. However, the user base is probably not too large yet for this to become a serious issue. This may change, if we start to bundle Apalache with the VScode plugin.

Note that Quint is downloading Apalache, so if we start publishing platform-specific distributions, the Quint team would have to integrate there.

Should the default distribution bundle all supported solver natives, or only the "default" solver (CVC5 treated as an optional runtime dependency where users provide the matching native jar/library themselves)?

For now, I would bundle everything. In principle, it would be nice to pull only the needed libraries on demand. However, the supply chain attacks may change this view. As far as I understand, most of time people just pull the docker image.

What should replace z3-turnkey if we want a consistent solver packaging strategy across Z3 and CVC5?

Do you know the status of https://github.com/tudo-aqua/cvc5-turnkey ?

[thpani]

Do you know the status of https://github.com/tudo-aqua/cvc5-turnkey ?

Yes, it's even worse behind. It bundles cvc5-1.2.0 from Aug 2024, when the latest cvc5-1.3.4 was cut 5 days ago.

[konnov]

Do you know the status of https://github.com/tudo-aqua/cvc5-turnkey ?

Yes, it's even worse behind. It bundles cvc5-1.2.0 from Aug 2024, when the latest cvc5-1.3.4 was cut 5 days ago.

Right. We also had issues with z3-turnkey lagging behind. So the plan would be to make our own version of turnkey for Apalache? This is probably easy with AI tools.

[thpani]

Maybe for z3. cvc5 is on maven.