ddsmt / ddSMT

A delta debugger for SMT benchmarks in SMT-LIB v2.
https://ddsmt.readthedocs.io
Other
50 stars 17 forks source link

Add basic support for the theory of strings #14

Closed 4tXJ7f closed 6 years ago

4tXJ7f commented 6 years ago

This commit adds support for eight common string operators (str.len, str.++, str.contains, str.substr, str.replace, str.indexof, str.prefixof, str.suffixof) and adds two passes. The first pass tries to replace terms of sort String with the empty string and the second one tries to replace terms of sort String with a fresh variable. The standard for the theory of strings has not been finalized, so the commit does not implement all proposed operators but rather a subset of operators that are commonly used.