Scaling Up DPLL(T) String Solvers using Context-Dependent Simplification

Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, Cesare Tinelli

This site provides our paper Scaling Up DPLL(T) String Solvers using Context-Dependent Simplification and related material at CAV 2017.

Downloads

• Paper at CAV 2017
• Benchmarks:
  • .smt2 Benchmarks [tgz]
    The *.smt2 version of our benchmarks. This is the format used by cvc4 and z3.
  • .z3str2 Benchmarks [tgz]
    The *.z3st2 version of our benchmarks. This is the format used by z3str2.
• Binaries:
  • CVC4 Binary [tgz]
  • Z3 Binary [tgz]
  • Z3str2 Binary [tgz]

Solver Configurations

To enable individual configurations of CVC4:

• Configuration cvc4+fs is enabled by --lang=smt2 --strings-exp --rewrite-divk --strings-fmf
• Configuration cvc4+f is enabled by --lang=smt2 --strings-exp --rewrite-divk --strings-fmf --no-strings-lazy-pp
• Configuration cvc4+s is enabled by --lang=smt2 --strings-exp --rewrite-divk
• Configuration cvc4 is enabled by --lang=smt2 --strings-exp --rewrite-divk --no-strings-lazy-pp

Results

Our evaluation used the StarExec cluster for evaluation. We provide a spreadsheet results-cav17.xlsx containing detailed results of the experiments. The columns of this spreadsheet show all benchmark/solver pairs, as well as various additional tests to verify the correctness of models produced by z3 and cvc4, on benchmarks where solvers gave different answers, including timeouts. For instance the column “z3 : +cvc4-m” indicates the result of z3 on the original benchmark plus constraints corresponding to cvc4’s model. The scripts used to test the consistency of models can be found here.