From 9f7e50702810aafd0ce67a79b4c5906b48aec4b4 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 21 Nov 2018 16:47:57 -0800 Subject: 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 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'src/theory') 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))); -- cgit v1.2.3