From 71bd93b9e073cb9d7d8e14eb5b279f29d45c1019 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 10 Oct 2018 12:30:06 -0700 Subject: [PATCH] Add length-based rewrites for (str.substr _ _ _) (#2610) --- .../strings/theory_strings_rewriter.cpp | 35 ++++++++++++++++ .../theory/theory_strings_rewriter_white.h | 40 +++++++++++++++++-- 2 files changed, 72 insertions(+), 3 deletions(-) diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index b2778298a..00a711a31 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1610,6 +1610,33 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) return returnRewrite(node, ret, "ss-len-non-pos"); } + if (node[0].getKind() == STRING_SUBSTR) + { + // (str.substr (str.substr x a b) c d) ---> "" if c >= b + // + // Note that this rewrite can be generalized to: + // + // (str.substr x a b) ---> "" if a >= (str.len x) + // + // This can be done when we generalize our entailment methods to + // accept an optional context. Then we could conjecture that + // (str.substr x a b) rewrites to "" and do a case analysis: + // + // - a < 0 or b < 0 (the result is trivially empty in these cases) + // - a >= (str.len x) assuming that { a >= 0, b >= 0 } + // + // For example, for (str.substr (str.substr x a a) a a), we could + // then deduce that under those assumptions, "a" is an + // over-approximation of the length of (str.substr x a a), which + // then allows us to reason that the result of the whole term must + // be empty. + if (checkEntailArith(node[1], node[0][2])) + { + Node ret = nm->mkConst(::CVC4::String("")); + return returnRewrite(node, ret, "ss-start-geq-len"); + } + } + std::vector n1; getConcat(node[0], n1); @@ -1673,6 +1700,14 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) Node ret = nm->mkConst(::CVC4::String("")); return returnRewrite(node, ret, "ss-start-entails-zero-len"); } + + // (str.substr s x x) ---> "" if (str.len s) <= 1 + Node one = nm->mkConst(CVC4::Rational(1)); + if (node[1] == node[2] && checkEntailArith(one, tot_len)) + { + Node ret = nm->mkConst(::CVC4::String("")); + return returnRewrite(node, ret, "ss-len-one-z-z"); + } } if (!curr.isNull()) { diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index d038b310e..d967ab793 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -152,7 +152,9 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node empty = d_nm->mkConst(::CVC4::String("")); Node a = d_nm->mkConst(::CVC4::String("A")); + Node b = d_nm->mkConst(::CVC4::String("B")); Node abcd = d_nm->mkConst(::CVC4::String("ABCD")); + Node zero = d_nm->mkConst(Rational(0)); Node two = d_nm->mkConst(Rational(2)); Node three = d_nm->mkConst(Rational(3)); @@ -198,6 +200,26 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite kind::STRING_SUBSTR, abcd, d_nm->mkNode(kind::PLUS, x, two), x); res = TheoryStringsRewriter::rewriteSubstr(n); TS_ASSERT_EQUALS(res, n); + + // (str.substr (str.substr s x x) x x) -> "" + n = d_nm->mkNode( + kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_SUBSTR, s, x, x), x, x); + sameNormalForm(n, empty); + + // Same normal form for: + // + // (str.substr (str.replace "" s "B") x x) + // + // (str.replace "" s (str.substr "B" x x))) + Node lhs = d_nm->mkNode(kind::STRING_SUBSTR, + d_nm->mkNode(kind::STRING_STRREPL, empty, s, b), + x, + x); + Node rhs = d_nm->mkNode(kind::STRING_STRREPL, + empty, + s, + d_nm->mkNode(kind::STRING_SUBSTR, b, x, x)); + sameNormalForm(lhs, rhs); } void testRewriteConcat() @@ -297,6 +319,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite void testRewriteIndexOf() { + TypeNode intType = d_nm->integerType(); TypeNode strType = d_nm->stringType(); Node a = d_nm->mkConst(::CVC4::String("A")); @@ -305,17 +328,20 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node b = d_nm->mkConst(::CVC4::String("B")); Node x = d_nm->mkVar("x", strType); Node y = d_nm->mkVar("y", strType); - Node one = d_nm->mkConst(Rational(2)); + Node negOne = d_nm->mkConst(Rational(-1)); + Node one = d_nm->mkConst(Rational(1)); + Node two = d_nm->mkConst(Rational(2)); Node three = d_nm->mkConst(Rational(3)); + Node i = d_nm->mkVar("i", intType); // 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 a_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, a, x, two); 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 b_idof_x = d_nm->mkNode(kind::STRING_STRIDOF, b, x, two); Node itos_b_idof_x = d_nm->mkNode(kind::STRING_ITOS, b_idof_x); sameNormalForm(itos_a_idof_x, itos_b_idof_x); @@ -333,6 +359,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite y, three); sameNormalForm(idof_abcd, idof_aaad); + + // (str.indexof (str.substr x 1 i) "A" i) ---> -1 + Node idof_substr = + d_nm->mkNode(kind::STRING_STRIDOF, + d_nm->mkNode(kind::STRING_SUBSTR, x, one, i), + a, + i); + sameNormalForm(idof_substr, negOne); } void testRewriteReplace() -- 2.30.2