{
if (!ctn.getConst<bool>())
{
- return returnRewrite(node, ctn, "eq-nctn");
+ return returnRewrite(node, ctn, Rewrite::EQ_NCTN);
}
else
{
len_eq = Rewriter::rewrite(len_eq);
if (len_eq.isConst() && !len_eq.getConst<bool>())
{
- return returnRewrite(node, len_eq, "eq-len-deq");
+ return returnRewrite(node, len_eq, Rewrite::EQ_LEN_DEQ);
}
std::vector<Node> c[2];
if (!isSameFix)
{
Node ret = NodeManager::currentNM()->mkConst(false);
- return returnRewrite(node, ret, "eq-nfix");
+ return returnRewrite(node, ret, Rewrite::EQ_NFIX);
}
}
if (c[0][index1] != c[1][index2])
Node s1 = utils::mkConcat(c[0], stype);
Node s2 = utils::mkConcat(c[1], stype);
new_ret = s1.eqNode(s2);
- node = returnRewrite(node, new_ret, "str-eq-unify");
+ node = returnRewrite(node, new_ret, Rewrite::STR_EQ_UNIFY);
}
// ------- homogeneous constants
// this conflict just in case.
new_ret = nm->mkConst(false);
return returnRewrite(
- node, new_ret, "string-eq-const-conflict-non-homog");
+ node, new_ret, Rewrite::STR_EQ_CONST_NHOMOG);
}
numHChars[j]++;
}
// "AA" = y ++ x ---> "AA" = x ++ y if x < y
// "AAA" = y ++ "A" ++ z ---> "AA" = y ++ z
new_ret = lhs.eqNode(ss);
- node = returnRewrite(node, new_ret, "str-eq-homog-const");
+ node = returnRewrite(node, new_ret, Rewrite::STR_EQ_HOMOG_CONST);
}
}
}
if (ne[0] == ne[2])
{
Node ret = nm->mkNode(EQUAL, ne[0], empty);
- return returnRewrite(node, ret, "str-emp-repl-x-y-x");
+ return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_X_Y_X);
}
// (= "" (str.replace x y "A")) ---> (and (= x "") (not (= y "")))
nm->mkNode(AND,
nm->mkNode(EQUAL, ne[0], empty),
nm->mkNode(NOT, nm->mkNode(EQUAL, ne[1], empty)));
- return returnRewrite(node, ret, "str-emp-repl-emp");
+ return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
}
// (= "" (str.replace x "A" "")) ---> (str.prefix x "A")
if (checkEntailLengthOne(ne[1]) && ne[2] == empty)
{
Node ret = nm->mkNode(STRING_PREFIX, ne[0], ne[1]);
- return returnRewrite(node, ret, "str-emp-repl-emp");
+ return returnRewrite(node, ret, Rewrite::STR_EMP_REPL_EMP);
}
}
else if (ne.getKind() == STRING_SUBSTR)
if (ne[1] == zero)
{
Node ret = nm->mkNode(EQUAL, ne[0], empty);
- return returnRewrite(node, ret, "str-emp-substr-leq-len");
+ return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_LEN);
}
// (= "" (str.substr x n m)) ---> (<= (str.len x) n)
// if n >= 0 and m > 0
Node ret = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, ne[0]), ne[1]);
- return returnRewrite(node, ret, "str-emp-substr-leq-len");
+ return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_LEN);
}
// (= "" (str.substr "A" 0 z)) ---> (<= z 0)
if (checkEntailNonEmpty(ne[0]) && ne[1] == zero)
{
Node ret = nm->mkNode(LEQ, ne[2], zero);
- return returnRewrite(node, ret, "str-emp-substr-leq-z");
+ return returnRewrite(node, ret, Rewrite::STR_EMP_SUBSTR_LEQ_Z);
}
}
}
{
Node ret = nm->mkNode(
EQUAL, empty, nm->mkNode(STRING_STRREPL, x, repl[2], repl[1]));
- return returnRewrite(node, ret, "str-eq-repl-emp");
+ return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_EMP);
}
// (= x (str.replace y x y)) ---> (= x y)
if (repl[0] == repl[2] && x == repl[1])
{
Node ret = nm->mkNode(EQUAL, x, repl[0]);
- return returnRewrite(node, ret, "str-eq-repl-to-eq");
+ return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_TO_EQ);
}
// (= x (str.replace x "A" "B")) ---> (not (str.contains x "A"))
if (eq.isConst() && !eq.getConst<bool>())
{
Node ret = nm->mkNode(NOT, nm->mkNode(STRING_STRCTN, x, repl[1]));
- return returnRewrite(node, ret, "str-eq-repl-not-ctn");
+ return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_NOT_CTN);
}
}
Node ret = nm->mkNode(OR,
nm->mkNode(EQUAL, repl[0], repl[1]),
nm->mkNode(EQUAL, repl[0], repl[2]));
- return returnRewrite(node, ret, "str-eq-repl-to-dis");
+ return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_TO_DIS);
}
}
}
new_ret = inferEqsFromContains(node[i], node[1 - i]);
if (!new_ret.isNull())
{
- return returnRewrite(node, new_ret, "str-eq-conj-len-entail");
+ return returnRewrite(node, new_ret, Rewrite::STR_EQ_CONJ_LEN_ENTAIL);
}
}
}
pfx0.eqNode(pfx1),
utils::mkConcat(sfxv0, stype)
.eqNode(utils::mkConcat(sfxv1, stype)));
- return returnRewrite(node, ret, "split-eq");
+ return returnRewrite(node, ret, Rewrite::SPLIT_EQ);
}
else if (checkEntailArith(lenPfx1, lenPfx0, true))
{
pfx0.eqNode(utils::mkConcat(rpfxv1, stype)),
utils::mkConcat(sfxv0, stype)
.eqNode(utils::mkConcat(pfxv1, stype)));
- return returnRewrite(node, ret, "split-eq-strip-r");
+ return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_R);
}
// If the prefix of the right-hand side is (strictly) longer than
utils::mkConcat(rpfxv0, stype).eqNode(pfx1),
utils::mkConcat(pfxv0, stype)
.eqNode(utils::mkConcat(sfxv1, stype)));
- return returnRewrite(node, ret, "split-eq-strip-l");
+ return returnRewrite(node, ret, Rewrite::SPLIT_EQ_STRIP_L);
}
// If the prefix of the left-hand side is (strictly) longer than
{
retNode = vec.size() == 1 ? vec[0] : nm->mkNode(REGEXP_CONCAT, vec);
}
- return returnRewrite(node, retNode, "re.concat-flatten");
+ return returnRewrite(node, retNode, Rewrite::RE_CONCAT_FLATTEN);
}
Trace("strings-rewrite-debug")
<< "Strings::rewriteConcatRegExp start " << node << std::endl;
{
// handles all cases where consecutive re constants are combined or
// dropped as described in the loop above.
- return returnRewrite(node, retNode, "re.concat");
+ return returnRewrite(node, retNode, Rewrite::RE_CONCAT);
}
// flipping adjacent star arguments
if (changed)
{
retNode = utils::mkConcat(cvec, rtype);
- return returnRewrite(node, retNode, "re.concat.opt");
+ return returnRewrite(node, retNode, Rewrite::RE_CONCAT_OPT);
}
return node;
}
if (node[0].getKind() == REGEXP_STAR)
{
// ((R)*)* ---> R*
- return returnRewrite(node, node[0], "re-star-nested-star");
+ return returnRewrite(node, node[0], Rewrite::RE_STAR_NESTED_STAR);
}
else if (node[0].getKind() == STRING_TO_REGEXP && node[0][0].isConst()
&& Word::isEmpty(node[0][0]))
{
// ("")* ---> ""
- return returnRewrite(node, node[0], "re-star-empty-string");
+ return returnRewrite(node, node[0], Rewrite::RE_STAR_EMPTY_STRING);
}
else if (node[0].getKind() == REGEXP_EMPTY)
{
// (empty)* ---> ""
retNode = nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")));
- return returnRewrite(node, retNode, "re-star-empty");
+ return returnRewrite(node, retNode, Rewrite::RE_STAR_EMPTY);
}
else if (node[0].getKind() == REGEXP_UNION)
{
retNode = nm->mkNode(REGEXP_STAR, retNode);
// simplification of union beneath star based on loop above
// for example, ( "" | "a" )* ---> ("a")*
- return returnRewrite(node, retNode, "re-star-union");
+ return returnRewrite(node, retNode, Rewrite::RE_STAR_UNION);
}
}
}
{
if (nk == REGEXP_INTER)
{
- return returnRewrite(node, ni, "re.and-empty");
+ return returnRewrite(node, ni, Rewrite::RE_AND_EMPTY);
}
// otherwise, can ignore
}
{
if (nk == REGEXP_UNION)
{
- return returnRewrite(node, ni, "re.or-all");
+ return returnRewrite(node, ni, Rewrite::RE_OR_ALL);
}
// otherwise, can ignore
}
if (retNode != node)
{
// flattening and removing children, based on loop above
- return returnRewrite(node, retNode, "re.andor-flatten");
+ return returnRewrite(node, retNode, Rewrite::RE_ANDOR_FLATTEN);
}
return node;
}
Node r = node[0];
if (r.getKind() == REGEXP_STAR)
{
- return returnRewrite(node, r, "re.loop-star");
+ return returnRewrite(node, r, Rewrite::RE_LOOP_STAR);
}
TNode n1 = node[1];
NodeManager* nm = NodeManager::currentNM();
<< std::endl;
if (retNode != node)
{
- return returnRewrite(node, retNode, "re.loop");
+ return returnRewrite(node, retNode, Rewrite::RE_LOOP);
}
return node;
}
{
retNode = nm->mkConst(true);
// e.g. (str.in.re "" (re.* (str.to.re x))) ----> true
- return returnRewrite(node, retNode, "re-empty-in-str-star");
+ return returnRewrite(node, retNode, Rewrite::RE_EMPTY_IN_STR_STAR);
}
else if (s.size() == 1)
{
{
retNode = r[0][0].eqNode(x);
// e.g. (str.in.re "A" (re.* (str.to.re x))) ----> "A" = x
- return returnRewrite(node, retNode, "re-char-in-str-star");
+ return returnRewrite(node, retNode, Rewrite::RE_CHAR_IN_STR_STAR);
}
}
}
nb << nm->mkNode(STRING_IN_REGEXP, xc, r);
}
return returnRewrite(
- node, nb.constructNode(), "re-in-dist-char-star");
+ node, nb.constructNode(), Rewrite::RE_IN_DIST_CHAR_STAR);
}
}
}
if (r[0].getKind() == kind::REGEXP_SIGMA)
{
retNode = NodeManager::currentNM()->mkConst(true);
- return returnRewrite(node, retNode, "re-in-sigma-star");
+ return returnRewrite(node, retNode, Rewrite::RE_IN_SIGMA_STAR);
}
}
else if (r.getKind() == kind::REGEXP_CONCAT)
Node num = nm->mkConst(Rational(allSigmaMinSize));
Node lenx = nm->mkNode(STRING_LENGTH, x);
retNode = nm->mkNode(allSigmaStrict ? EQUAL : GEQ, lenx, num);
- return returnRewrite(node, retNode, "re-concat-pure-allchar");
+ 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);
- return returnRewrite(node, retNode, "re-concat-to-contains");
+ return returnRewrite(node, retNode, Rewrite::RE_CONCAT_TO_CONTAINS);
}
}
}
}
Trace("regexp-ext-rewrite") << "Regexp : rewrite : " << node << " -> "
<< retNode << std::endl;
- return returnRewrite(node, retNode, "re-simple-consume");
+ return returnRewrite(node, retNode, Rewrite::RE_SIMPLE_CONSUME);
}
}
}
if (Word::isEmpty(node[0]))
{
Node ret = node[0];
- return returnRewrite(node, ret, "ss-emptystr");
+ return returnRewrite(node, ret, Rewrite::SS_EMPTYSTR);
}
// rewriting for constant arguments
if (node[1].isConst() && node[2].isConst())
// start beyond the maximum size of strings
// thus, it must be beyond the end point of this string
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-const-start-max-oob");
+ return returnRewrite(node, ret, Rewrite::SS_CONST_START_MAX_OOB);
}
else if (node[1].getConst<Rational>().sgn() < 0)
{
// start before the beginning of the string
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-const-start-neg");
+ return returnRewrite(node, ret, Rewrite::SS_CONST_START_NEG);
}
else
{
{
// start beyond the end of the string
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-const-start-oob");
+ return returnRewrite(node, ret, Rewrite::SS_CONST_START_OOB);
}
}
if (node[2].getConst<Rational>() > rMaxInt)
// take up to the end of the string
size_t lenS = Word::getLength(s);
Node ret = Word::suffix(s, lenS - start);
- return returnRewrite(node, ret, "ss-const-len-max-oob");
+ return returnRewrite(node, ret, Rewrite::SS_CONST_LEN_MAX_OOB);
}
else if (node[2].getConst<Rational>().sgn() <= 0)
{
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-const-len-non-pos");
+ return returnRewrite(node, ret, Rewrite::SS_CONST_LEN_NON_POS);
}
else
{
// take up to the end of the string
size_t lenS = Word::getLength(s);
Node ret = Word::suffix(s, lenS - start);
- return returnRewrite(node, ret, "ss-const-end-oob");
+ return returnRewrite(node, ret, Rewrite::SS_CONST_END_OOB);
}
else
{
// compute the substr using the constant string
Node ret = Word::substr(s, start, len);
- return returnRewrite(node, ret, "ss-const-ss");
+ return returnRewrite(node, ret, Rewrite::SS_CONST_SS);
}
}
}
if (checkEntailArith(zero, node[1], true))
{
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-start-neg");
+ return returnRewrite(node, ret, Rewrite::SS_START_NEG);
}
else if (checkEntailArith(zero, node[2]))
{
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-len-non-pos");
+ return returnRewrite(node, ret, Rewrite::SS_LEN_NON_POS);
}
if (node[0].getKind() == STRING_SUBSTR)
if (checkEntailArith(node[1], node[0][2]))
{
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-start-geq-len");
+ return returnRewrite(node, ret, Rewrite::SS_START_GEQ_LEN);
}
}
else if (node[0].getKind() == STRING_STRREPL)
nm->mkNode(kind::STRING_SUBSTR, node[0][0], node[1], node[2]),
node[0][1],
node[0][2]);
- return returnRewrite(node, ret, "substr-repl-swap");
+ return returnRewrite(node, ret, Rewrite::SUBSTR_REPL_SWAP);
}
}
}
kind::STRING_SUBSTR, utils::mkConcat(n1, stype), node[1], curr));
}
Node ret = utils::mkConcat(childrenr, stype);
- return returnRewrite(node, ret, "ss-len-include");
+ return returnRewrite(node, ret, Rewrite::SS_LEN_INCLUDE);
}
}
{
// end point beyond end point of string, map to tot_len
Node ret = nm->mkNode(kind::STRING_SUBSTR, node[0], node[1], tot_len);
- return returnRewrite(node, ret, "ss-end-pt-norm");
+ return returnRewrite(node, ret, Rewrite::SS_END_PT_NORM);
}
else
{
if (checkEntailArithWithAssumption(n1_lt_tot_len, zero, node[2], false))
{
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-start-entails-zero-len");
+ return returnRewrite(node, ret, Rewrite::SS_START_ENTAILS_ZERO_LEN);
}
// (str.substr s x y) --> "" if 0 < y |= x >= str.len(s)
if (checkEntailArithWithAssumption(non_zero_len, node[1], tot_len, false))
{
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-non-zero-len-entails-oob");
+ return returnRewrite(node, ret, Rewrite::SS_NON_ZERO_LEN_ENTAILS_OOB);
}
// (str.substr s x y) --> "" if x >= 0 |= 0 >= str.len(s)
if (checkEntailArithWithAssumption(geq_zero_start, zero, tot_len, false))
{
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-geq-zero-start-entails-emp-s");
+ return returnRewrite(
+ node, ret, Rewrite::SS_GEQ_ZERO_START_ENTAILS_EMP_S);
}
// (str.substr s x x) ---> "" if (str.len s) <= 1
if (node[1] == node[2] && checkEntailLengthOne(node[0]))
{
Node ret = Word::mkEmptyWord(node.getType());
- return returnRewrite(node, ret, "ss-len-one-z-z");
+ return returnRewrite(node, ret, Rewrite::SS_LEN_ONE_Z_Z);
}
}
if (!curr.isNull())
{
Node ret = nm->mkNode(
kind::STRING_SUBSTR, utils::mkConcat(n1, stype), curr, node[2]);
- return returnRewrite(node, ret, "ss-strip-start-pt");
+ return returnRewrite(node, ret, Rewrite::SS_STRIP_START_PT);
}
else
{
utils::mkConcat(n1, stype),
node[1],
node[2]);
- return returnRewrite(node, ret, "ss-strip-end-pt");
+ return returnRewrite(node, ret, Rewrite::SS_STRIP_END_PT);
}
}
}
Node new_start = nm->mkNode(kind::PLUS, start_inner, start_outer);
Node ret =
nm->mkNode(kind::STRING_SUBSTR, node[0][0], new_start, new_len);
- return returnRewrite(node, ret, "ss-combine");
+ return returnRewrite(node, ret, Rewrite::SS_COMBINE);
}
}
}
if (node[0] == node[1])
{
Node ret = NodeManager::currentNM()->mkConst(true);
- return returnRewrite(node, ret, "ctn-eq");
+ return returnRewrite(node, ret, Rewrite::CTN_EQ);
}
if (node[0].isConst())
{
if (node[1].isConst())
{
Node ret = nm->mkConst(Word::find(node[0], node[1]) != std::string::npos);
- return returnRewrite(node, ret, "ctn-const");
+ return returnRewrite(node, ret, Rewrite::CTN_CONST);
}
else
{
// uses this function, hence we want to conclude false if possible.
// len(x)>0 => contains( "", x ) ---> false
Node ret = NodeManager::currentNM()->mkConst(false);
- return returnRewrite(node, ret, "ctn-lhs-emptystr");
+ return returnRewrite(node, ret, Rewrite::CTN_LHS_EMPTYSTR);
}
}
else if (checkEntailLengthOne(t))
// t = "" v t = "A" v t = "B" v t = "C" v t = "a" v t = "b" v t = "c"
// if len(t) <= 1
Node ret = nb;
- return returnRewrite(node, ret, "ctn-split");
+ return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
}
else if (node[1].getKind() == kind::STRING_CONCAT)
{
if (!canConstantContainConcat(node[0], node[1], firstc, lastc))
{
Node ret = NodeManager::currentNM()->mkConst(false);
- return returnRewrite(node, ret, "ctn-nconst-ctn-concat");
+ return returnRewrite(node, ret, Rewrite::CTN_NCONST_CTN_CONCAT);
}
}
}
{
// contains( x, "" ) ---> true
Node ret = NodeManager::currentNM()->mkConst(true);
- return returnRewrite(node, ret, "ctn-rhs-emptystr");
+ return returnRewrite(node, ret, Rewrite::CTN_RHS_EMPTYSTR);
}
else if (len == 1)
{
Node ret = nb.constructNode();
// str.contains( x ++ y, "A" ) --->
// str.contains( x, "A" ) OR str.contains( y, "A" )
- return returnRewrite(node, ret, "ctn-concat-char");
+ return returnRewrite(node, ret, Rewrite::CTN_CONCAT_CHAR);
}
else if (node[0].getKind() == STRING_STRREPL)
{
// str.contains( str.replace( x, y, z ), "A" ) --->
// str.contains( x, "A" ) OR
// ( str.contains( x, y ) AND str.contains( z, "A" ) )
- return returnRewrite(node, ret, "ctn-repl-char");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL_CHAR);
}
}
}
if (componentContains(nc1, nc2, nc1rb, nc1re) != -1)
{
Node ret = NodeManager::currentNM()->mkConst(true);
- return returnRewrite(node, ret, "ctn-component");
+ return returnRewrite(node, ret, Rewrite::CTN_COMPONENT);
}
TypeNode stype = node[0].getType();
{
Node ret = NodeManager::currentNM()->mkNode(
kind::STRING_STRCTN, utils::mkConcat(nc1, stype), node[1]);
- return returnRewrite(node, ret, "ctn-strip-endpt");
+ return returnRewrite(node, ret, Rewrite::CTN_STRIP_ENDPT);
}
for (const Node& n : nc2)
if (!ctnConst2.isNull() && !ctnConst2.getConst<bool>())
{
Node res = nm->mkConst(false);
- return returnRewrite(node, res, "ctn-rpl-non-ctn");
+ return returnRewrite(node, res, Rewrite::CTN_RPL_NON_CTN);
}
}
{
ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
}
- return returnRewrite(node, ret, "ctn-repl-self");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL_SELF);
}
}
}
{
// len( n2 ) > len( n1 ) => contains( n1, n2 ) ---> false
Node ret = NodeManager::currentNM()->mkConst(false);
- return returnRewrite(node, ret, "ctn-len-ineq");
+ return returnRewrite(node, ret, Rewrite::CTN_LEN_INEQ);
}
// multi-set reasoning
if (checkEntailMultisetSubset(node[0], node[1]))
{
Node ret = nm->mkConst(false);
- return returnRewrite(node, ret, "ctn-mset-nss");
+ return returnRewrite(node, ret, Rewrite::CTN_MSET_NSS);
}
if (checkEntailArith(len_n2, len_n1, false))
{
// len( n2 ) >= len( n1 ) => contains( n1, n2 ) ---> n1 = n2
Node ret = node[0].eqNode(node[1]);
- return returnRewrite(node, ret, "ctn-len-ineq-nstrict");
+ return returnRewrite(node, ret, Rewrite::CTN_LEN_INEQ_NSTRICT);
}
// splitting
NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
utils::mkConcat(spl[1], stype),
node[1]));
- return returnRewrite(node, ret, "ctn-split");
+ return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
}
}
}
if (node[0][2] == nm->mkNode(kind::STRING_LENGTH, node[1]))
{
Node ret = nm->mkNode(kind::EQUAL, node[0], node[1]);
- return returnRewrite(node, ret, "ctn-substr");
+ return returnRewrite(node, ret, Rewrite::CTN_SUBSTR);
}
}
else if (node[0].getKind() == kind::STRING_STRREPL)
// (str.contains (str.replace x c1 c2) c3) ---> (str.contains x c3)
// if there is no overlap between c1 and c3 and none between c2 and c3
Node ret = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
- return returnRewrite(node, ret, "ctn-repl-cnsts-to-ctn");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL_CNSTS_TO_CTN);
}
}
if (node[0][1] == node[1])
{
Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
- return returnRewrite(node, ret, "ctn-repl-to-ctn");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN);
}
// (str.contains (str.replace x y x) z) ---> (str.contains x z)
if (checkEntailLengthOne(node[1]))
{
Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
- return returnRewrite(node, ret, "ctn-repl-len-one-to-ctn");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL_LEN_ONE_TO_CTN);
}
}
Node ret = nm->mkNode(OR,
nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]),
nm->mkNode(STRING_STRCTN, node[0][0], node[0][2]));
- return returnRewrite(node, ret, "ctn-repl-to-ctn-disj");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN_DISJ);
}
// (str.contains (str.replace x y z) w) --->
kind::STRING_STRCTN,
nm->mkNode(kind::STRING_STRREPL, node[0][0], node[0][1], empty),
node[1]);
- return returnRewrite(node, ret, "ctn-repl-simp-repl");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL_SIMP_REPL);
}
}
}
if (node[0] == node[1][1] && node[1][0] == node[1][2])
{
Node ret = nm->mkNode(kind::STRING_STRCTN, node[0], node[1][0]);
- return returnRewrite(node, ret, "ctn-repl");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL);
}
// (str.contains x (str.replace "" x y)) --->
if (node[0] == node[1][1] && node[1][0] == emp)
{
Node ret = nm->mkNode(kind::EQUAL, emp, node[1]);
- return returnRewrite(node, ret, "ctn-repl-empty");
+ return returnRewrite(node, ret, Rewrite::CTN_REPL_EMPTY);
}
}
{
// z<0 implies str.indexof( x, y, z ) --> -1
Node negone = nm->mkConst(Rational(-1));
- return returnRewrite(node, negone, "idof-neg");
+ return returnRewrite(node, negone, Rewrite::IDOF_NEG);
}
// the string type
// in our implementation, that accessing a position greater than
// rMaxInt is guaranteed to be out of bounds.
Node negone = nm->mkConst(Rational(-1));
- return returnRewrite(node, negone, "idof-max");
+ return returnRewrite(node, negone, Rewrite::IDOF_MAX);
}
Assert(node[2].getConst<Rational>().sgn() >= 0);
Node s = children0[0];
if (ret != std::string::npos)
{
Node retv = nm->mkConst(Rational(static_cast<unsigned>(ret)));
- return returnRewrite(node, retv, "idof-find");
+ return returnRewrite(node, retv, Rewrite::IDOF_FIND);
}
else if (children0.size() == 1)
{
Node negone = nm->mkConst(Rational(-1));
- return returnRewrite(node, negone, "idof-nfind");
+ return returnRewrite(node, negone, Rewrite::IDOF_NFIND);
}
}
{
// indexof( x, x, 0 ) --> 0
Node zero = nm->mkConst(Rational(0));
- return returnRewrite(node, zero, "idof-eq-cst-start");
+ return returnRewrite(node, zero, Rewrite::IDOF_EQ_CST_START);
}
}
if (checkEntailArith(node[2], true))
{
// y>0 implies indexof( x, x, y ) --> -1
Node negone = nm->mkConst(Rational(-1));
- return returnRewrite(node, negone, "idof-eq-nstart");
+ return returnRewrite(node, negone, Rewrite::IDOF_EQ_NSTART);
}
Node emp = nm->mkConst(CVC4::String(""));
if (node[0] != emp)
{
// indexof( x, x, z ) ---> indexof( "", "", z )
Node ret = nm->mkNode(STRING_STRIDOF, emp, emp, node[2]);
- return returnRewrite(node, ret, "idof-eq-norm");
+ return returnRewrite(node, ret, Rewrite::IDOF_EQ_NORM);
}
}
if (checkEntailArith(len0, node[2]) && checkEntailArith(node[2]))
{
// len(x)>=z ^ z >=0 implies indexof( x, "", z ) ---> z
- return returnRewrite(node, node[2], "idof-emp-idof");
+ return returnRewrite(node, node[2], Rewrite::IDOF_EMP_IDOF);
}
}
}
{
// len(x)-z < len(y) implies indexof( x, y, z ) ----> -1
Node negone = nm->mkConst(Rational(-1));
- return returnRewrite(node, negone, "idof-len");
+ return returnRewrite(node, negone, Rewrite::IDOF_LEN);
}
Node fstr = node[0];
// str.indexof(str.++(x,y,z),y,0) ---> str.indexof(str.++(x,y),y,0)
Node nn = utils::mkConcat(children0, stype);
Node ret = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
- return returnRewrite(node, ret, "idof-def-ctn");
+ return returnRewrite(node, ret, Rewrite::IDOF_DEF_CTN);
}
// Strip components from the beginning that are guaranteed not to match
utils::mkConcat(children0, stype),
node[1],
node[2]));
- return returnRewrite(node, ret, "idof-strip-cnst-endpts");
+ return returnRewrite(node, ret, Rewrite::IDOF_STRIP_CNST_ENDPTS);
}
}
nm->mkNode(kind::PLUS,
nm->mkNode(kind::MINUS, node[2], new_len),
nm->mkNode(kind::STRING_STRIDOF, nn, node[1], new_len));
- return returnRewrite(node, ret, "idof-strip-sym-len");
+ return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
}
}
else
{
// str.contains( x, y ) --> false implies str.indexof(x,y,z) --> -1
Node negone = nm->mkConst(Rational(-1));
- return returnRewrite(node, negone, "idof-nctn");
+ return returnRewrite(node, negone, Rewrite::IDOF_NCTN);
}
}
else
children.insert(children.end(), children0.begin(), children0.end());
Node nn = utils::mkConcat(children, stype);
Node res = nm->mkNode(kind::STRING_STRIDOF, nn, node[1], node[2]);
- return returnRewrite(node, res, "idof-norm-prefix");
+ return returnRewrite(node, res, Rewrite::IDOF_NORM_PREFIX);
}
}
}
ret = nm->mkNode(STRING_STRIDOF, ret, node[1], node[2]);
// For example:
// str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 )
- return returnRewrite(node, ret, "rpl-pull-endpt");
+ return returnRewrite(node, ret, Rewrite::RPL_PULL_ENDPT);
}
}
if (node[1].isConst() && Word::isEmpty(node[1]))
{
Node ret = nm->mkNode(STRING_CONCAT, node[2], node[0]);
- return returnRewrite(node, ret, "rpl-rpl-empty");
+ return returnRewrite(node, ret, Rewrite::RPL_RPL_EMPTY);
}
// the string type
TypeNode stype = node.getType();
{
if (children0.size() == 1)
{
- return returnRewrite(node, node[0], "rpl-const-nfind");
+ return returnRewrite(node, node[0], Rewrite::RPL_CONST_NFIND);
}
}
else
}
children.insert(children.end(), children0.begin() + 1, children0.end());
Node ret = utils::mkConcat(children, stype);
- return returnRewrite(node, ret, "rpl-const-find");
+ return returnRewrite(node, ret, Rewrite::RPL_CONST_FIND);
}
}
Node l1 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, node[1]);
if (checkEntailArith(l1, l0))
{
- return returnRewrite(node, node[0], "rpl-rpl-len-id");
+ return returnRewrite(node, node[0], Rewrite::RPL_RPL_LEN_ID);
}
// (str.replace x y x) ---> (str.replace x (str.++ y1 ... yn) x)
if (node[1] != nn1)
{
Node ret = nm->mkNode(STRING_STRREPL, node[0], nn1, node[2]);
- return returnRewrite(node, ret, "rpl-x-y-x-simp");
+ return returnRewrite(node, ret, Rewrite::RPL_X_Y_X_SIMP);
}
}
}
cres.push_back(node[2]);
cres.insert(cres.end(), ce.begin(), ce.end());
Node ret = utils::mkConcat(cres, stype);
- return returnRewrite(node, ret, "rpl-cctn-rpl");
+ return returnRewrite(node, ret, Rewrite::RPL_CCTN_RPL);
}
else if (!ce.empty())
{
node[2]));
scc.insert(scc.end(), ce.begin(), ce.end());
Node ret = utils::mkConcat(scc, stype);
- return returnRewrite(node, ret, "rpl-cctn");
+ return returnRewrite(node, ret, Rewrite::RPL_CCTN);
}
}
}
else
{
// ~contains( t, s ) => ( replace( t, s, r ) ----> t )
- return returnRewrite(node, node[0], "rpl-nctn");
+ return returnRewrite(node, node[0], Rewrite::RPL_NCTN);
}
}
else if (cmp_conr.getKind() == kind::EQUAL || cmp_conr.getKind() == kind::AND)
if (nn1 != node[1] || nn2 != node[2])
{
Node res = nm->mkNode(kind::STRING_STRREPL, node[0], nn1, nn2);
- return returnRewrite(node, res, "rpl-emp-cnts-substs");
+ return returnRewrite(node, res, Rewrite::RPL_EMP_CNTS_SUBSTS);
}
}
if (nn2 != node[2])
{
Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1], nn2);
- return returnRewrite(node, res, "rpl-cnts-substs");
+ return returnRewrite(node, res, Rewrite::RPL_CNTS_SUBSTS);
}
}
}
node[2]));
cc.insert(cc.end(), ce.begin(), ce.end());
Node ret = utils::mkConcat(cc, stype);
- return returnRewrite(node, ret, "rpl-pull-endpt");
+ return returnRewrite(node, ret, Rewrite::RPL_PULL_ENDPT);
}
}
}
node[0],
utils::mkConcat(children1, stype),
node[2]);
- return returnRewrite(node, res, "repl-subst-idx");
+ return returnRewrite(node, res, Rewrite::REPL_SUBST_IDX);
}
}
nm->mkNode(kind::STRING_STRREPL, y, w, z),
y,
z);
- return returnRewrite(node, ret, "repl-repl-short-circuit");
+ return returnRewrite(node, ret, Rewrite::REPL_REPL_SHORT_CIRCUIT);
}
}
}
if (node[1][0] == node[1][2] && node[1][0] == node[2])
{
// str.replace( x, str.replace( x, y, x ), x ) ---> x
- return returnRewrite(node, node[0], "repl-repl2-inv-id");
+ return returnRewrite(node, node[0], Rewrite::REPL_REPL2_INV_ID);
}
bool dualReplIteSuccess = false;
Node cmp_con2 = checkEntailContains(node[1][0], node[1][2]);
nm->mkNode(STRING_STRCTN, node[0], node[1][1]),
node[0],
node[2]);
- return returnRewrite(node, res, "repl-dual-repl-ite");
+ return returnRewrite(node, res, Rewrite::REPL_DUAL_REPL_ITE);
}
}
if (invSuccess)
{
Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1][0], node[2]);
- return returnRewrite(node, res, "repl-repl2-inv");
+ return returnRewrite(node, res, Rewrite::REPL_REPL2_INV);
}
}
if (node[2].getKind() == STRING_STRREPL)
{
Node res =
nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]);
- return returnRewrite(node, res, "repl-repl3-inv");
+ return returnRewrite(node, res, Rewrite::REPL_REPL3_INV);
}
}
if (node[2][0] == node[1])
}
if (success)
{
- return returnRewrite(node, node[0], "repl-repl3-inv-id");
+ return returnRewrite(node, node[0], Rewrite::REPL_REPL3_INV_ID);
}
}
}
// second occurrence of x. Notice this is specific to single characters
// due to complications with finds that span multiple components for
// non-characters.
- return returnRewrite(node, ret, "repl-char-ncontrib-find");
+ return returnRewrite(node, ret, Rewrite::REPL_CHAR_NCONTRIB_FIND);
}
}
Node t = node[1];
if (Word::isEmpty(s) || Word::isEmpty(t))
{
- return returnRewrite(node, node[0], "replall-empty-find");
+ return returnRewrite(node, node[0], Rewrite::REPLALL_EMPTY_FIND);
}
std::size_t sizeS = Word::getLength(s);
std::size_t sizeT = Word::getLength(t);
} while (curr != std::string::npos && curr < sizeS);
// constant evaluation
Node res = utils::mkConcat(children, stype);
- return returnRewrite(node, res, "replall-const");
+ return returnRewrite(node, res, Rewrite::REPLALL_CONST);
}
// rewrites that apply to both replace and replaceall
if (node[1] == node[2])
{
- return returnRewrite(node, node[0], "rpl-id");
+ return returnRewrite(node, node[0], Rewrite::RPL_ID);
}
if (node[0] == node[1])
// only holds for replaceall if non-empty
if (nk == STRING_STRREPL || checkEntailNonEmpty(node[1]))
{
- return returnRewrite(node, node[2], "rpl-replace");
+ return returnRewrite(node, node[2], Rewrite::RPL_REPLACE);
}
}
std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
std::reverse(nvec.begin(), nvec.end());
Node retNode = nm->mkConst(String(nvec));
- return returnRewrite(node, retNode, "str-conv-const");
+ return returnRewrite(node, retNode, Rewrite::STR_CONV_CONST);
}
else if (x.getKind() == STRING_CONCAT)
{
std::reverse(children.begin(), children.end());
// rev( x1 ++ x2 ) --> rev( x2 ) ++ rev( x1 )
Node retNode = nm->mkNode(STRING_CONCAT, children);
- return returnRewrite(node, retNode, "str-rev-minscope-concat");
+ return returnRewrite(node, retNode, Rewrite::STR_REV_MINSCOPE_CONCAT);
}
else if (x.getKind() == STRING_REV)
{
// rev( rev( x ) ) --> x
Node retNode = x[0];
- return returnRewrite(node, retNode, "str-rev-idem");
+ return returnRewrite(node, retNode, Rewrite::STR_REV_IDEM);
}
return node;
}
if (n[0] == n[1])
{
Node ret = NodeManager::currentNM()->mkConst(true);
- return returnRewrite(n, ret, "suf/prefix-eq");
+ return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EQ);
}
if (n[0].isConst())
{
if (t.isEmptyString())
{
Node ret = NodeManager::currentNM()->mkConst(true);
- return returnRewrite(n, ret, "suf/prefix-empty-const");
+ return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY_CONST);
}
}
if (n[1].isConst())
ret = NodeManager::currentNM()->mkConst(true);
}
}
- return returnRewrite(n, ret, "suf/prefix-const");
+ return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CONST);
}
else if (lenS == 0)
{
Node ret = n[0].eqNode(n[1]);
- return returnRewrite(n, ret, "suf/prefix-empty");
+ return returnRewrite(n, ret, Rewrite::SUF_PREFIX_EMPTY);
}
else if (lenS == 1)
{
// (str.contains "A" x )
Node ret =
NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, n[1], n[0]);
- return returnRewrite(n, ret, "suf/prefix-ctn");
+ return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CTN);
}
}
Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, n[0]);
Node eqs = inferEqsFromContains(n[1], n[0]);
if (!eqs.isNull())
{
- return returnRewrite(n, eqs, "suf/prefix-to-eqs");
+ return returnRewrite(n, eqs, Rewrite::SUF_PREFIX_TO_EQS);
}
// general reduction to equality + substr
allEmptyEqs, std::vector<Node>(emptyNodes.begin(), emptyNodes.end()));
}
-Node SequencesRewriter::returnRewrite(Node node, Node ret, const char* c)
+Node SequencesRewriter::returnRewrite(Node node, Node ret, Rewrite r)
{
- Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << c
+ Trace("strings-rewrite") << "Rewrite " << node << " to " << ret << " by " << r
<< "." << std::endl;
NodeManager* nm = NodeManager::currentNM();
projects / cvc5.git / commitdiff