A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions
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
- 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.
We have used the following versions in our experiments:
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
file in the artifact above.
The compiled results are available as a CSV file, available in the artifact
above. For convenience, it also available
It is documented in the README file above.