Assert(node.getKind() == kind::EQUAL);
if (node[0] == node[1])
{
- return NodeManager::currentNM()->mkConst(true);
+ Node ret = NodeManager::currentNM()->mkConst(true);
+ return returnRewrite(node, ret, Rewrite::EQ_REFL);
}
else if (node[0].isConst() && node[1].isConst())
{
- return NodeManager::currentNM()->mkConst(false);
+ Node ret = NodeManager::currentNM()->mkConst(false);
+ return returnRewrite(node, ret, Rewrite::EQ_CONST_FALSE);
}
// ( ~contains( s, t ) V ~contains( t, s ) ) => ( s == t ---> false )
// standard ordering
if (node[0] > node[1])
{
- return NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]);
+ Node ret = NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]);
+ return returnRewrite(node, ret, Rewrite::EQ_SYM);
}
return node;
}
return node;
}
+Node SequencesRewriter::rewriteLength(Node node)
+{
+ Assert(node.getKind() == STRING_LENGTH);
+ NodeManager* nm = NodeManager::currentNM();
+ Kind nk0 = node[0].getKind();
+ if (node[0].isConst())
+ {
+ Node retNode = nm->mkConst(Rational(Word::getLength(node[0])));
+ return returnRewrite(node, retNode, Rewrite::LEN_EVAL);
+ }
+ else if (nk0 == kind::STRING_CONCAT)
+ {
+ Node tmpNode = node[0];
+ if (tmpNode.getKind() == kind::STRING_CONCAT)
+ {
+ std::vector<Node> node_vec;
+ for (unsigned int i = 0; i < tmpNode.getNumChildren(); ++i)
+ {
+ if (tmpNode[i].isConst())
+ {
+ node_vec.push_back(
+ nm->mkConst(Rational(Word::getLength(tmpNode[i]))));
+ }
+ else
+ {
+ node_vec.push_back(NodeManager::currentNM()->mkNode(
+ kind::STRING_LENGTH, tmpNode[i]));
+ }
+ }
+ Node retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
+ return returnRewrite(node, retNode, Rewrite::LEN_CONCAT);
+ }
+ }
+ else if (nk0 == STRING_STRREPL || nk0 == STRING_STRREPLALL)
+ {
+ Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1]));
+ Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2]));
+ if (len1 == len2)
+ {
+ // len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x )
+ Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
+ return returnRewrite(node, retNode, Rewrite::LEN_REPL_INV);
+ }
+ }
+ else if (nk0 == STRING_TOLOWER || nk0 == STRING_TOUPPER || nk0 == STRING_REV)
+ {
+ // len( f( x ) ) == len( x ) where f is tolower, toupper, or rev.
+ Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
+ return returnRewrite(node, retNode, Rewrite::LEN_CONV_INV);
+ }
+ return node;
+}
+
// TODO (#1180) add rewrite
// str.++( str.substr( x, n1, n2 ), str.substr( x, n1+n2, n3 ) ) --->
// str.substr( x, n1, n2+n3 )
Trace("strings-rewrite-debug")
<< "Strings::rewriteConcat start " << node << std::endl;
NodeManager* nm = NodeManager::currentNM();
- Node retNode = node;
std::vector<Node> node_vec;
Node preNode = Node::null();
for (Node tmpNode : node)
std::sort(node_vec.begin() + lastIdx, node_vec.end());
TypeNode tn = node.getType();
- retNode = utils::mkConcat(node_vec, tn);
+ Node retNode = utils::mkConcat(node_vec, tn);
Trace("strings-rewrite-debug")
<< "Strings::rewriteConcat end " << retNode << std::endl;
- return retNode;
+ if (retNode != node)
+ {
+ return returnRewrite(node, retNode, Rewrite::CONCAT_NORM);
+ }
+ return node;
}
Node SequencesRewriter::rewriteConcatRegExp(TNode node)
{
// re.++( ..., empty, ... ) ---> empty
std::vector<Node> nvec;
- return nm->mkNode(REGEXP_EMPTY, nvec);
+ Node ret = nm->mkNode(REGEXP_EMPTY, nvec);
+ return returnRewrite(node, ret, Rewrite::RE_CONCAT_EMPTY);
}
else
{
return node;
}
+Node SequencesRewriter::rewriteRepeatRegExp(TNode node)
+{
+ Assert(node.getKind() == REGEXP_REPEAT);
+ NodeManager* nm = NodeManager::currentNM();
+ // ((_ re.^ n) R) --> ((_ re.loop n n) R)
+ unsigned r = utils::getRepeatAmount(node);
+ Node lop = nm->mkConst(RegExpLoop(r, r));
+ Node retNode = nm->mkNode(REGEXP_LOOP, lop, node[0]);
+ return returnRewrite(node, retNode, Rewrite::RE_REPEAT_ELIM);
+}
+
+Node SequencesRewriter::rewriteOptionRegExp(TNode node)
+{
+ Assert(node.getKind() == REGEXP_OPT);
+ NodeManager* nm = NodeManager::currentNM();
+ Node retNode =
+ nm->mkNode(REGEXP_UNION,
+ nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))),
+ node[0]);
+ return returnRewrite(node, retNode, Rewrite::RE_OPT_ELIM);
+}
+
+Node SequencesRewriter::rewritePlusRegExp(TNode node)
+{
+ Assert(node.getKind() == REGEXP_PLUS);
+ NodeManager* nm = NodeManager::currentNM();
+ Node retNode =
+ nm->mkNode(REGEXP_CONCAT, node[0], nm->mkNode(REGEXP_STAR, node[0]));
+ return returnRewrite(node, retNode, Rewrite::RE_PLUS_ELIM);
+}
+
+Node SequencesRewriter::rewriteDifferenceRegExp(TNode node)
+{
+ Assert(node.getKind() == REGEXP_DIFF);
+ NodeManager* nm = NodeManager::currentNM();
+ Node retNode =
+ nm->mkNode(REGEXP_INTER, node[0], nm->mkNode(REGEXP_COMPLEMENT, node[1]));
+ return returnRewrite(node, retNode, Rewrite::RE_DIFF_ELIM);
+}
+
+Node SequencesRewriter::rewriteRangeRegExp(TNode node)
+{
+ Assert(node.getKind() == REGEXP_RANGE);
+ if (node[0] == node[1])
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ Node retNode = nm->mkNode(STRING_TO_REGEXP, node[0]);
+ // re.range( "A", "A" ) ---> str.to_re( "A" )
+ return returnRewrite(node, retNode, Rewrite::RE_RANGE_SINGLE);
+ }
+ return node;
+}
+
bool SequencesRewriter::isConstRegExp(TNode t)
{
if (t.getKind() == kind::STRING_TO_REGEXP)
Node SequencesRewriter::rewriteMembership(TNode node)
{
NodeManager* nm = NodeManager::currentNM();
- Node retNode = node;
Node x = node[0];
Node r = node[1];
if(r.getKind() == kind::REGEXP_EMPTY)
{
- retNode = NodeManager::currentNM()->mkConst( false );
+ Node retNode = NodeManager::currentNM()->mkConst(false);
+ return returnRewrite(node, retNode, Rewrite::RE_IN_EMPTY);
}
else if (x.isConst() && isConstRegExp(r))
{
// test whether x in node[1]
CVC4::String s = x.getConst<String>();
- retNode =
+ Node retNode =
NodeManager::currentNM()->mkConst(testConstStringInRegExp(s, 0, r));
+ return returnRewrite(node, retNode, Rewrite::RE_IN_EVAL);
}
else if (r.getKind() == kind::REGEXP_SIGMA)
{
Node one = nm->mkConst(Rational(1));
- retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x));
+ Node retNode = one.eqNode(nm->mkNode(STRING_LENGTH, x));
+ return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA);
}
else if (r.getKind() == kind::REGEXP_STAR)
{
String s = x.getConst<String>();
if (s.size() == 0)
{
- retNode = nm->mkConst(true);
+ 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);
}
{
if (r[0].getKind() == STRING_TO_REGEXP)
{
- retNode = r[0][0].eqNode(x);
+ Node retNode = r[0][0].eqNode(x);
// e.g. (str.in.re "A" (re.* (str.to.re x))) ----> "A" = x
return returnRewrite(node, retNode, Rewrite::RE_CHAR_IN_STR_STAR);
}
}
if (r[0].getKind() == kind::REGEXP_SIGMA)
{
- retNode = NodeManager::currentNM()->mkConst(true);
+ Node retNode = NodeManager::currentNM()->mkConst(true);
return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA_STAR);
}
}
// x in re.++(_*, _, _) ---> str.len(x) >= 2
Node num = nm->mkConst(Rational(allSigmaMinSize));
Node lenx = nm->mkNode(STRING_LENGTH, x);
- retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
+ Node retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
return returnRewrite(node, retNode, Rewrite::RE_CONCAT_PURE_ALLCHAR);
}
else if (allSigmaMinSize == 0 && nchildren >= 3 && constIdx != 0
&& constIdx != nchildren - 1)
{
// x in re.++(_*, "abc", _*) ---> str.contains(x, "abc")
- retNode = nm->mkNode(STRING_STRCTN, x, constStr);
+ Node retNode = nm->mkNode(STRING_STRCTN, x, constStr);
return returnRewrite(node, retNode, Rewrite::RE_CONCAT_TO_CONTAINS);
}
}
mvec.push_back(
NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r[i]));
}
- retNode = NodeManager::currentNM()->mkNode(
+ Node retNode = NodeManager::currentNM()->mkNode(
r.getKind() == kind::REGEXP_INTER ? kind::AND : kind::OR, mvec);
+ return returnRewrite(node, retNode, Rewrite::RE_IN_ANDOR);
}
else if (r.getKind() == kind::STRING_TO_REGEXP)
{
- retNode = x.eqNode(r[0]);
+ Node retNode = x.eqNode(r[0]);
+ return returnRewrite(node, retNode, Rewrite::RE_IN_CSTRING);
}
else if (r.getKind() == REGEXP_RANGE)
{
// x in re.range( char_i, char_j ) ---> i <= str.code(x) <= j
Node xcode = nm->mkNode(STRING_TO_CODE, x);
- retNode =
+ Node retNode =
nm->mkNode(AND,
nm->mkNode(LEQ, nm->mkNode(STRING_TO_CODE, r[0]), xcode),
nm->mkNode(LEQ, xcode, nm->mkNode(STRING_TO_CODE, r[1])));
+ return returnRewrite(node, retNode, Rewrite::RE_IN_RANGE);
}
else if (r.getKind() == REGEXP_COMPLEMENT)
{
- retNode = nm->mkNode(STRING_IN_REGEXP, x, r[0]).negate();
- }
- else if (x != node[0] || r != node[1])
- {
- retNode = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r);
+ Node retNode = nm->mkNode(STRING_IN_REGEXP, x, r[0]).negate();
+ return returnRewrite(node, retNode, Rewrite::RE_IN_COMPLEMENT);
}
// do simple consumes
- if (retNode == node)
+ Node retNode = node;
+ if (r.getKind() == kind::REGEXP_STAR)
{
- if (r.getKind() == kind::REGEXP_STAR)
+ for (unsigned dir = 0; dir <= 1; dir++)
{
- for (unsigned dir = 0; dir <= 1; dir++)
+ std::vector<Node> mchildren;
+ utils::getConcat(x, mchildren);
+ bool success = true;
+ while (success)
{
- std::vector<Node> mchildren;
- utils::getConcat(x, mchildren);
- bool success = true;
- while (success)
+ success = false;
+ std::vector<Node> children;
+ utils::getConcat(r[0], children);
+ Node scn = simpleRegexpConsume(mchildren, children, dir);
+ if (!scn.isNull())
{
- success = false;
- std::vector<Node> children;
- utils::getConcat(r[0], children);
- Node scn = simpleRegexpConsume(mchildren, children, dir);
- if (!scn.isNull())
+ Trace("regexp-ext-rewrite")
+ << "Regexp star : const conflict : " << node << std::endl;
+ return returnRewrite(node, scn, Rewrite::RE_CONSUME_S_CCONF);
+ }
+ else if (children.empty())
+ {
+ // fully consumed one copy of the STAR
+ if (mchildren.empty())
{
Trace("regexp-ext-rewrite")
- << "Regexp star : const conflict : " << node << std::endl;
- return scn;
+ << "Regexp star : full consume : " << node << std::endl;
+ Node ret = NodeManager::currentNM()->mkConst(true);
+ return returnRewrite(node, ret, Rewrite::RE_CONSUME_S_FULL);
}
- else if (children.empty())
+ else
{
- // fully consumed one copy of the STAR
- if (mchildren.empty())
- {
- Trace("regexp-ext-rewrite")
- << "Regexp star : full consume : " << node << std::endl;
- return NodeManager::currentNM()->mkConst(true);
- }
- else
- {
- retNode = nm->mkNode(STRING_IN_REGEXP,
- utils::mkConcat(mchildren, stype),
- r);
- success = true;
- }
+ retNode = nm->mkNode(
+ STRING_IN_REGEXP, utils::mkConcat(mchildren, stype), r);
+ success = true;
}
}
- if (retNode != node)
- {
- Trace("regexp-ext-rewrite") << "Regexp star : rewrite " << node
- << " -> " << retNode << std::endl;
- break;
- }
+ }
+ if (retNode != node)
+ {
+ Trace("regexp-ext-rewrite") << "Regexp star : rewrite " << node
+ << " -> " << retNode << std::endl;
+ return returnRewrite(node, retNode, Rewrite::RE_CONSUME_S);
}
}
- else
- {
- std::vector<Node> children;
- utils::getConcat(r, children);
- std::vector<Node> mchildren;
- utils::getConcat(x, mchildren);
- unsigned prevSize = children.size() + mchildren.size();
- Node scn = simpleRegexpConsume(mchildren, children);
- if (!scn.isNull())
+ }
+ else
+ {
+ std::vector<Node> children;
+ utils::getConcat(r, children);
+ std::vector<Node> mchildren;
+ utils::getConcat(x, mchildren);
+ unsigned prevSize = children.size() + mchildren.size();
+ Node scn = simpleRegexpConsume(mchildren, children);
+ if (!scn.isNull())
+ {
+ Trace("regexp-ext-rewrite")
+ << "Regexp : const conflict : " << node << std::endl;
+ return returnRewrite(node, scn, Rewrite::RE_CONSUME_CCONF);
+ }
+ else if ((children.size() + mchildren.size()) != prevSize)
+ {
+ // Given a membership (str.++ x1 ... xn) in (re.++ r1 ... rm),
+ // 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(""));
+ if (children.empty())
{
- Trace("regexp-ext-rewrite")
- << "Regexp : const conflict : " << node << std::endl;
- return scn;
+ // If we stripped all components on the right, then the left is
+ // equal to the empty string.
+ // e.g. (str.++ "a" x) in (re.++ (str.to.re "a")) ---> (= x "")
+ retNode = xn.eqNode(emptyStr);
}
else
{
- if ((children.size() + mchildren.size()) != prevSize)
- {
- // Given a membership (str.++ x1 ... xn) in (re.++ r1 ... rm),
- // 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(""));
- if (children.empty())
- {
- // If we stripped all components on the right, then the left is
- // equal to the empty string.
- // e.g. (str.++ "a" x) in (re.++ (str.to.re "a")) ---> (= x "")
- retNode = xn.eqNode(emptyStr);
- }
- else
- {
- // otherwise, construct the updated regular expression
- retNode = nm->mkNode(
- STRING_IN_REGEXP, xn, utils::mkConcat(children, rtype));
- }
- Trace("regexp-ext-rewrite") << "Regexp : rewrite : " << node << " -> "
- << retNode << std::endl;
- return returnRewrite(node, retNode, Rewrite::RE_SIMPLE_CONSUME);
- }
+ // otherwise, construct the updated regular expression
+ retNode =
+ nm->mkNode(STRING_IN_REGEXP, xn, utils::mkConcat(children, rtype));
}
+ Trace("regexp-ext-rewrite")
+ << "Regexp : rewrite : " << node << " -> " << retNode << std::endl;
+ return returnRewrite(node, retNode, Rewrite::RE_SIMPLE_CONSUME);
}
}
- return retNode;
+ return node;
}
RewriteResponse SequencesRewriter::postRewrite(TNode node)
{
Trace("strings-postrewrite")
<< "Strings::postRewrite start " << node << std::endl;
- NodeManager* nm = NodeManager::currentNM();
Node retNode = node;
- Node orig = retNode;
Kind nk = node.getKind();
if (nk == kind::STRING_CONCAT)
{
}
else if (nk == kind::STRING_LENGTH)
{
- Kind nk0 = node[0].getKind();
- if (node[0].isConst())
- {
- retNode = nm->mkConst(Rational(Word::getLength(node[0])));
- }
- else if (nk0 == kind::STRING_CONCAT)
- {
- Node tmpNode = node[0];
- if (tmpNode.isConst())
- {
- retNode = nm->mkConst(Rational(Word::getLength(tmpNode)));
- }
- else if (tmpNode.getKind() == kind::STRING_CONCAT)
- {
- std::vector<Node> node_vec;
- for (unsigned int i = 0; i < tmpNode.getNumChildren(); ++i)
- {
- if (tmpNode[i].isConst())
- {
- node_vec.push_back(
- nm->mkConst(Rational(Word::getLength(tmpNode[i]))));
- }
- else
- {
- node_vec.push_back(NodeManager::currentNM()->mkNode(
- kind::STRING_LENGTH, tmpNode[i]));
- }
- }
- retNode = NodeManager::currentNM()->mkNode(kind::PLUS, node_vec);
- }
- }
- else if (nk0 == STRING_STRREPL || nk0 == STRING_STRREPLALL)
- {
- Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1]));
- Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2]));
- if (len1 == len2)
- {
- // len( y ) == len( z ) => len( str.replace( x, y, z ) ) ---> len( x )
- retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
- }
- }
- else if (nk0 == STRING_TOLOWER || nk0 == STRING_TOUPPER
- || nk0 == STRING_REV)
- {
- // len( f( x ) ) == len( x ) where f is tolower, toupper, or rev.
- retNode = nm->mkNode(STRING_LENGTH, node[0][0]);
- }
+ retNode = rewriteLength(node);
}
else if (nk == kind::STRING_CHARAT)
{
- Node one = NodeManager::currentNM()->mkConst(Rational(1));
- retNode = NodeManager::currentNM()->mkNode(
- kind::STRING_SUBSTR, node[0], node[1], one);
+ retNode = rewriteCharAt(node);
}
else if (nk == kind::STRING_SUBSTR)
{
}
else if (nk == kind::STRING_LT)
{
- // eliminate s < t ---> s != t AND s <= t
- retNode = nm->mkNode(AND,
- node[0].eqNode(node[1]).negate(),
- nm->mkNode(STRING_LEQ, node[0], node[1]));
+ retNode = StringsRewriter::rewriteStringLt(node);
}
else if (nk == kind::STRING_LEQ)
{
}
else if (nk == STRING_IS_DIGIT)
{
- // eliminate str.is_digit(s) ----> 48 <= str.to_code(s) <= 57
- Node t = nm->mkNode(STRING_TO_CODE, node[0]);
- retNode = nm->mkNode(AND,
- nm->mkNode(LEQ, nm->mkConst(Rational(48)), t),
- nm->mkNode(LEQ, t, nm->mkConst(Rational(57))));
+ retNode = StringsRewriter::rewriteStringIsDigit(node);
}
else if (nk == kind::STRING_ITOS)
{
}
else if (nk == REGEXP_DIFF)
{
- retNode = nm->mkNode(
- REGEXP_INTER, node[0], nm->mkNode(REGEXP_COMPLEMENT, node[1]));
+ retNode = rewriteDifferenceRegExp(node);
}
else if (nk == REGEXP_STAR)
{
}
else if (nk == REGEXP_PLUS)
{
- retNode =
- nm->mkNode(REGEXP_CONCAT, node[0], nm->mkNode(REGEXP_STAR, node[0]));
+ retNode = rewritePlusRegExp(node);
}
else if (nk == REGEXP_OPT)
{
- retNode = nm->mkNode(REGEXP_UNION,
- nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String(""))),
- node[0]);
+ retNode = rewriteOptionRegExp(node);
}
else if (nk == REGEXP_RANGE)
{
- if (node[0] == node[1])
- {
- retNode = nm->mkNode(STRING_TO_REGEXP, node[0]);
- }
+ retNode = rewriteRangeRegExp(node);
}
else if (nk == REGEXP_LOOP)
{
}
else if (nk == REGEXP_REPEAT)
{
- // ((_ re.^ n) R) --> ((_ re.loop n n) R)
- unsigned r = utils::getRepeatAmount(node);
- Node lop = nm->mkConst(RegExpLoop(r, r));
- retNode = nm->mkNode(REGEXP_LOOP, lop, node[0]);
+ retNode = rewriteRepeatRegExp(node);
}
Trace("strings-postrewrite")
<< "Strings::postRewrite returning " << retNode << std::endl;
- if (orig != retNode)
+ if (node != retNode)
{
Trace("strings-rewrite-debug")
- << "Strings: post-rewrite " << orig << " to " << retNode << std::endl;
+ << "Strings: post-rewrite " << node << " to " << retNode << std::endl;
+ return RewriteResponse(REWRITE_AGAIN_FULL, retNode);
}
- return RewriteResponse(orig == retNode ? REWRITE_DONE : REWRITE_AGAIN_FULL,
- retNode);
+ return RewriteResponse(REWRITE_DONE, retNode);
}
bool SequencesRewriter::hasEpsilonNode(TNode node)
return RewriteResponse(REWRITE_DONE, node);
}
+Node SequencesRewriter::rewriteCharAt(Node node)
+{
+ Assert(node.getKind() == STRING_CHARAT);
+ NodeManager* nm = NodeManager::currentNM();
+ Node one = nm->mkConst(Rational(1));
+ Node retNode = nm->mkNode(STRING_SUBSTR, node[0], node[1], one);
+ return returnRewrite(node, retNode, Rewrite::CHARAT_ELIM);
+}
+
Node SequencesRewriter::rewriteSubstr(Node node)
{
Assert(node.getKind() == kind::STRING_SUBSTR);
Node retNode = n[0].eqNode(
NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, n[1], val, lens));
- return retNode;
+ return returnRewrite(n, retNode, Rewrite::SUF_PREFIX_ELIM);
}
Node SequencesRewriter::splitConstant(Node a, Node b, int& index, bool isRev)
projects / cvc5.git / commitdiff