Strip non-matching beginning from indexof operator (#2885)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 23 Mar 2019 00:15:53 +0000 (00:15 +0000)
committerGitHub <noreply@github.com>
Sat, 23 Mar 2019 00:15:53 +0000 (00:15 +0000)
commit3df45c5613bcd4c81d4cabae4bb7c98ce69d7141
treee712f906c2ebdc7220c42f363c8a00ce2d9939da
parent821d4b1c6c3ce3c711e9a24216758febf0937cf0
Strip non-matching beginning from indexof operator (#2885)

This commit adds a rewrite that strips endpoints from `str.indexof`
operators if they don't overlap with the string that is being searched
for using `stripConstantEndpoints()`. In addition to that, it makes
`stripConstantEndpoints()` slightly more aggressive by allowing it to
drop substring components that have zero overlap with the string that we
are looking at. Finally, the commit fixes the default argument for
`fullRewriter` of `checkEntailContains()` to be true instead of false,
which should allow for more rewriting opportunities.
src/theory/strings/theory_strings_rewriter.cpp
src/theory/strings/theory_strings_rewriter.h
test/unit/theory/theory_strings_rewriter_white.h