From 9f7e50702810aafd0ce67a79b4c5906b48aec4b4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 21 Nov 2018 16:47:57 -0800 Subject: [PATCH] Add rewrite for (str.substr s x y) --> "" (#2695) This commit adds the rewrite `(str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)`. --- src/theory/strings/theory_strings_rewriter.cpp | 18 +++++++++++++++--- .../theory/theory_strings_rewriter_white.h | 9 +++++++++ 2 files changed, 24 insertions(+), 3 deletions(-) diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index b7821d562..57a99532e 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -1764,6 +1764,15 @@ Node TheoryStringsRewriter::rewriteSubstr(Node node) return returnRewrite(node, ret, "ss-non-zero-len-entails-oob"); } + // (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s) + Node geq_zero_start = + Rewriter::rewrite(nm->mkNode(kind::GEQ, node[1], zero)); + if (checkEntailArithWithAssumption(geq_zero_start, zero, tot_len, false)) + { + Node ret = nm->mkConst(String("")); + return returnRewrite(node, ret, "ss-geq-zero-start-entails-emp-s"); + } + // (str.substr s x x) ---> "" if (str.len s) <= 1 if (node[1] == node[2] && checkEntailLengthOne(node[0])) { @@ -4506,6 +4515,10 @@ bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption, { candVars.insert(curr); } + else if (curr.getKind() == kind::STRING_LENGTH) + { + candVars.insert(curr); + } } // Check if any of the candidate variables are in n @@ -4522,8 +4535,7 @@ bool TheoryStringsRewriter::checkEntailArithWithEqAssumption(Node assumption, toVisit.push_back(currChild); } - if (curr.isVar() && Theory::theoryOf(curr) == THEORY_ARITH - && candVars.find(curr) != candVars.end()) + if (candVars.find(curr) != candVars.end()) { v = curr; break; @@ -4576,7 +4588,7 @@ bool TheoryStringsRewriter::checkEntailArithWithAssumption(Node assumption, y = assumption[0][0]; } - Node s = nm->mkBoundVar("s", nm->stringType()); + Node s = nm->mkBoundVar("slackVal", nm->stringType()); Node slen = nm->mkNode(kind::STRING_LENGTH, s); assumption = Rewriter::rewrite( nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::PLUS, y, slen))); diff --git a/test/unit/theory/theory_strings_rewriter_white.h b/test/unit/theory/theory_strings_rewriter_white.h index 42ac2cdd9..8139f1c2e 100644 --- a/test/unit/theory/theory_strings_rewriter_white.h +++ b/test/unit/theory/theory_strings_rewriter_white.h @@ -221,6 +221,7 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite 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 negone = d_nm->mkConst(Rational(-1)); Node zero = d_nm->mkConst(Rational(0)); Node one = d_nm->mkConst(Rational(1)); Node two = d_nm->mkConst(Rational(2)); @@ -330,6 +331,14 @@ class TheoryStringsRewriterWhite : public CxxTest::TestSuite Node substr_itos = d_nm->mkNode( kind::STRING_SUBSTR, d_nm->mkNode(kind::STRING_ITOS, x), x, x); sameNormalForm(substr_itos, empty); + + // (str.substr s (* (- 1) (str.len s)) 1) ---> empty + Node substr = d_nm->mkNode( + kind::STRING_SUBSTR, + s, + d_nm->mkNode(kind::MULT, negone, d_nm->mkNode(kind::STRING_LENGTH, s)), + one); + sameNormalForm(substr, empty); } void testRewriteConcat() -- 2.30.2