Designing Theory Solvers with Extensions

Andrew Reynolds, Cesare Tinelli, Dejan Jovanovic, Clark Barrett

This site provides our paper Designing Theory Solvers with Extensions and related material at FROCOS 2017.

Downloads

• Paper at FROCOS 2017

Extended Theory of Strings

• For the strings experiments in Section 4, we used the master version of CVC4: CVC4, revision 3837f84a.
  • Configuration cvc4+sm is enabled by --lang=smt2 --strings-exp --rewrite-divk --strings-fmf.
  • Configuration cvc4+m is enabled by --lang=smt2 --strings-exp --rewrite-divk --no-strings-lazy-pp --strings-fmf
• The .tgz containing the binary of z3 used in our experiments can be found here: z3
• The .tgz containing the binary of z3Str2 used in our experiments can be found here: z3Str2

The benchmarks considered in this section can be downloaded here.

The spreadsheet summarizing the results for the strings benchmarks considered in this paper can be accessed here: results-strings.xlsx.

Lazy Bit-blasting for Expensive Bit-Vector Operators

• For the strings experiments in Section 5, we used a development branch of CVC4: CVC4.
  • Configuration cvc4+sm is enabled by --bv-lazy-bb-exp.
  • Configuration cvc4 is enabled by no command line parameters.

We considered the sage2 family of benchmarks from the QF_BV division of SMT LIB. For instructions downloading these benchmarks, see this page.

The spreadsheet summarizing the results for the strings benchmarks considered in this paper can be accessed here: results-bv.xlsx.

Lightweight Techniques for Non-linear Arithmetic

• For the strings experiments in Section 5, we used a development branch of CVC4: CVC4.
  • Configuration cvc4+sm is enabled by --nl-alg --nl-alg-tplanes.
  • Configuration cvc4+m is enabled by --nl-alg --nl-alg-tplanes --no-nl-alg-rewrite

We considered all benchmarks from the QF_NRA and QF_NIA divisions of SMT LIB. For instructions downloading these benchmarks, see this page.

The spreadsheet summarizing the results for the strings benchmarks considered in this paper for QF_NRA can be accessed here: results-nra.xlsx, and QF_NIA can be accessed here: results-nia.xlsx.