diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 20:19:26 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-01-23 20:19:26 -0800 |
commit | 77a9cac1975f30153c16493fba673b50e0331509 (patch) | |
tree | 2b677352a36beff717b2031eb39044a5337d4f8f | |
parent | f6a940be26d6255fe61e7bbce85f06a77cf0010d (diff) |
Fix
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 42 |
1 files changed, 36 insertions, 6 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 6ec1f28c6..f1cdcb9e9 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2285,18 +2285,48 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { // past the first position in node[0] that contains node[1], we can drop std::vector<Node> nb; std::vector<Node> ne; - int cc = componentContains(children0, children1, nb, ne, true, 0); - if (cc != -1 && (!nb.empty() || !ne.empty())) + int cc = componentContains(children0, children1, nb, ne, true, 1); + if (cc != -1 && !ne.empty()) { // For example: // str.indexof(str.++(x,y,z),y,0) ---> str.indexof(str.++(x,y),y,0) Node nn = mkConcat(kind::STRING_CONCAT, children0); - Node ret = nm->mkNode( - PLUS, - nm->mkNode(STRING_LENGTH, mkConcat(STRING_CONCAT, nb)), - nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2])); + Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]); return returnRewrite(node, ret, "idof-def-ctn"); } + + if (node[1].isConst()) + { + CVC4::String t = node[1].getConst<String>(); + if (t.size() == 1) + { + size_t i = 0; + std::vector<Node> children0; + getConcat(node[0], children0); + for (size_t size = children0.size(); i < size; i++) + { + Node ectn = checkEntailContains(children0[i], node[1]); + if (ectn.isNull() || ectn.getConst<bool>()) + { + break; + } + } + Assert(i < children0.size()); + + if (i > 0) + { + std::vector<Node> pfxv(children0.begin(), children0.begin() + i); + children0.erase(children0.begin(), children0.begin() + i); + Node pfx = mkConcat(STRING_CONCAT, pfxv); + Node nn = mkConcat(STRING_CONCAT, children0); + Node ret = nm->mkNode( + PLUS, + nm->mkNode(STRING_LENGTH, pfx), + nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2])); + return returnRewrite(node, ret, "idof-def-ctn"); + } + } + } } // strip symbolic length |