diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-15 02:13:19 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-15 02:32:32 -0700 |
commit | f33c2bd9de5a811e14ea3b7201284e45ae4cbc6e (patch) | |
tree | 78e56cc7136cc19e2519be6df236ebaaba12d1cb | |
parent | ea24eec6b7914550c84cb09c569b7fc80304d8e7 (diff) |
Strengthen str.indexof rewriterewIndexOf
-rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 36 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_rewriter_white.h | 23 |
2 files changed, 41 insertions, 18 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 4ab81da7c..884e9ed86 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1989,24 +1989,6 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { return returnRewrite(node, ret, "idof-def-ctn"); } } - - // strip symbolic length - Node new_len = node[2]; - std::vector<Node> nr; - if (stripSymbolicLength(children0, nr, 1, new_len)) - { - // For example: - // z>str.len( x1 ) and str.contains( x2, y )-->true - // implies - // str.indexof( str.++( x1, x2 ), y, z ) ---> - // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) ) - Node nn = mkConcat(kind::STRING_CONCAT, children0); - Node ret = - nm->mkNode(kind::PLUS, - nm->mkNode(kind::MINUS, node[2], new_len), - nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len)); - return returnRewrite(node, ret, "idof-strip-sym-len"); - } } else { @@ -2016,6 +1998,24 @@ Node TheoryStringsRewriter::rewriteIndexof( Node node ) { } } + // strip symbolic length + Node new_len = node[2]; + std::vector<Node> nr; + if (stripSymbolicLength(children0, nr, 1, new_len)) + { + // For example: + // z>str.len( x1 ) + // implies + // str.indexof( str.++( x1, x2 ), y, z ) ---> + // str.len( x1 ) + str.indexof( x2, y, z-str.len(x1) ) + Node nn = mkConcat(kind::STRING_CONCAT, children0); + Node ret = + nm->mkNode(kind::PLUS, + nm->mkNode(kind::MINUS, node[2], new_len), + nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len)); + return returnRewrite(node, ret, "idof-strip-sym-len"); + } + if (node[2].isConst() && node[2].getConst<Rational>().sgn()==0) { std::vector<Node> cb; diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index acee9754b..e2ab390b9 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -245,4 +245,27 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node res_a_repl_substr = Rewriter::rewrite(a_repl_substr); TS_ASSERT_EQUALS(res_repl_substr_a, res_a_repl_substr); } + + void testRewriteIndexOf() + { + TypeNode strType = d_nm->stringType(); + + Node a = d_nm->mkConst(::CVC4::String("A")); + Node b = d_nm->mkConst(::CVC4::String("B")); + Node x = d_nm->mkVar("x", strType); + Node one = d_nm->mkConst(Rational(1)); + + // Same normal form for: + // + // (str.to.int (str.indexof "A" x 1)) + // + // (str.to.int (str.indexof "B" x 1)) + Node a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, one); + Node itos_a_idof_x = d_nm->mkNode(kind::STRING_ITOS, a_idof_x); + Node b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, one); + Node itos_b_idof_x = d_nm->mkNode(kind::STRING_ITOS, b_idof_x); + Node res_itos_a_idof_x = Rewriter::rewrite(itos_a_idof_x); + Node res_itos_b_idof_x = Rewriter::rewrite(itos_b_idof_x); + TS_ASSERT_EQUALS(res_itos_a_idof_x, res_itos_b_idof_x); + } }; |