How to choose the underlying SMT solvers?

[孟昭逸]

Hi CPAchecker's developers,

When I use CPAchecker, what criteria should I use to select an SMT solver?

As far as I know, the default SMT solver of CPAchecker is MathSAT5.

Why do you choose it as the default tool? 

Under what circumstances should I need to change the underly solver to Z3, CVC4 or other tools?

Whether these tools are good at dealing with different problems?

Thanks in advance!

Best,

Zhaoyi

[Karlheinz Friedberger]

Hi Zhaoyi,

The selection of the best SMT solver is a hard question.
It mostly depends on the set of features which are required by the analysis.

- If you execute an analysis based on predicate abstraction,
then interpolation is required (supported by MathSAT5, SMTInterpol, Princess).
For plain BMC or kInduction, interpolation is not required and all solvers can be applied.

- For encoding program behavior and variables with bit-precise formulae,
the theory of BV is needed (supported by MathSAT5, CVC4, Boolector, Z3, Princess).
For encoding variables as plain integers (no bitvectors!), all solvers can be applied (except Boolector).

- If support for array theory (we can encode arrays as uninterpreted function or real array theory),
the solver should support this feature (i think all do).

- If formula visitors are required by the analysis, the visitation methods must be supported.
This works best in mature solvers like MathSAT5, Z3, SMTInterpol, and Princess.

- If you work on Windows, we do deliver the necessary binaries automatically.
For testing you might want to use the JVM-based solvers like SMTInterpol and Princess,
which work on all systems.

That was just the (maybe incomplete) list of the external view of a solver.
Internally, some solvers are more mature than others.

Some solvers are simply faster than others for some kind of queries, e.g., because of internal heuristics.
- Z3 and MathSAT5 produce quite similar results depending on the analysis [1, Section 16].
However, Z3 misses interpolation since the latest release and is no longer available for PredicateAnalysis.
- Boolector is quite fast on BV-queries [2,3], but suffers from some unsupported features.
- SMTInterpol is good, Princess is slower.

For some users, the license needs to be taken into account.
MathSAT5 is included for research and evaluation purposes only.
The other solvers are more liberal.

Based on our own benchmark results, we chose MathSAT5 as the default SMT solver.
MathSAT5 produced the most results in a reasonable amount of time, and it supports BV theory.

Best,
Karlheinz

[1] https://www.sosy-lab.org/research/phd/2017.Wendler.Towards_Practical_Predicate_Analysis.pdf
[2] (german text:) https://www.sosy-lab.org/research/bsc/2019.Baier.Integration_des_SMT-Solvers_Boolector_in_das_Framework_JavaSMT_und_Evaluation_mit_CPAchecker.pdf
[3] https://www.sosy-lab.org/research/prs/2019-11-27_BA_IntegrationBoolectorInJavaSMT_Baier.pdf


Am 23.06.20 um 16:01 schrieb 孟昭逸:

> --
> You received this message because you are subscribed to the Google Groups "CPAchecker Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to cpachecker-use...@googlegroups.com <mailto:cpachecker-use...@googlegroups.com>.
> To view this discussion on the web visit https://groups.google.com/d/msgid/cpachecker-users/1dfbe294-0e85-4d6d-96a9-29056c66492bo%40googlegroups.com <https://groups.google.com/d/msgid/cpachecker-users/1dfbe294-0e85-4d6d-96a9-29056c66492bo%40googlegroups.com?utm_medium=email&utm_source=footer>.

--
Karlheinz Friedberger
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Room F009
Phone: 089/2180-9182

[Karlheinz Friedberger]

Correction:
If you work on Windows, we do *NOT* deliver the necessary binaries automatically.
:-)

[孟昭逸]

Hi Karlheinz,

Thanks for your timely response!

在 2020年6月24日星期三 UTC+8上午1:49:16，Karlheinz Friedberger写道：