Comparison of SBV and What4 as generic SMT solvers

[Vekhir]

In 2020, #117 proposed to switch away from using STP and Yices directly, to instead use a more generic SMTlib-based solver.
The proposal there mentions sbv as the preferred choice. In the mean time, what4 has become available, so those two are compared to assess their drawbacks in switching to them.

The 3 categories of comparison are:

1. GHC Support: Which/How many versions would need to be supported for the desired GHC compatibility?
2. Distro availability: Which versions are available by default in various distros?
3. Solver support: Which solvers can be used as backend?

GHC Support

SBV

The SBV support is determined from the changelog:

SBV version	Minimum supported GHC version	Maximum supported GHC version
7.12 - 8.0	8.0 (possibly 7.10.3)	8.6
8.1 - 8.4	8.4	8.6
8.5 - 8.10	8.4	8.10
8.11 - 8.17	8.4	9.0
9.0 - 9.2	8.4	9.4
10.1 - 10.2	8.4	9.6
10.3+	8.4	9.8+

What4

The What4 support is determined from the changelog and from the support of versions.

What4 version	Minimum supported GHC version	Maximum supported GHC version
1.0 - 1.1	8.2	8.10
1.2 - 1.2.1	8.2	9.0
1.3	8.2	9.2
1.4	8.2	9.4
1.5	8.2	9.6
1.5.1	8.8	9.6
1.6 - 1.6.1	8.8	9.8
1.6.2+	8.8	9.10+

Distro availability

Package versions and availability based on pkgs.org

SBV

OS	Arch Linux	Debian 10	Debian 11	Debian 12	Debian 13	Debian Sid	Fedora 40	Fedora 41	OpenSuse	Ubuntu 20.04	Ubuntu 22.04	Ubuntu 24.04	Ubuntu 24.10
Version	9.1	7.12	8.7	8.17	10.2	10.2	-	-	-	7.13	8.7	10.2	10.2

What4

OS	Arch Linux	Debian 10	Debian 11	Debian 12	Debian 13	Debian Sid	Fedora 40	Fedora 41	OpenSuse	Ubuntu 20.04	Ubuntu 22.04	Ubuntu 24.04	Ubuntu 24.10
Version	1.5.1	-	-	1.3	1.5.1	1.5.1	1.5.1	1.5.1	-	-	-	1.5.1	1.5.1

Solver support

SBV keeps track of supported solvers via SMTSolverVersions.md.
What4 support is taken from the description.
OS support via pkgs.org

Solver	SBV	What4	Arch Linux	Debian	Fedora	Ubuntu
ABC	Yes	No	Yes	No	Yes	No
Boolector	Yes	Yes	No	Yes	No	Yes
Bitwuzla	8.17+	1.6+	Yes	No	No	No
CVC4	Yes	Yes	Yes	Yes	No	Yes
CVC5	8.17+	1.4+	No	Yes (12)	Yes	Yes (24.04)
dReal	8.8+	Yes	No	No	No	No
MathSat	Yes	No	No	No	No	No
OpenSMT	10.3+	No	No	No	No	No
STP	No	Yes	Yes	No	Yes	No
Yices	Yes	Yes	Yes	No	Yes	No
Z3	Yes	Yes	Yes	Yes	Yes	Yes

SBV generally focuses on Z3 (which is the default there), using the latest features where possible. Yices is supported by both, so that can continue to be used. STP is only supported by What4.
Depending on version, not all features may be supported.

Conclusion

Using what4 would immediately mean dropping support for GHC <8.2. sbv does possibly support GHC 7.10.3, though only before v8.1 which is positively ancient. In more general terms, sbv tends to support more and older releases for GHC. It also has better solver support with the exception of STP, though it's neither default for bsc nor is it impossible to add if it's needed.
When choosing to use sbv, allowing use as far back as 7.12 would cover both all supported GHC releases as well as the major distributions out-of-the-box. There are 38 versions since then (as of 11.1), so might be done more on an on-demand basis where issues occur. sbv itself only supports the latest 3 versions (currently 10.12, 11.0, 11.1).
The solvers to focus on could be Z3 for its widespread use and Yices as the current default.

What do you think? I believe this summary to be useful to make an informed decision.

Examples

SBV

:m Data.SBV
e :: [SMTConfig] <- getAvailableSolvers
f =  \x -> x `shiftL` 2 .== 4 * (x::SWord8)
proveWithAll e $ f

yields [(Yices,0.002754131s,Q.E.D.),(Z3,0.012029021s,Q.E.D.)] when Yices and Z3 are installed.

[quark17]

Thanks!

There are various open issues about the SMT solvers, and I apologize that they're not consolidated in one place. It's worth stepping back and asking what are the concerns that people are trying to solve. For example, I think many of the proposals are from people who are trying to package BSC, and are having difficulty in building or want to simplify the install for their users.

My current feeling is that we should do this:

1. Statically link BSC with the SMT solvers, and eliminate all the run-time nonsense from dynamic linking (we wouldn't ship separate object files or need to set LD_LIBRARY_PATH in a wrapper; and there'd be no need for a stub library, because the BSC source could include or not include whatever solver one wants at compile time)
2. Since STP is now available on GitHub, replace the very old STP snapshot with a reference to that repo (git submodule), which has a recent v2.3.4 tag

Less important, but we could also do the following:

3. Make STP the default solver, since it beat out the other solvers (including Yices and Z3) in the bit-vector category (which is what BSC uses) at SMT-COMP in 2023 (which was the latest at the time I last thought of this, though I don't see that STP participated in 2024?): https://smt-comp.github.io/2023/results/qf-bitvec-single-query
4. Update the Yices submodule to the latest tagged release (v2.6.5)

The SMT solver versions that we currently use have not had a bug, and there's a lot to be said for that and not upgrading unnecessarily. But I'm certainly fine with upgrading if it improves speed and if it makes building easier (particular to keep up with support for newer architectures and compilers). However, the speed of the SMT solvers is not currently a big concern. But it would be good to have some examples that stress-test the scaling of SMT solver use in scheduling, typechecking, and logic optimization.

Supporting the ability to plug in other solvers is also nice, but is not what people are clamouring for. I'm all for adding an SMTLib interface, as a way to allow people to experiment with other solvers, but I don't think it's a solution to the priority problems -- I think it would need to be an optional solver (via a flag like --sat-smtlib) alongside at least one statically-linked solver. While I did say that speed is not a big concern, I would worry about making the solver slower -- because there are designs that schedule large numbers of rules and need millions of queries. I suspect that an SMTLib interface might add overhead that slows down queries (relative to a statically linked solver using the current C APIs). The way that BSC currently uses solvers is through direct interfaces that return pointers to constructed terms, and BSC caches those pointers to avoid re-creating those structures. It's possible that the solver side of the SMTLib interface might do some of that, but I would want to see some experiments. In any case, my understanding of SMTLib is that it passes queries as strings, which means that BSC would have to construct strings and the solver side would need to parse the string, on every query, which again I worry is a source of overhead.