projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a4b0e46) | patch
Add rewrites for str.replace in str.contains (#2623)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 12 Oct 2018 07:21:51 +0000 (00:21 -0700)
committerGitHub <noreply@github.com>
Fri, 12 Oct 2018 07:21:51 +0000 (00:21 -0700)
commit9f5fb42580e00370ea461be5a00f8debfb59b636
tree29e982dfcd63311aeadbcc5f33560247990e54f3tree
parenta4b0e462833f89bea6a35e0adcf103201b9ebca1commit | diff
 Add rewrites for str.replace in str.contains  (#2623)

This commit adds two rewrites for `(str.contains (str.replace x y x) z) ---> (str.contains x z)`, either when `z = y` or `(str.len z) <= 1`. Additionally, the commit adds `(str.contains (str.replace x y z) w) ---> true` if `(str.contains x w) --> true` and `(str.contains z w) ---> true`.
src/theory/strings/theory_strings_rewriter.cpp diff | blob | history
test/unit/theory/theory_strings_rewriter_white.h diff | blob | history