summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/query_generator.cpp
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-03-23 00:15:53 +0000
committerGitHub <noreply@github.com>2019-03-23 00:15:53 +0000
commit3df45c5613bcd4c81d4cabae4bb7c98ce69d7141 (patch)
treee712f906c2ebdc7220c42f363c8a00ce2d9939da /src/theory/quantifiers/query_generator.cpp
parent821d4b1c6c3ce3c711e9a24216758febf0937cf0 (diff)
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.
Diffstat (limited to 'src/theory/quantifiers/query_generator.cpp')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback