diff options
Diffstat (limited to 'src/theory/strings/sequences_rewriter.cpp')
| -rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 169 |
1 files changed, 135 insertions, 34 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index babf260fc..fbb40f212 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -352,7 +352,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) } else if (ne.getKind() == STRING_SUBSTR) { - Node zero = nm->mkConst(Rational(0)); + Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); if (d_arithEntail.check(ne[1], false) && d_arithEntail.check(ne[2], true)) @@ -586,7 +586,8 @@ Node SequencesRewriter::rewriteLength(Node node) Kind nk0 = node[0].getKind(); if (node[0].isConst()) { - Node retNode = nm->mkConst(Rational(Word::getLength(node[0]))); + Node retNode = + nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(node[0]))); return returnRewrite(node, retNode, Rewrite::LEN_EVAL); } else if (nk0 == kind::STRING_CONCAT) @@ -599,8 +600,8 @@ Node SequencesRewriter::rewriteLength(Node node) { if (tmpNode[i].isConst()) { - node_vec.push_back( - nm->mkConst(Rational(Word::getLength(tmpNode[i])))); + node_vec.push_back(nm->mkConst( + CONST_RATIONAL, Rational(Word::getLength(tmpNode[i])))); } else { @@ -633,7 +634,7 @@ Node SequencesRewriter::rewriteLength(Node node) } else if (nk0 == SEQ_UNIT) { - Node retNode = nm->mkConst(Rational(1)); + Node retNode = nm->mkConst(CONST_RATIONAL, Rational(1)); return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT); } return node; @@ -978,11 +979,17 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) Assert(nk == REGEXP_UNION || nk == REGEXP_INTER); Trace("strings-rewrite-debug") << "Strings::rewriteAndOrRegExp start " << node << std::endl; + NodeManager* nm = NodeManager::currentNM(); std::vector<Node> node_vec; std::vector<Node> polRegExp[2]; + // list of constant string regular expressions (str.to_re c) + std::vector<Node> constStrRe; + // list of all other regular expressions + std::vector<Node> otherRe; for (const Node& ni : node) { - if (ni.getKind() == nk) + Kind nik = ni.getKind(); + if (nik == nk) { for (const Node& nic : ni) { @@ -992,7 +999,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) } } } - else if (ni.getKind() == REGEXP_NONE) + else if (nik == REGEXP_NONE) { if (nk == REGEXP_INTER) { @@ -1000,7 +1007,7 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) } // otherwise, can ignore } - else if (ni.getKind() == REGEXP_STAR && ni[0].getKind() == REGEXP_ALLCHAR) + else if (nik == REGEXP_STAR && ni[0].getKind() == REGEXP_ALLCHAR) { if (nk == REGEXP_UNION) { @@ -1010,13 +1017,103 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node) } else if (std::find(node_vec.begin(), node_vec.end(), ni) == node_vec.end()) { + if (nik == STRING_TO_REGEXP && ni[0].isConst()) + { + if (nk == REGEXP_INTER) + { + if (!constStrRe.empty()) + { + Assert(constStrRe[0][0] != ni[0]); + // (re.inter .. (str.to_re c1) .. (str.to_re c2) ..) ---> re.none + // for distinct constant strings c1, c2. + Node ret = nm->mkNode(kind::REGEXP_NONE); + return returnRewrite( + node, ret, Rewrite::RE_INTER_CONST_CONST_CONFLICT); + } + } + else + { + Assert(nk == REGEXP_UNION); + } + constStrRe.push_back(ni); + } + else + { + otherRe.push_back(ni); + uint32_t pindex = nik == REGEXP_COMPLEMENT ? 1 : 0; + Node nia = pindex == 1 ? ni[0] : ni; + polRegExp[pindex].push_back(nia); + } node_vec.push_back(ni); - uint32_t pindex = ni.getKind() == REGEXP_COMPLEMENT ? 1 : 0; - Node nia = pindex == 1 ? ni[0] : ni; - polRegExp[pindex].push_back(nia); } } - NodeManager* nm = NodeManager::currentNM(); + Trace("strings-rewrite-debug") + << "Partition constant components " << constStrRe.size() << " / " + << otherRe.size() << std::endl; + // go back and process constant strings against the others + if (!constStrRe.empty()) + { + std::unordered_set<Node> toRemove; + for (const Node& c : constStrRe) + { + Assert(c.getKind() == STRING_TO_REGEXP && c[0].getKind() == CONST_STRING); + cvc5::String s = c[0].getConst<String>(); + for (const Node& r : otherRe) + { + Trace("strings-rewrite-debug") + << "Check " << c << " vs " << r << std::endl; + // skip if already removing, or not constant + if (!RegExpEntail::isConstRegExp(r) + || toRemove.find(r) != toRemove.end()) + { + Trace("strings-rewrite-debug") << "...skip" << std::endl; + continue; + } + // test whether c from (str.to_re c) is in r + if (RegExpEntail::testConstStringInRegExp(s, 0, r)) + { + Trace("strings-rewrite-debug") << "...included" << std::endl; + if (nk == REGEXP_INTER) + { + // (re.inter .. (str.to_re c) .. R ..) ---> + // (re.inter .. (str.to_re c) .. ..) when c in R + toRemove.insert(r); + } + else + { + // (re.union .. (str.to_re c) .. R ..) ---> + // (re.union .. .. R ..) when c in R + toRemove.insert(c); + break; + } + } + else + { + Trace("strings-rewrite-debug") << "...not included" << std::endl; + if (nk == REGEXP_INTER) + { + // (re.inter .. (str.to_re c) .. R ..) ---> re.none + // if c is not a member of R. + Node ret = nm->mkNode(kind::REGEXP_NONE); + return returnRewrite( + node, ret, Rewrite::RE_INTER_CONST_RE_CONFLICT); + } + } + } + } + if (!toRemove.empty()) + { + std::vector<Node> nodeVecTmp; + node_vec.swap(nodeVecTmp); + for (const Node& nvt : nodeVecTmp) + { + if (toRemove.find(nvt) == toRemove.end()) + { + node_vec.push_back(nvt); + } + } + } + } // use inclusion tests for (const Node& negMem : polRegExp[1]) { @@ -1214,7 +1311,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) } else if (r.getKind() == kind::REGEXP_ALLCHAR) { - Node one = nm->mkConst(Rational(1)); + Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x)); return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA); } @@ -1247,7 +1344,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) Node flr = RegExpEntail::getFixedLengthForRegexp(r[0]); if (!flr.isNull()) { - Node one = nm->mkConst(Rational(1)); + Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); if (flr == one) { NodeBuilder nb(AND); @@ -1310,7 +1407,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) if (constStr.isNull()) { // x in re.++(_*, _, _) ---> str.len(x) >= 2 - Node num = nm->mkConst(Rational(allSigmaMinSize)); + Node num = nm->mkConst(CONST_RATIONAL, Rational(allSigmaMinSize)); Node lenx = nm->mkNode(STRING_LENGTH, x); Node retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num); return returnRewrite(node, retNode, Rewrite::RE_CONCAT_PURE_ALLCHAR); @@ -1602,9 +1699,10 @@ TrustNode SequencesRewriter::expandDefinition(Node node) Node s = node[0]; Node n = node[1]; // seq.nth(s, n) --> ite(0 <= n < len(s), seq.nth_total(s,n), Uf(s, n)) - Node cond = nm->mkNode(AND, - nm->mkNode(LEQ, nm->mkConst(Rational(0)), n), - nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s))); + Node cond = + nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConst(CONST_RATIONAL, Rational(0)), n), + nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s))); Node ss = nm->mkNode(SEQ_NTH_TOTAL, s, n); Node uf = SkolemCache::mkSkolemSeqNth(s.getType(), "Uf"); Node u = nm->mkNode(APPLY_UF, uf, s, n); @@ -1654,7 +1752,7 @@ Node SequencesRewriter::rewriteCharAt(Node node) { Assert(node.getKind() == STRING_CHARAT); NodeManager* nm = NodeManager::currentNM(); - Node one = nm->mkConst(Rational(1)); + Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); Node retNode = nm->mkNode(STRING_SUBSTR, node[0], node[1], one); return returnRewrite(node, retNode, Rewrite::CHARAT_ELIM); } @@ -1732,7 +1830,7 @@ Node SequencesRewriter::rewriteSubstr(Node node) } } } - Node zero = nm->mkConst(cvc5::Rational(0)); + Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0)); // if entailed non-positive length or negative start point if (d_arithEntail.check(zero, node[1], true)) @@ -2331,7 +2429,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (node[2].isConst() && node[2].getConst<Rational>().sgn() < 0) { // z<0 implies str.indexof( x, y, z ) --> -1 - Node negone = nm->mkConst(Rational(-1)); + Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NEG); } @@ -2349,7 +2447,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) // We know that, due to limitations on the size of string constants // in our implementation, that accessing a position greater than // rMaxInt is guaranteed to be out of bounds. - Node negone = nm->mkConst(Rational(-1)); + Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_MAX); } Assert(node[2].getConst<Rational>().sgn() >= 0); @@ -2360,12 +2458,13 @@ Node SequencesRewriter::rewriteIndexof(Node node) std::size_t ret = Word::find(s, t, start); if (ret != std::string::npos) { - Node retv = nm->mkConst(Rational(static_cast<unsigned>(ret))); + Node retv = + nm->mkConst(CONST_RATIONAL, Rational(static_cast<unsigned>(ret))); return returnRewrite(node, retv, Rewrite::IDOF_FIND); } else if (children0.size() == 1) { - Node negone = nm->mkConst(Rational(-1)); + Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NFIND); } } @@ -2377,14 +2476,14 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (node[2].getConst<Rational>().sgn() == 0) { // indexof( x, x, 0 ) --> 0 - Node zero = nm->mkConst(Rational(0)); + Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START); } } if (d_arithEntail.check(node[2], true)) { // y>0 implies indexof( x, x, y ) --> -1 - Node negone = nm->mkConst(Rational(-1)); + Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART); } Node emp = Word::mkEmptyWord(stype); @@ -2415,7 +2514,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (d_arithEntail.check(len1, len0m2, true)) { // len(x)-z < len(y) implies indexof( x, y, z ) ----> -1 - Node negone = nm->mkConst(Rational(-1)); + Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_LEN); } @@ -2497,7 +2596,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) else { // str.contains( x, y ) --> false implies str.indexof(x,y,z) --> -1 - Node negone = nm->mkConst(Rational(-1)); + Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NCTN); } } @@ -2552,12 +2651,12 @@ Node SequencesRewriter::rewriteIndexofRe(Node node) Node s = node[0]; Node r = node[1]; Node n = node[2]; - Node zero = nm->mkConst(Rational(0)); + Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); Node slen = nm->mkNode(STRING_LENGTH, s); if (d_arithEntail.check(zero, n, true) || d_arithEntail.check(n, slen, true)) { - Node ret = nm->mkConst(Rational(-1)); + Node ret = nm->mkConst(CONST_RATIONAL, Rational(-1)); return returnRewrite(node, ret, Rewrite::INDEXOF_RE_INVALID_INDEX); } @@ -2572,7 +2671,7 @@ Node SequencesRewriter::rewriteIndexofRe(Node node) // We know that, due to limitations on the size of string constants // in our implementation, that accessing a position greater than // rMaxInt is guaranteed to be out of bounds. - Node negone = nm->mkConst(Rational(-1)); + Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); return returnRewrite(node, negone, Rewrite::INDEXOF_RE_MAX_INDEX); } @@ -2580,6 +2679,7 @@ Node SequencesRewriter::rewriteIndexofRe(Node node) Node rem = nm->mkConst(s.getConst<String>().substr(start)); std::pair<size_t, size_t> match = firstMatch(rem, r); Node ret = nm->mkConst( + CONST_RATIONAL, Rational(match.first == string::npos ? -1 : static_cast<int64_t>(start + match.first))); @@ -2843,8 +2943,8 @@ Node SequencesRewriter::rewriteReplace(Node node) nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(children1, stype)); Node maxLen1 = nm->mkNode(kind::PLUS, partLen1, lastChild1[2]); - Node zero = nm->mkConst(Rational(0)); - Node one = nm->mkConst(Rational(1)); + Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); Node len0 = nm->mkNode(kind::STRING_LENGTH, node[0]); Node len0_1 = nm->mkNode(kind::PLUS, len0, one); // Check len(t) + j > len(x) + 1 @@ -3367,7 +3467,8 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) Node val; if (isPrefix) { - val = NodeManager::currentNM()->mkConst(::cvc5::Rational(0)); + val = + NodeManager::currentNM()->mkConst(CONST_RATIONAL, ::cvc5::Rational(0)); } else { |