summaryrefslogtreecommitdiff
path: root/src/theory/strings/sequences_rewriter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/sequences_rewriter.cpp')
-rw-r--r--src/theory/strings/sequences_rewriter.cpp87
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>();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback