diff options
Diffstat (limited to 'src/theory/strings/sequences_rewriter.cpp')
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 87 |
1 files changed, 47 insertions, 40 deletions
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 1d82f9abd..1ccb67490 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(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(Rational(0)); if (d_arithEntail.check(ne[1], false) && d_arithEntail.check(ne[2], true)) @@ -586,8 +586,7 @@ Node SequencesRewriter::rewriteLength(Node node) Kind nk0 = node[0].getKind(); if (node[0].isConst()) { - Node retNode = - nm->mkConst(CONST_RATIONAL, Rational(Word::getLength(node[0]))); + Node retNode = nm->mkConstInt(Rational(Word::getLength(node[0]))); return returnRewrite(node, retNode, Rewrite::LEN_EVAL); } else if (nk0 == kind::STRING_CONCAT) @@ -600,8 +599,8 @@ Node SequencesRewriter::rewriteLength(Node node) { if (tmpNode[i].isConst()) { - node_vec.push_back(nm->mkConst( - CONST_RATIONAL, Rational(Word::getLength(tmpNode[i])))); + node_vec.push_back( + nm->mkConstInt(Rational(Word::getLength(tmpNode[i])))); } else { @@ -634,7 +633,7 @@ Node SequencesRewriter::rewriteLength(Node node) } else if (nk0 == SEQ_UNIT) { - Node retNode = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node retNode = nm->mkConstInt(Rational(1)); return returnRewrite(node, retNode, Rewrite::LEN_SEQ_UNIT); } return node; @@ -1311,7 +1310,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) } else if (r.getKind() == kind::REGEXP_ALLCHAR) { - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x)); return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA); } @@ -1344,7 +1343,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) Node flr = RegExpEntail::getFixedLengthForRegexp(r[0]); if (!flr.isNull()) { - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); if (flr == one) { NodeBuilder nb(AND); @@ -1430,7 +1429,7 @@ Node SequencesRewriter::rewriteMembership(TNode node) if (constStr.isNull()) { // x in re.++(_*, _, _) ---> str.len(x) >= 2 - Node num = nm->mkConst(CONST_RATIONAL, Rational(allSigmaMinSize)); + Node num = nm->mkConstInt(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); @@ -1722,10 +1721,9 @@ 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(CONST_RATIONAL, Rational(0)), n), - nm->mkNode(LT, n, nm->mkNode(STRING_LENGTH, s))); + Node cond = nm->mkNode(AND, + nm->mkNode(LEQ, nm->mkConstInt(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); @@ -1761,22 +1759,22 @@ Node SequencesRewriter::rewriteSeqNth(Node node) Node ret = nm->mkGroundValue(s.getType().getSequenceElementType()); return returnRewrite(node, ret, Rewrite::SEQ_NTH_TOTAL_OOB); } - else - { - return node; - } } - else + + if (s.getKind() == SEQ_UNIT && i.isConst() && i.getConst<Rational>().isZero()) { - return node; + Node ret = s[0]; + return returnRewrite(node, ret, Rewrite::SEQ_NTH_UNIT); } + + return node; } Node SequencesRewriter::rewriteCharAt(Node node) { Assert(node.getKind() == STRING_CHARAT); NodeManager* nm = NodeManager::currentNM(); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node one = nm->mkConstInt(Rational(1)); Node retNode = nm->mkNode(STRING_SUBSTR, node[0], node[1], one); return returnRewrite(node, retNode, Rewrite::CHARAT_ELIM); } @@ -1854,7 +1852,7 @@ Node SequencesRewriter::rewriteSubstr(Node node) } } } - Node zero = nm->mkConst(CONST_RATIONAL, cvc5::Rational(0)); + Node zero = nm->mkConstInt(cvc5::Rational(0)); // if entailed non-positive length or negative start point if (d_arithEntail.check(zero, node[1], true)) @@ -2047,6 +2045,8 @@ Node SequencesRewriter::rewriteUpdate(Node node) { Assert(node.getKind() == kind::STRING_UPDATE); Node s = node[0]; + Node i = node[1]; + Node x = node[2]; if (s.isConst()) { if (Word::isEmpty(s)) @@ -2084,6 +2084,16 @@ Node SequencesRewriter::rewriteUpdate(Node node) } } + if (s.getKind() == STRING_REV) + { + NodeManager* nm = NodeManager::currentNM(); + Node idx = nm->mkNode(MINUS, + nm->mkNode(STRING_LENGTH, s), + nm->mkNode(PLUS, i, nm->mkConst(Rational(1)))); + Node ret = nm->mkNode(STRING_REV, nm->mkNode(STRING_UPDATE, s, idx, x)); + return returnRewrite(node, ret, Rewrite::UPD_REV); + } + return node; } @@ -2453,7 +2463,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(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NEG); } @@ -2471,7 +2481,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(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_MAX); } Assert(node[2].getConst<Rational>().sgn() >= 0); @@ -2482,13 +2492,12 @@ Node SequencesRewriter::rewriteIndexof(Node node) std::size_t ret = Word::find(s, t, start); if (ret != std::string::npos) { - Node retv = - nm->mkConst(CONST_RATIONAL, Rational(static_cast<unsigned>(ret))); + Node retv = nm->mkConstInt(Rational(static_cast<unsigned>(ret))); return returnRewrite(node, retv, Rewrite::IDOF_FIND); } else if (children0.size() == 1) { - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NFIND); } } @@ -2500,14 +2509,14 @@ Node SequencesRewriter::rewriteIndexof(Node node) if (node[2].getConst<Rational>().sgn() == 0) { // indexof( x, x, 0 ) --> 0 - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(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(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART); } Node emp = Word::mkEmptyWord(stype); @@ -2538,7 +2547,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(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_LEN); } @@ -2620,7 +2629,7 @@ Node SequencesRewriter::rewriteIndexof(Node node) else { // str.contains( x, y ) --> false implies str.indexof(x,y,z) --> -1 - Node negone = nm->mkConst(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::IDOF_NCTN); } } @@ -2675,12 +2684,12 @@ Node SequencesRewriter::rewriteIndexofRe(Node node) Node s = node[0]; Node r = node[1]; Node n = node[2]; - Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)); + Node zero = nm->mkConstInt(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(CONST_RATIONAL, Rational(-1)); + Node ret = nm->mkConstInt(Rational(-1)); return returnRewrite(node, ret, Rewrite::INDEXOF_RE_INVALID_INDEX); } @@ -2695,15 +2704,14 @@ 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(CONST_RATIONAL, Rational(-1)); + Node negone = nm->mkConstInt(Rational(-1)); return returnRewrite(node, negone, Rewrite::INDEXOF_RE_MAX_INDEX); } uint32_t start = nrat.getNumerator().toUnsignedInt(); 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, + Node ret = nm->mkConstInt( Rational(match.first == string::npos ? -1 : static_cast<int64_t>(start + match.first))); @@ -2967,8 +2975,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(CONST_RATIONAL, Rational(0)); - Node one = nm->mkConst(CONST_RATIONAL, Rational(1)); + Node zero = nm->mkConstInt(Rational(0)); + Node one = nm->mkConstInt(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 @@ -3491,8 +3499,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n) Node val; if (isPrefix) { - val = - NodeManager::currentNM()->mkConst(CONST_RATIONAL, ::cvc5::Rational(0)); + val = NodeManager::currentNM()->mkConstInt(::cvc5::Rational(0)); } else { @@ -3527,7 +3534,7 @@ Node SequencesRewriter::canonicalStrForSymbolicLength(Node len, TypeNode stype) NodeManager* nm = NodeManager::currentNM(); Node res; - if (len.getKind() == CONST_RATIONAL) + if (len.isConst()) { // c -> "A" repeated c times Rational ratLen = len.getConst<Rational>(); |