Yices 2 default solver despite being 'optional'

[KrystalDelusion]

Using smtbmc will default to Yices 2 (an optional solver) as opposed to z3 (a required solver). If Yices 2 is not installed any code using smtbmc will fail rather than trying with the available solver(s).

[jix]

I think it would be best to change the default solver from Yices to either Boolector or to Bitwuzla, and to make that a required dependency. For the vast majority of cases I've seen, they are faster than Yices and much faster than z3. According to the git history, the default in smtbmc was switched from z3 to yices around 5 years ago. I presume that was for performance reasons and the choice fell to Yices as Boolector became open-source only later (IIRC) and Bitwuzla is a more recent Boolector fork.

Boolector and Bitwuzla do not support (* allconst *) and (* allseq *) though. Yices supports them with some limitations, but becomes unusably slow. Yices also needs a non-default option in that case, so that's currently already broken when you don't specify anything. Thus in this regard, changing the default to Boolector or Bitwuzla would not be a regression.

We could also add z3 as an automatic fallback in smtbmc when (* allconst *) or (* allseq *) are used and no explicit solver is specified. I don't think having any kind of automatic fallback depending on what is installed is a good idea though, as it's easy to cause major performance regression by installing or uninstalling a solver without updating yosys, sby or changing any sby files.

I'm not sure whether such an automated fallback for (* allconst *) or (* allseq *) would warrant keeping z3 as a required dependency though.

[nakengelhardt]

Why is z3 even non-optional, is that just a holdover from when it was the default or is it used somewhere else? If anything I think yices should be non-optional currently as that's what's used to generate the VCD for any engine that doesn't have native VCD generation. And yes, I agree that we should probably change that to boolector for performance reasons.

I wouldn't do automatic fallback, maybe print a message instead. But can we even tell within sby what the design contains?

[jix]

z3 is just a holdover, it's only non-optional in that the installation guide still says so.

We can check for allconst/allseq because write_smt2 adds ; yosys-smt2-forall as a header comment, but for just an error message we can instead make sure that smtbmc produces a useful message and that sby passes that along.