From 3f3a0445fe772360d8a2da3069a5f082c031d7f8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 15 Apr 2020 02:34:33 -0500 Subject: Convert more cases of strings to words (#4206) --- src/theory/strings/sequences_rewriter.cpp | 58 +++++++++++++++---------------- 1 file changed, 29 insertions(+), 29 deletions(-) (limited to 'src/theory/strings/sequences_rewriter.cpp') diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 152f71019..d8b8765eb 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -99,20 +99,22 @@ Node SequencesRewriter::rewriteEquality(Node node) { unsigned index1 = r == 0 ? i : (c[0].size() - 1) - i; unsigned index2 = r == 0 ? i : (c[1].size() - 1) - i; - if (c[0][index1].isConst() && c[1][index2].isConst()) + Node s = c[0][index1]; + Node t = c[1][index2]; + if (s.isConst() && t.isConst()) { - CVC4::String s = c[0][index1].getConst(); - CVC4::String t = c[1][index2].getConst(); - unsigned len_short = s.size() <= t.size() ? s.size() : t.size(); - bool isSameFix = - r == 1 ? s.rstrncmp(t, len_short) : s.strncmp(t, len_short); + size_t lenS = Word::getLength(s); + size_t lenT = Word::getLength(t); + size_t lenShort = lenS <= lenT ? lenS : lenT; + bool isSameFix = r == 1 ? Word::rstrncmp(s, t, lenShort) + : Word::strncmp(s, t, lenShort); if (!isSameFix) { Node ret = NodeManager::currentNM()->mkConst(false); return returnRewrite(node, ret, Rewrite::EQ_NFIX); } } - if (c[0][index1] != c[1][index2]) + if (s != t) { break; } @@ -280,7 +282,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) } // ------- rewrites for (= "" _) - Node empty = nm->mkConst(::CVC4::String("")); + Node empty = Word::mkEmptyWord(stype); for (size_t i = 0; i < 2; i++) { if (node[i] == empty) @@ -585,7 +587,6 @@ Node SequencesRewriter::rewriteConcat(Node node) Assert(node.getKind() == kind::STRING_CONCAT); Trace("strings-rewrite-debug") << "Strings::rewriteConcat start " << node << std::endl; - NodeManager* nm = NodeManager::currentNM(); std::vector node_vec; Node preNode = Node::null(); for (Node tmpNode : node) @@ -598,8 +599,10 @@ Node SequencesRewriter::rewriteConcat(Node node) { if (tmpNode[0].isConst()) { - preNode = nm->mkConst( - preNode.getConst().concat(tmpNode[0].getConst())); + std::vector wvec; + wvec.push_back(preNode); + wvec.push_back(tmpNode[0]); + preNode = Word::mkWord(wvec); node_vec.push_back(preNode); } else @@ -1114,14 +1117,14 @@ Node SequencesRewriter::rewriteMembership(TNode node) { if (x.isConst()) { - String s = x.getConst(); - if (s.size() == 0) + size_t xlen = Word::getLength(x); + if (xlen == 0) { Node retNode = nm->mkConst(true); // e.g. (str.in.re "" (re.* (str.to.re x))) ----> true return returnRewrite(node, retNode, Rewrite::RE_EMPTY_IN_STR_STAR); } - else if (s.size() == 1) + else if (xlen == 1) { if (r[0].getKind() == STRING_TO_REGEXP) { @@ -1317,7 +1320,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) // above, we strip components to construct an equivalent membership: // (str.++ xi .. xj) in (re.++ rk ... rl). Node xn = utils::mkConcat(mchildren, stype); - Node emptyStr = nm->mkConst(String("")); + Node emptyStr = Word::mkEmptyWord(stype); if (children.empty()) { // If we stripped all components on the right, then the left is @@ -1913,7 +1916,7 @@ Node SequencesRewriter::rewriteContains(Node node) Node ret; if (nc2.size() > 1) { - Node emp = nm->mkConst(CVC4::String("")); + Node emp = Word::mkEmptyWord(stype); NodeBuilder<> nb2(kind::AND); for (const Node& n2 : nc2) { @@ -1969,7 +1972,7 @@ Node SequencesRewriter::rewriteContains(Node node) { if (node[1].isConst()) { - CVC4::String t = node[1].getConst(); + Node t = node[1]; // Below, we are looking for a constant component of node[0] // has no overlap with node[1], which means we can split. // Notice that if the first or last components had no @@ -1981,9 +1984,8 @@ Node SequencesRewriter::rewriteContains(Node node) // constant contains if (node[0][i].isConst()) { - CVC4::String s = node[0][i].getConst(); // if no overlap, we can split into disjunction - if (s.noOverlapWith(t)) + if (Word::noOverlapWith(node[0][i], node[1])) { std::vector nc0; utils::getConcat(node[0], nc0); @@ -2067,7 +2069,7 @@ Node SequencesRewriter::rewriteContains(Node node) Node ctn = d_stringsEntail.checkContains(node[1], node[0][2]); if (!ctn.isNull() && !ctn.getConst()) { - Node empty = nm->mkConst(String("")); + Node empty = Word::mkEmptyWord(stype); Node ret = nm->mkNode( kind::STRING_STRCTN, nm->mkNode(kind::STRING_STRREPL, node[0][0], node[0][1], empty), @@ -2093,7 +2095,7 @@ Node SequencesRewriter::rewriteContains(Node node) // Note: Length-based reasoning is not sufficient to get this rewrite. We // can neither show that str.len(str.replace("", x, y)) - str.len(x) >= 0 // nor str.len(x) - str.len(str.replace("", x, y)) >= 0 - Node emp = nm->mkConst(CVC4::String("")); + Node emp = Word::mkEmptyWord(stype); if (node[0] == node[1][1] && node[1][0] == emp) { Node ret = nm->mkNode(kind::EQUAL, emp, node[1]); @@ -2169,7 +2171,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) Node negone = nm->mkConst(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART); } - Node emp = nm->mkConst(CVC4::String("")); + Node emp = Word::mkEmptyWord(stype); if (node[0] != emp) { // indexof( x, x, z ) ---> indexof( "", "", z ) @@ -2390,7 +2392,7 @@ Node SequencesRewriter::rewriteReplace(Node node) // if 1 >= (str.len x) and (= y "") ---> (= y1 "") ... (= yn "") if (StringsEntail::checkLengthOne(node[0])) { - Node empty = nm->mkConst(String("")); + Node empty = Word::mkEmptyWord(stype); Node rn1 = Rewriter::rewrite( rewriteEqualityExt(nm->mkNode(EQUAL, node[1], empty))); if (rn1 != node[1]) @@ -2480,7 +2482,7 @@ Node SequencesRewriter::rewriteReplace(Node node) // substitute y with "" in the third argument. Note that the third argument // does not matter when the str.replace does not apply. // - Node empty = nm->mkConst(::CVC4::String("")); + Node empty = Word::mkEmptyWord(stype); std::vector emptyNodes; bool allEmptyEqs; @@ -2890,9 +2892,8 @@ Node SequencesRewriter::rewriteStrReverse(Node node) Node x = node[0]; if (x.isConst()) { - std::vector nvec = node[0].getConst().getVec(); - std::reverse(nvec.begin(), nvec.end()); - Node retNode = nm->mkConst(String(nvec)); + // reverse the characters in the constant + Node retNode = Word::reverse(x); return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST); } else if (x.getKind() == STRING_CONCAT) @@ -2928,8 +2929,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) } if (n[0].isConst()) { - CVC4::String t = n[0].getConst(); - if (t.isEmptyString()) + if (Word::isEmpty(n[0])) { Node ret = NodeManager::currentNM()->mkConst(true); return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY_CONST); -- cgit v1.2.3