diff options
Diffstat (limited to 'src/theory/strings')
| -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 * |