diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-23 00:15:53 +0000 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-23 00:15:53 +0000 |
commit | 3df45c5613bcd4c81d4cabae4bb7c98ce69d7141 (patch) | |
tree | e712f906c2ebdc7220c42f363c8a00ce2d9939da /src/theory | |
parent | 821d4b1c6c3ce3c711e9a24216758febf0937cf0 (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')
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 24 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 2 |
2 files changed, 25 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 0763fa7d5..27393e5d4 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2318,6 +2318,22 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]); return returnRewrite(node, ret, "idof-def-ctn"); } + + // Strip components from the beginning that are guaranteed not to match + if (stripConstantEndpoints(children0, children1, nb, ne, 1)) + { + // str.indexof(str.++("AB", x, "C"), "C", 0) ---> + // 2 + str.indexof(str.++(x, "C"), "C", 0) + Node ret = + nm->mkNode(kind::PLUS, + nm->mkNode(kind::STRING_LENGTH, + mkConcat(kind::STRING_CONCAT, nb)), + nm->mkNode(kind::STRING_STRIDOF, + mkConcat(kind::STRING_CONCAT, children0), + node[1], + node[2])); + return returnRewrite(node, ret, "idof-strip-cnst-endpts"); + } } // strip symbolic length @@ -3664,6 +3680,14 @@ bool TheoryStringsRewriter::stripConstantEndpoints(std::vector<Node>& n1, // str.contains( str.++( "c", x ), str.++( "cd", y ) ) overlap = r == 0 ? s.overlap(t) : t.overlap(s); } + else + { + // if we are looking at a substring, we can remove the component + // if there is no overlap + // e.g. str.contains( str.++( str.substr( "c", i, j ), x), "a" ) + // --> str.contains( x, "a" ) + removeComponent = ((r == 0 ? s.overlap(t) : t.overlap(s)) == 0); + } } else if (sss.empty()) // only if not substr { diff --git a/src/theory/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h index 8b0072f52..81bc29ad6 100644 --- a/src/theory/strings/theory_strings_rewriter.h +++ b/src/theory/strings/theory_strings_rewriter.h @@ -472,7 +472,7 @@ class TheoryStringsRewriter { * @return true node if it can be shown that `a` contains `b`, false node if * it can be shown that `a` does not contain `b`, null node otherwise */ - static Node checkEntailContains(Node a, Node b, bool fullRewriter = false); + static Node checkEntailContains(Node a, Node b, bool fullRewriter = true); /** entail non-empty * |