diff options
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 9 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.h | 2 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 45 |
3 files changed, 38 insertions, 18 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 349a8b4fb..6ec1f28c6 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -2285,13 +2285,16 @@ 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, 1); - if (cc != -1 && !ne.empty()) + int cc = componentContains(children0, children1, nb, ne, true, 0); + if (cc != -1 && (!nb.empty() || !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(kind::STRING_STRIDOF, nn, node[1], node[2]); + Node ret = nm->mkNode( + PLUS, + nm->mkNode(STRING_LENGTH, mkConcat(STRING_CONCAT, nb)), + nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2])); return returnRewrite(node, ret, "idof-def-ctn"); } } 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 * diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 760e35471..457e78cfc 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -500,19 +500,33 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite sameNormalForm(idof, negOne); } - // (str.indexof (str.++ (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 - // 1) "B") 0) ---> -1 + Node substr_substr_idof = + d_nm->mkNode(kind::STRING_SUBSTR, substr_idof, zero, one); + + // (str.indexof (str.++ + // (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1) "B") 0) ---> + // -1 { - Node idof = d_nm->mkNode( - kind::STRING_STRIDOF, - d_nm->mkNode( - kind::STRING_CONCAT, - d_nm->mkNode(kind::STRING_SUBSTR, substr_idof, zero, one), - b), - a, - zero); + Node idof = + d_nm->mkNode(kind::STRING_STRIDOF, + d_nm->mkNode(kind::STRING_CONCAT, substr_substr_idof, b), + a, + zero); sameNormalForm(idof, negOne); } + + // (str.indexof (str.++ + // (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1) "A") 0) ---> + // (str.len (str.substr (str.substr x 0 (str.indexof "A" 0)) 0 1)) + { + Node lhs = + d_nm->mkNode(kind::STRING_STRIDOF, + d_nm->mkNode(kind::STRING_CONCAT, substr_substr_idof, a), + a, + zero); + Node rhs = d_nm->mkNode(kind::STRING_LENGTH, substr_substr_idof); + sameNormalForm(lhs, rhs); + } } void testRewriteReplace() @@ -918,8 +932,10 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite } { - // (str.contains (str.substr (str.substr x 0 (str.indexof x "AAC" zero)) 0 - // n) "B") ---> false + // (str.contains + // (str.substr + // (str.substr x 0 (str.indexof x "AAC" zero)) 0 n) "B") ---> + // false Node ctn = d_nm->mkNode( kind::STRING_STRCTN, d_nm->mkNode(kind::STRING_SUBSTR, @@ -931,8 +947,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite } { - // (str.contains (str.substr (str.substr x 0 (str.indexof x "A" zero)) 0 - // 1) "A") ---> false + // (str.contains + // (str.substr (str.substr x 0 (str.indexof x "A" zero)) 0 1) "A") ---> + // false Node ctn = d_nm->mkNode( kind::STRING_STRCTN, d_nm->mkNode( |