projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1fe3247) | patch
Improve strings rewriter for contains (#1207)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 28 Oct 2017 04:16:38 +0000 (23:16 -0500)
committerGitHub <noreply@github.com>
Sat, 28 Oct 2017 04:16:38 +0000 (23:16 -0500)
commit675e82e32a34911163f9de0e6389eb107be5b0f1
treea3215999b2f1550325b77d19e14a61793dafce35tree
parent1fe3247a0bf4b806f99c161dcc9c6644aabb38c1commit | diff
Improve strings rewriter for contains (#1207)

* Work on rewriter for string contains.

* Add rewrites that mix str.to.int and str.contains. Documentation, add regression.

* Minor

* Minor

* Address review, add a few TODOs. Improve some non-digit -> not is number.

* Fix

* Simplify.

* Clang format, minor fixing of comments.
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
src/theory/strings/theory_strings_rewriter.h diff | blob | history
src/util/regexp.cpp diff | blob | history
src/util/regexp.h diff | blob | history
test/regress/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/issue1189.smt2 [new file with mode: 0644] blob