A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions

Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Morgan Deters

This site provides our paper A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions and related material at CAV 2014.

An extended version of our paper at CAV 2014 can be found below.

All materials to reproduce the experimental evaluation in our paper can be found below.

Downloads

• Paper at CAV 2014
• Extended version of our paper at CAV 2014
• README for the artifact
• Artifact [tgz]
  This artifact provides the raw data logs, results files, binaries, sources, scripts, benchmarks, etc., used for the experiments in this paper are available as a single (250MB!) tarball with the following md5sum: 0d4e350520795e4c8fc018e88433b70a
• Benchmarks [tgz]
  All benchmarks (50MB) and translation tools we used are also contained in the archive above. You can view the benchmarks-README.txt without downloading the benchmarks archive.
  The tarball contains original Kaluza benchmarks, the "SMT-LIB" (cvc4) translations of those, and the Z3-str translations of the SMTLIB set.
  It also contains the KaluzaTranslator tool (to translate from Kaluza format to CVC4-style SMT-LIB format) and the "z3str-translator" tool to convert the CVC4-style SMT-LIB into Z3-str-style SMT-LIB.

Solver Configurations

We have used the following versions in our experiments:

• CVC4 version 1.4 pre-release (commit ef5d5880)
• The latest Kaluza as of January 2014, available from http://webblaze.cs.berkeley.edu/2010/kaluza/ (the exact version used is in the archive above)
  • Hampi (required by Kaluza), available from http://people.csail.mit.edu/akiezun/hampi/ (the exact version used is in the archive above)
  • Yices version 1.0.27 (required by Kaluza), available from http://yices.csl.sri.com/cgi-bin/yices-newlicense.cgi?file=yices-1.0.27-i686-pc-linux-gnu-static-gmp.tar.gz (for license reasons, this binary is not in the above archive)
• Z3-str version 20140120, available from http://sourceforge.net/projects/z3str/ (the exact version used is in the archive above)
  • Z3 version 4.1.1 (required by Z3-str, modified according to README.txt in the Z3-str package), available from http://z3.codeplex.com/releases/view/95640 (the exact version used is in the archive above)

Please note that:

• CVC4 was compiled as configure --gpl production-cln-staticbinary
• CVC4, Kaluza and Z3-str were run as default settings

More details are available in the README.txt file in the artifact above.

Results

The compiled results are available as a CSV file, available in the artifact above. For convenience, it also available here. It is documented in the README file above.