This commit replaces (old) internal string kind names to match the API / smt2 standard names.
{STRING_SUBSTR, cvc5::Kind::STRING_SUBSTR},
{STRING_UPDATE, cvc5::Kind::STRING_UPDATE},
{STRING_CHARAT, cvc5::Kind::STRING_CHARAT},
- {STRING_CONTAINS, cvc5::Kind::STRING_STRCTN},
- {STRING_INDEXOF, cvc5::Kind::STRING_STRIDOF},
+ {STRING_CONTAINS, cvc5::Kind::STRING_CONTAINS},
+ {STRING_INDEXOF, cvc5::Kind::STRING_INDEXOF},
{STRING_INDEXOF_RE, cvc5::Kind::STRING_INDEXOF_RE},
- {STRING_REPLACE, cvc5::Kind::STRING_STRREPL},
- {STRING_REPLACE_ALL, cvc5::Kind::STRING_STRREPLALL},
+ {STRING_REPLACE, cvc5::Kind::STRING_REPLACE},
+ {STRING_REPLACE_ALL, cvc5::Kind::STRING_REPLACE_ALL},
{STRING_REPLACE_RE, cvc5::Kind::STRING_REPLACE_RE},
{STRING_REPLACE_RE_ALL, cvc5::Kind::STRING_REPLACE_RE_ALL},
{STRING_TOLOWER, cvc5::Kind::STRING_TOLOWER},
{SEQ_EXTRACT, cvc5::Kind::STRING_SUBSTR},
{SEQ_UPDATE, cvc5::Kind::STRING_UPDATE},
{SEQ_AT, cvc5::Kind::STRING_CHARAT},
- {SEQ_CONTAINS, cvc5::Kind::STRING_STRCTN},
- {SEQ_INDEXOF, cvc5::Kind::STRING_STRIDOF},
- {SEQ_REPLACE, cvc5::Kind::STRING_STRREPL},
- {SEQ_REPLACE_ALL, cvc5::Kind::STRING_STRREPLALL},
+ {SEQ_CONTAINS, cvc5::Kind::STRING_CONTAINS},
+ {SEQ_INDEXOF, cvc5::Kind::STRING_INDEXOF},
+ {SEQ_REPLACE, cvc5::Kind::STRING_REPLACE},
+ {SEQ_REPLACE_ALL, cvc5::Kind::STRING_REPLACE_ALL},
{SEQ_REV, cvc5::Kind::STRING_REV},
{SEQ_PREFIX, cvc5::Kind::STRING_PREFIX},
{SEQ_SUFFIX, cvc5::Kind::STRING_SUFFIX},
{cvc5::Kind::STRING_SUBSTR, STRING_SUBSTR},
{cvc5::Kind::STRING_UPDATE, STRING_UPDATE},
{cvc5::Kind::STRING_CHARAT, STRING_CHARAT},
- {cvc5::Kind::STRING_STRCTN, STRING_CONTAINS},
- {cvc5::Kind::STRING_STRIDOF, STRING_INDEXOF},
+ {cvc5::Kind::STRING_CONTAINS, STRING_CONTAINS},
+ {cvc5::Kind::STRING_INDEXOF, STRING_INDEXOF},
{cvc5::Kind::STRING_INDEXOF_RE, STRING_INDEXOF_RE},
- {cvc5::Kind::STRING_STRREPL, STRING_REPLACE},
- {cvc5::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL},
+ {cvc5::Kind::STRING_REPLACE, STRING_REPLACE},
+ {cvc5::Kind::STRING_REPLACE_ALL, STRING_REPLACE_ALL},
{cvc5::Kind::STRING_REPLACE_RE, STRING_REPLACE_RE},
{cvc5::Kind::STRING_REPLACE_RE_ALL, STRING_REPLACE_RE_ALL},
{cvc5::Kind::STRING_TOLOWER, STRING_TOLOWER},
case cvc5::Kind::STRING_SUBSTR: return SEQ_EXTRACT;
case cvc5::Kind::STRING_UPDATE: return SEQ_UPDATE;
case cvc5::Kind::STRING_CHARAT: return SEQ_AT;
- case cvc5::Kind::STRING_STRCTN: return SEQ_CONTAINS;
- case cvc5::Kind::STRING_STRIDOF: return SEQ_INDEXOF;
- case cvc5::Kind::STRING_STRREPL: return SEQ_REPLACE;
- case cvc5::Kind::STRING_STRREPLALL: return SEQ_REPLACE_ALL;
+ case cvc5::Kind::STRING_CONTAINS: return SEQ_CONTAINS;
+ case cvc5::Kind::STRING_INDEXOF: return SEQ_INDEXOF;
+ case cvc5::Kind::STRING_REPLACE: return SEQ_REPLACE;
+ case cvc5::Kind::STRING_REPLACE_ALL: return SEQ_REPLACE_ALL;
case cvc5::Kind::STRING_REV: return SEQ_REV;
case cvc5::Kind::STRING_PREFIX: return SEQ_PREFIX;
case cvc5::Kind::STRING_SUFFIX: return SEQ_SUFFIX;
case kind::STRING_SUBSTR:
case kind::STRING_UPDATE:
case kind::STRING_CHARAT:
- case kind::STRING_STRCTN:
- case kind::STRING_STRIDOF:
+ case kind::STRING_CONTAINS:
+ case kind::STRING_INDEXOF:
case kind::STRING_INDEXOF_RE:
- case kind::STRING_STRREPL:
- case kind::STRING_STRREPLALL:
+ case kind::STRING_REPLACE:
+ case kind::STRING_REPLACE_ALL:
case kind::STRING_REPLACE_RE:
case kind::STRING_REPLACE_RE_ALL:
case kind::STRING_TOLOWER:
case kind::STRING_LENGTH: return "str.len";
case kind::STRING_SUBSTR: return "str.substr" ;
case kind::STRING_UPDATE: return "str.update";
- case kind::STRING_STRCTN: return "str.contains" ;
+ case kind::STRING_CONTAINS: return "str.contains";
case kind::STRING_CHARAT: return "str.at" ;
- case kind::STRING_STRIDOF: return "str.indexof" ;
+ case kind::STRING_INDEXOF: return "str.indexof";
case kind::STRING_INDEXOF_RE: return "str.indexof_re";
- case kind::STRING_STRREPL: return "str.replace" ;
- case kind::STRING_STRREPLALL: return "str.replace_all";
+ case kind::STRING_REPLACE: return "str.replace";
+ case kind::STRING_REPLACE_ALL: return "str.replace_all";
case kind::STRING_REPLACE_RE: return "str.replace_re";
case kind::STRING_REPLACE_RE_ALL: return "str.replace_re_all";
case kind::STRING_TOLOWER: return "str.tolower";
deq_child[1].push_back(1);
}
}
- if (nk == ITE || nk == STRING_STRREPL || nk == STRING_STRREPLALL)
+ if (nk == ITE || nk == STRING_REPLACE || nk == STRING_REPLACE_ALL)
{
deq_child[0].push_back(1);
deq_child[1].push_back(2);
}
- if (nk == STRING_STRREPL || nk == STRING_STRREPLALL)
+ if (nk == STRING_REPLACE || nk == STRING_REPLACE_ALL)
{
deq_child[0].push_back(0);
deq_child[1].push_back(1);
break;
}
- case kind::STRING_STRCTN:
+ case kind::STRING_CONTAINS:
{
const String& s = results[currNode[0]].d_str;
const String& t = results[currNode[1]].d_str;
break;
}
- case kind::STRING_STRIDOF:
+ case kind::STRING_INDEXOF:
{
const String& s = results[currNode[0]].d_str;
Integer s_len(s.size());
break;
}
- case kind::STRING_STRREPL:
+ case kind::STRING_REPLACE:
{
const String& s = results[currNode[0]].d_str;
const String& x = results[currNode[1]].d_str;
Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]);
Node out = d_exo[ii];
Node cont =
- NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre);
+ NodeManager::currentNM()->mkNode(kind::STRING_CONTAINS, out, nbvre);
Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl;
Node contr = Rewriter::rewrite(cont);
if (!contr.isConst())
Assert(d_examples_out[i].isConst());
Trace("sygus-sui-cterm-debug")
<< " " << results[i] << " <> " << d_examples_out[i];
- Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]);
+ Node cont = nm->mkNode(STRING_CONTAINS, d_examples_out[i], results[i]);
Node contr = Rewriter::rewrite(cont);
if (contr == d_false)
{
return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
}
}
- else if (ik == STRING_STRIDOF)
+ else if (ik == STRING_INDEXOF)
{
if (arg == 0 || arg == 1)
{
{
return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
}
- else if (ik == STRING_STRIDOF)
+ else if (ik == STRING_INDEXOF)
{
Assert(arg == 2);
return mkTypeValue(NodeManager::currentNM()->integerType(), -1);
}
}
}
- else if (aak == STRING_STRREPL)
+ else if (aak == STRING_REPLACE)
{
// over,under-approximations for len( replace( x, y, z ) )
// notice this is either len( x ) or ( len( x ) + len( z ) - len( y ) )
}
}
}
- else if (ak == STRING_STRIDOF)
+ else if (ak == STRING_INDEXOF)
{
// over,under-approximations for indexof( x, y, n )
if (isOverApprox)
{
d_extt.addFunctionKind(kind::STRING_SUBSTR);
d_extt.addFunctionKind(kind::STRING_UPDATE);
- d_extt.addFunctionKind(kind::STRING_STRIDOF);
+ d_extt.addFunctionKind(kind::STRING_INDEXOF);
d_extt.addFunctionKind(kind::STRING_INDEXOF_RE);
d_extt.addFunctionKind(kind::STRING_ITOS);
d_extt.addFunctionKind(kind::STRING_STOI);
- d_extt.addFunctionKind(kind::STRING_STRREPL);
- d_extt.addFunctionKind(kind::STRING_STRREPLALL);
+ d_extt.addFunctionKind(kind::STRING_REPLACE);
+ d_extt.addFunctionKind(kind::STRING_REPLACE_ALL);
d_extt.addFunctionKind(kind::STRING_REPLACE_RE);
d_extt.addFunctionKind(kind::STRING_REPLACE_RE_ALL);
- d_extt.addFunctionKind(kind::STRING_STRCTN);
+ d_extt.addFunctionKind(kind::STRING_CONTAINS);
d_extt.addFunctionKind(kind::STRING_IN_REGEXP);
d_extt.addFunctionKind(kind::STRING_LEQ);
d_extt.addFunctionKind(kind::STRING_TO_CODE);
{
pol = d_extfInfoTmp[n].d_const.getConst<bool>() ? 1 : -1;
}
- if (k == STRING_STRCTN)
+ if (k == STRING_CONTAINS)
{
if (pol == 1)
{
Node c_n = pol == -1 ? n.negate() : n;
Trace("strings-process-debug")
<< "Process reduction for " << n << ", pol = " << pol << std::endl;
- if (k == STRING_STRCTN && pol == 1)
+ if (k == STRING_CONTAINS && pol == 1)
{
Node x = n[0];
Node s = n[1];
else if (k != kind::STRING_TO_CODE)
{
NodeManager* nm = NodeManager::currentNM();
- Assert(k == STRING_SUBSTR || k == STRING_UPDATE || k == STRING_STRCTN
- || k == STRING_STRIDOF || k == STRING_INDEXOF_RE || k == STRING_ITOS
- || k == STRING_STOI || k == STRING_STRREPL || k == STRING_STRREPLALL
+ Assert(k == STRING_SUBSTR || k == STRING_UPDATE || k == STRING_CONTAINS
+ || k == STRING_INDEXOF || k == STRING_INDEXOF_RE || k == STRING_ITOS
+ || k == STRING_STOI || k == STRING_REPLACE || k == STRING_REPLACE_ALL
|| k == SEQ_NTH || k == STRING_REPLACE_RE
|| k == STRING_REPLACE_RE_ALL || k == STRING_LEQ
|| k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV);
// with a node n,
// this may need to be generalized if multiple inferences apply
- if (nr.getKind() == STRING_STRCTN)
+ if (nr.getKind() == STRING_CONTAINS)
{
Assert(in.d_const.isConst());
bool pol = in.d_const.getConst<bool>();
for (const Node& nrc : nr[index])
{
children[index] = nrc;
- Node conc = nm->mkNode(STRING_STRCTN, children);
+ Node conc = nm->mkNode(STRING_CONTAINS, children);
conc = Rewriter::rewrite(pol ? conc : conc.negate());
// check if it already (does not) hold
if (d_state.hasTerm(conc))
{
Node onr = d_extfInfoTmp[nr[0]].d_ctn[opol][i];
Node concOrig =
- nm->mkNode(STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1]);
+ nm->mkNode(STRING_CONTAINS, pol ? nr[1] : onr, pol ? onr : nr[1]);
Node conc = Rewriter::rewrite(concOrig);
// For termination concerns, we only do the inference if the contains
// does not rewrite (and thus does not introduce new terms).
operator STRING_SUBSTR 3 "string substr"
operator STRING_UPDATE 3 "string update"
operator STRING_CHARAT 2 "string charat"
-operator STRING_STRCTN 2 "string contains"
+operator STRING_CONTAINS 2 "string contains"
operator STRING_LT 2 "string less than"
operator STRING_LEQ 2 "string less than or equal"
-operator STRING_STRIDOF 3 "string index of substring"
+operator STRING_INDEXOF 3 "string index of substring"
operator STRING_INDEXOF_RE 3 "string index of regular expression match"
-operator STRING_STRREPL 3 "string replace"
-operator STRING_STRREPLALL 3 "string replace all"
+operator STRING_REPLACE 3 "string replace"
+operator STRING_REPLACE_ALL 3 "string replace all"
operator STRING_REPLACE_RE 3 "string replace regular expression match"
operator STRING_REPLACE_RE_ALL 3 "string replace all regular expression matches"
operator STRING_PREFIX 2 "string prefixof"
typerule STRING_SUBSTR ::cvc5::theory::strings::StringSubstrTypeRule
typerule STRING_UPDATE ::cvc5::theory::strings::StringUpdateTypeRule
typerule STRING_CHARAT ::cvc5::theory::strings::StringAtTypeRule
-typerule STRING_STRCTN ::cvc5::theory::strings::StringRelationTypeRule
-typerule STRING_STRIDOF ::cvc5::theory::strings::StringIndexOfTypeRule
+typerule STRING_CONTAINS ::cvc5::theory::strings::StringRelationTypeRule
+typerule STRING_INDEXOF ::cvc5::theory::strings::StringIndexOfTypeRule
typerule STRING_INDEXOF_RE "SimpleTypeRule<RInteger, AString, ARegExp, AInteger>"
-typerule STRING_STRREPL ::cvc5::theory::strings::StringReplaceTypeRule
-typerule STRING_STRREPLALL ::cvc5::theory::strings::StringReplaceTypeRule
+typerule STRING_REPLACE ::cvc5::theory::strings::StringReplaceTypeRule
+typerule STRING_REPLACE_ALL ::cvc5::theory::strings::StringReplaceTypeRule
typerule STRING_REPLACE_RE "SimpleTypeRule<RString, AString, ARegExp, AString>"
typerule STRING_REPLACE_RE_ALL "SimpleTypeRule<RString, AString, ARegExp, AString>"
typerule STRING_PREFIX ::cvc5::theory::strings::StringStrToBoolTypeRule
non_greedy_find_vars.push_back(k);
prev_end = nm->mkNode(PLUS, prev_end, k);
}
- Node curr = nm->mkNode(STRING_STRIDOF, x, sc, prev_end);
+ Node curr = nm->mkNode(STRING_INDEXOF, x, sc, prev_end);
Node idofFind = curr.eqNode(nm->mkConst(Rational(-1))).negate();
conj.push_back(idofFind);
prev_end = nm->mkNode(PLUS, curr, lensc);
if (node[i] == empty)
{
Node ne = node[1 - i];
- if (ne.getKind() == STRING_STRREPL)
+ if (ne.getKind() == STRING_REPLACE)
{
// (= "" (str.replace x y x)) ---> (= x "")
if (ne[0] == ne[2])
// ------- rewrites for (= (str.replace _ _ _) _)
for (size_t i = 0; i < 2; i++)
{
- if (node[i].getKind() == STRING_STRREPL)
+ if (node[i].getKind() == STRING_REPLACE)
{
Node repl = node[i];
Node x = node[1 - i];
if (StringsEntail::checkNonEmpty(x) && repl[0] == empty)
{
Node ret = nm->mkNode(
- EQUAL, empty, nm->mkNode(STRING_STRREPL, x, repl[2], repl[1]));
+ EQUAL, empty, nm->mkNode(STRING_REPLACE, x, repl[2], repl[1]));
return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_EMP);
}
Node eq = Rewriter::rewrite(nm->mkNode(EQUAL, repl[1], repl[2]));
if (eq.isConst() && !eq.getConst<bool>())
{
- Node ret = nm->mkNode(NOT, nm->mkNode(STRING_STRCTN, x, repl[1]));
+ Node ret = nm->mkNode(NOT, nm->mkNode(STRING_CONTAINS, x, repl[1]));
return returnRewrite(node, ret, Rewrite::STR_EQ_REPL_NOT_CTN);
}
}
return returnRewrite(node, retNode, Rewrite::LEN_CONCAT);
}
}
- else if (nk0 == STRING_STRREPL || nk0 == STRING_STRREPLALL)
+ else if (nk0 == STRING_REPLACE || nk0 == STRING_REPLACE_ALL)
{
Node len1 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][1]));
Node len2 = Rewriter::rewrite(nm->mkNode(STRING_LENGTH, node[0][2]));
&& constIdx != nchildren - 1)
{
// x in re.++(_*, "abc", _*) ---> str.contains(x, "abc")
- Node retNode = nm->mkNode(STRING_STRCTN, x, constStr);
+ Node retNode = nm->mkNode(STRING_CONTAINS, x, constStr);
return returnRewrite(node, retNode, Rewrite::RE_CONCAT_TO_CONTAINS);
}
}
{
retNode = rewriteUpdate(node);
}
- else if (nk == kind::STRING_STRCTN)
+ else if (nk == kind::STRING_CONTAINS)
{
retNode = rewriteContains(node);
}
- else if (nk == kind::STRING_STRIDOF)
+ else if (nk == kind::STRING_INDEXOF)
{
retNode = rewriteIndexof(node);
}
{
retNode = rewriteIndexofRe(node);
}
- else if (nk == kind::STRING_STRREPL)
+ else if (nk == kind::STRING_REPLACE)
{
retNode = rewriteReplace(node);
}
- else if (nk == kind::STRING_STRREPLALL)
+ else if (nk == kind::STRING_REPLACE_ALL)
{
retNode = rewriteReplaceAll(node);
}
return returnRewrite(node, ret, Rewrite::SS_START_GEQ_LEN);
}
}
- else if (node[0].getKind() == STRING_STRREPL)
+ else if (node[0].getKind() == STRING_REPLACE)
{
// (str.substr (str.replace x y z) 0 n)
// ---> (str.replace (str.substr x 0 n) y z)
&& StringsEntail::checkLengthOne(node[0][2], true))
{
Node ret = nm->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
nm->mkNode(kind::STRING_SUBSTR, node[0][0], node[1], node[2]),
node[0][1],
node[0][2]);
Node SequencesRewriter::rewriteContains(Node node)
{
- Assert(node.getKind() == kind::STRING_STRCTN);
+ Assert(node.getKind() == kind::STRING_CONTAINS);
NodeManager* nm = NodeManager::currentNM();
if (node[0] == node[1])
NodeBuilder nb(OR);
for (const Node& ncc : nc1)
{
- nb << nm->mkNode(STRING_STRCTN, ncc, node[1]);
+ nb << nm->mkNode(STRING_CONTAINS, ncc, node[1]);
}
Node ret = nb.constructNode();
// str.contains( x ++ y, "A" ) --->
// str.contains( x, "A" ) OR str.contains( y, "A" )
return returnRewrite(node, ret, Rewrite::CTN_CONCAT_CHAR);
}
- else if (node[0].getKind() == STRING_STRREPL)
+ else if (node[0].getKind() == STRING_REPLACE)
{
Node rplDomain = d_stringsEntail.checkContains(node[0][1], node[1]);
if (!rplDomain.isNull() && !rplDomain.getConst<bool>())
{
- Node d1 = nm->mkNode(STRING_STRCTN, node[0][0], node[1]);
+ Node d1 = nm->mkNode(STRING_CONTAINS, node[0][0], node[1]);
Node d2 =
nm->mkNode(AND,
- nm->mkNode(STRING_STRCTN, node[0][0], node[0][1]),
- nm->mkNode(STRING_STRCTN, node[0][2], node[1]));
+ nm->mkNode(STRING_CONTAINS, node[0][0], node[0][1]),
+ nm->mkNode(STRING_CONTAINS, node[0][2], node[1]));
Node ret = nm->mkNode(OR, d1, d2);
// If str.contains( y, "A" ) ---> false, then:
// str.contains( str.replace( x, y, z ), "A" ) --->
if (StringsEntail::stripConstantEndpoints(nc1, nc2, nb, ne))
{
Node ret = NodeManager::currentNM()->mkNode(
- kind::STRING_STRCTN, utils::mkConcat(nc1, stype), node[1]);
+ kind::STRING_CONTAINS, utils::mkConcat(nc1, stype), node[1]);
return returnRewrite(node, ret, Rewrite::CTN_STRIP_ENDPT);
}
for (const Node& n : nc2)
{
- if (n.getKind() == kind::STRING_STRREPL)
+ if (n.getKind() == kind::STRING_REPLACE)
{
// (str.contains x (str.replace y z w)) --> false
// if (str.contains x y) = false and (str.contains x w) = false
spl[1].insert(spl[1].end(), nc0.begin() + i + 1, nc0.end());
Node ret = NodeManager::currentNM()->mkNode(
kind::OR,
- NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
+ NodeManager::currentNM()->mkNode(kind::STRING_CONTAINS,
utils::mkConcat(spl[0], stype),
node[1]),
- NodeManager::currentNM()->mkNode(kind::STRING_STRCTN,
+ NodeManager::currentNM()->mkNode(kind::STRING_CONTAINS,
utils::mkConcat(spl[1], stype),
node[1]));
return returnRewrite(node, ret, Rewrite::CTN_SPLIT);
return returnRewrite(node, ret, Rewrite::CTN_SUBSTR);
}
}
- else if (node[0].getKind() == kind::STRING_STRREPL)
+ else if (node[0].getKind() == kind::STRING_REPLACE)
{
if (node[1].isConst() && node[0][1].isConst() && node[0][2].isConst())
{
{
// (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]);
+ Node ret = nm->mkNode(STRING_CONTAINS, node[0][0], node[1]);
return returnRewrite(node, ret, Rewrite::CTN_REPL_CNSTS_TO_CTN);
}
}
// (str.contains (str.replace x y x) y) ---> (str.contains x y)
if (node[0][1] == node[1])
{
- Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
+ Node ret = nm->mkNode(kind::STRING_CONTAINS, node[0][0], node[1]);
return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN);
}
// if (str.len z) <= 1
if (StringsEntail::checkLengthOne(node[1]))
{
- Node ret = nm->mkNode(kind::STRING_STRCTN, node[0][0], node[1]);
+ Node ret = nm->mkNode(kind::STRING_CONTAINS, node[0][0], node[1]);
return returnRewrite(node, ret, Rewrite::CTN_REPL_LEN_ONE_TO_CTN);
}
}
// (or (str.contains x y) (str.contains x z))
if (node[0][2] == node[1])
{
- 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]));
+ Node ret =
+ nm->mkNode(OR,
+ nm->mkNode(STRING_CONTAINS, node[0][0], node[0][1]),
+ nm->mkNode(STRING_CONTAINS, node[0][0], node[0][2]));
return returnRewrite(node, ret, Rewrite::CTN_REPL_TO_CTN_DISJ);
}
{
Node empty = Word::mkEmptyWord(stype);
Node ret = nm->mkNode(
- kind::STRING_STRCTN,
- nm->mkNode(kind::STRING_STRREPL, node[0][0], node[0][1], empty),
+ kind::STRING_CONTAINS,
+ nm->mkNode(kind::STRING_REPLACE, node[0][0], node[0][1], empty),
node[1]);
return returnRewrite(node, ret, Rewrite::CTN_REPL_SIMP_REPL);
}
}
}
- if (node[1].getKind() == kind::STRING_STRREPL)
+ if (node[1].getKind() == kind::STRING_REPLACE)
{
// (str.contains x (str.replace y x y)) --->
// (str.contains x y)
if (node[0] == node[1][1] && node[1][0] == node[1][2])
{
- Node ret = nm->mkNode(kind::STRING_STRCTN, node[0], node[1][0]);
+ Node ret = nm->mkNode(kind::STRING_CONTAINS, node[0], node[1][0]);
return returnRewrite(node, ret, Rewrite::CTN_REPL);
}
Node SequencesRewriter::rewriteIndexof(Node node)
{
- Assert(node.getKind() == kind::STRING_STRIDOF);
+ Assert(node.getKind() == kind::STRING_INDEXOF);
NodeManager* nm = NodeManager::currentNM();
if (node[2].isConst() && node[2].getConst<Rational>().sgn() < 0)
if (node[0] != emp)
{
// indexof( x, x, z ) ---> indexof( "", "", z )
- Node ret = nm->mkNode(STRING_STRIDOF, emp, emp, node[2]);
+ Node ret = nm->mkNode(STRING_INDEXOF, emp, emp, node[2]);
return returnRewrite(node, ret, Rewrite::IDOF_EQ_NORM);
}
}
// For example:
// 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]);
+ Node ret = nm->mkNode(kind::STRING_INDEXOF, nn, node[1], node[2]);
return returnRewrite(node, ret, Rewrite::IDOF_DEF_CTN);
}
Node ret = nm->mkNode(
kind::PLUS,
nm->mkNode(kind::STRING_LENGTH, utils::mkConcat(nb, stype)),
- nm->mkNode(kind::STRING_STRIDOF,
+ nm->mkNode(kind::STRING_INDEXOF,
utils::mkConcat(children0, stype),
node[1],
node[2]));
Node ret =
nm->mkNode(PLUS,
nm->mkNode(MINUS, node[2], new_len),
- nm->mkNode(STRING_STRIDOF, nn, node[1], new_len));
+ nm->mkNode(STRING_INDEXOF, nn, node[1], new_len));
return returnRewrite(node, ret, Rewrite::IDOF_STRIP_SYM_LEN);
}
}
std::vector<Node> children(normNrChildren);
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]);
+ Node res = nm->mkNode(kind::STRING_INDEXOF, nn, node[1], node[2]);
return returnRewrite(node, res, Rewrite::IDOF_NORM_PREFIX);
}
}
if (StringsEntail::stripConstantEndpoints(children0, children1, cb, ce, -1))
{
Node ret = utils::mkConcat(children0, stype);
- ret = nm->mkNode(STRING_STRIDOF, ret, node[1], node[2]);
+ ret = nm->mkNode(STRING_INDEXOF, ret, node[1], node[2]);
// For example:
// str.indexof( str.++( x, "A" ), "B", 0 ) ---> str.indexof( x, "B", 0 )
return returnRewrite(node, ret, Rewrite::RPL_PULL_ENDPT);
Node SequencesRewriter::rewriteReplace(Node node)
{
- Assert(node.getKind() == kind::STRING_STRREPL);
+ Assert(node.getKind() == kind::STRING_REPLACE);
NodeManager* nm = NodeManager::currentNM();
if (node[1].isConst() && Word::isEmpty(node[1]))
Node nn1 = utils::mkConcat(emptyNodes, stype);
if (node[1] != nn1)
{
- Node ret = nm->mkNode(STRING_STRREPL, node[0], nn1, node[2]);
+ Node ret = nm->mkNode(STRING_REPLACE, node[0], nn1, node[2]);
return returnRewrite(node, ret, Rewrite::RPL_X_Y_X_SIMP);
}
}
utils::getConcat(node[1], children1);
// check if contains definitely does (or does not) hold
- Node cmp_con = nm->mkNode(kind::STRING_STRCTN, node[0], node[1]);
+ Node cmp_con = nm->mkNode(kind::STRING_CONTAINS, node[0], node[1]);
Node cmp_conr = Rewriter::rewrite(cmp_con);
if (cmp_conr.isConst())
{
// this is independent of whether the second argument may be empty
std::vector<Node> scc;
scc.push_back(NodeManager::currentNM()->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
utils::mkConcat(children0, stype),
node[1],
node[2]));
Node nn1 = utils::mkConcat(emptyNodesList, stype);
if (nn1 != node[1] || nn2 != node[2])
{
- Node res = nm->mkNode(kind::STRING_STRREPL, node[0], nn1, nn2);
+ Node res = nm->mkNode(kind::STRING_REPLACE, node[0], nn1, nn2);
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);
+ Node res = nm->mkNode(kind::STRING_REPLACE, node[0], node[1], nn2);
return returnRewrite(node, res, Rewrite::RPL_CNTS_SUBSTS);
}
}
std::vector<Node> cc;
cc.insert(cc.end(), cb.begin(), cb.end());
cc.push_back(
- NodeManager::currentNM()->mkNode(kind::STRING_STRREPL,
+ NodeManager::currentNM()->mkNode(kind::STRING_REPLACE,
utils::mkConcat(children0, stype),
node[1],
node[2]));
lastChild1[1],
nm->mkNode(
kind::PLUS, len0, one, nm->mkNode(kind::UMINUS, partLen1))));
- Node res = nm->mkNode(kind::STRING_STRREPL,
+ Node res = nm->mkNode(kind::STRING_REPLACE,
node[0],
utils::mkConcat(children1, stype),
node[2]);
}
}
- if (node[0].getKind() == STRING_STRREPL)
+ if (node[0].getKind() == STRING_REPLACE)
{
Node x = node[0];
Node y = node[1];
Node wEqZ = Rewriter::rewrite(nm->mkNode(kind::EQUAL, w, z));
if (wEqZ.isConst() && !wEqZ.getConst<bool>())
{
- Node ret = nm->mkNode(kind::STRING_STRREPL,
- nm->mkNode(kind::STRING_STRREPL, y, w, z),
+ Node ret = nm->mkNode(kind::STRING_REPLACE,
+ nm->mkNode(kind::STRING_REPLACE, y, w, z),
y,
z);
return returnRewrite(node, ret, Rewrite::REPL_REPL_SHORT_CIRCUIT);
}
}
- if (node[1].getKind() == STRING_STRREPL)
+ if (node[1].getKind() == STRING_REPLACE)
{
if (node[1][0] == node[0])
{
if (dualReplIteSuccess)
{
Node res = nm->mkNode(ITE,
- nm->mkNode(STRING_STRCTN, node[0], node[1][1]),
+ nm->mkNode(STRING_CONTAINS, node[0], node[1][1]),
node[0],
node[2]);
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]);
+ Node res = nm->mkNode(kind::STRING_REPLACE, node[0], node[1][0], node[2]);
return returnRewrite(node, res, Rewrite::REPL_REPL2_INV);
}
}
- if (node[2].getKind() == STRING_STRREPL)
+ if (node[2].getKind() == STRING_REPLACE)
{
if (node[2][1] == node[0])
{
if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>())
{
Node res =
- nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]);
+ nm->mkNode(kind::STRING_REPLACE, node[0], node[1], node[2][0]);
return returnRewrite(node, res, Rewrite::REPL_REPL3_INV);
}
}
Node rem = utils::mkConcat(remc, stype);
Node ret =
nm->mkNode(STRING_CONCAT,
- nm->mkNode(STRING_STRREPL, lastLhs, node[1], node[2]),
+ nm->mkNode(STRING_REPLACE, lastLhs, node[1], node[2]),
rem);
// for example:
// str.replace( x ++ x, "A", y ) ---> str.replace( x, "A", y ) ++ x
Node SequencesRewriter::rewriteReplaceAll(Node node)
{
- Assert(node.getKind() == STRING_STRREPLALL);
+ Assert(node.getKind() == STRING_REPLACE_ALL);
TypeNode stype = node.getType();
Node SequencesRewriter::rewriteReplaceInternal(Node node)
{
Kind nk = node.getKind();
- Assert(nk == STRING_STRREPL || nk == STRING_STRREPLALL);
+ Assert(nk == STRING_REPLACE || nk == STRING_REPLACE_ALL);
if (node[1] == node[2])
{
if (node[0] == node[1])
{
// only holds for replaceall if non-empty
- if (nk == STRING_STRREPL || StringsEntail::checkNonEmpty(node[1]))
+ if (nk == STRING_REPLACE || StringsEntail::checkNonEmpty(node[1]))
{
return returnRewrite(node, node[2], Rewrite::RPL_REPLACE);
}
// (str.prefix x "A") and (str.suffix x "A") are equivalent to
// (str.contains "A" x )
Node ret =
- NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, n[1], n[0]);
+ NodeManager::currentNM()->mkNode(kind::STRING_CONTAINS, n[1], n[0]);
return returnRewrite(n, ret, Rewrite::SUF_PREFIX_CTN);
}
}
{
// SK_FIRST_CTN_PRE(x,y) ---> SK_PREFIX(x, indexof(x,y,0))
id = SK_PREFIX;
- b = nm->mkNode(STRING_STRIDOF, a, b, d_zero);
+ b = nm->mkNode(STRING_INDEXOF, a, b, d_zero);
}
if (id == SK_ID_V_UNIFIED_SPT || id == SK_ID_V_UNIFIED_SPT_REV)
if (!computeRemainder && dir == 0)
{
- if (n1.getKind() == STRING_STRREPL)
+ if (n1.getKind() == STRING_REPLACE)
{
// (str.contains (str.replace x y z) w) ---> true
// if (str.contains x w) --> true and (str.contains z w) ---> true
Node StringsEntail::checkContains(Node a, Node b, bool fullRewriter)
{
NodeManager* nm = NodeManager::currentNM();
- Node ctn = nm->mkNode(STRING_STRCTN, a, b);
+ Node ctn = nm->mkNode(STRING_CONTAINS, a, b);
if (fullRewriter)
{
{
prev = ctn;
ctn = d_rewriter.rewriteContains(ctn);
- } while (prev != ctn && ctn.getKind() == STRING_STRCTN);
+ } while (prev != ctn && ctn.getKind() == STRING_CONTAINS);
}
Assert(ctn.getType().isBoolean());
{
return a[0];
}
- else if (a.getKind() == STRING_STRREPL)
+ else if (a.getKind() == STRING_REPLACE)
{
return getMultisetApproximation(nm->mkNode(STRING_CONCAT, a[0], a[2]));
}
{
switch (n.getKind())
{
- case STRING_STRREPL:
+ case STRING_REPLACE:
{
if (Word::isEmpty(n[0]))
{
LT, t, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
lemma = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
}
- else if (tk == STRING_STRIDOF || tk == STRING_INDEXOF_RE)
+ else if (tk == STRING_INDEXOF || tk == STRING_INDEXOF_RE)
{
// (and
// (or (= (f x y n) (- 1)) (>= (f x y n) n))
// (>= (str.to_int x) (- 1))
lemma = nm->mkNode(GEQ, t, nm->mkConst(Rational(-1)));
}
- else if (tk == STRING_STRCTN)
+ else if (tk == STRING_CONTAINS)
{
// ite( (str.contains s r), (= s (str.++ sk1 r sk2)), (not (= s r)))
Node sk1 =
Kind k = n.getKind();
if (!options::stringExp())
{
- if (k == STRING_STRIDOF || k == STRING_INDEXOF_RE || k == STRING_ITOS
- || k == STRING_STOI || k == STRING_STRREPL || k == STRING_SUBSTR
- || k == STRING_STRREPLALL || k == SEQ_NTH || k == STRING_REPLACE_RE
- || k == STRING_REPLACE_RE_ALL || k == STRING_STRCTN || k == STRING_LEQ
+ if (k == STRING_INDEXOF || k == STRING_INDEXOF_RE || k == STRING_ITOS
+ || k == STRING_STOI || k == STRING_REPLACE || k == STRING_SUBSTR
+ || k == STRING_REPLACE_ALL || k == SEQ_NTH || k == STRING_REPLACE_RE
+ || k == STRING_REPLACE_RE_ALL || k == STRING_CONTAINS || k == STRING_LEQ
|| k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV
|| k == STRING_UPDATE)
{
else if (tn.isBoolean())
{
// All kinds that we do congruence over that may return a Boolean go here
- if (k==STRING_STRCTN || k == STRING_LEQ || k == SEQ_NTH)
+ if (k == STRING_CONTAINS || k == STRING_LEQ || k == SEQ_NTH)
{
// Get triggered for both equal and dis-equal
ee->addTriggerPredicate(n);
// for concat/const/replace, introduce proxy var and state length relation
regTermLem = getRegisterTermLemma(n);
}
- else if (n.getKind() != STRING_STRCTN)
+ else if (n.getKind() != STRING_CONTAINS)
{
// we don't send out eager reduction lemma for str.contains currently
Node eagerRedLemma = eagerReduce(n, &d_skCache);
// `seq.nth` is not always defined, and so we do not evaluate it eagerly.
d_equalityEngine->addFunctionKind(kind::SEQ_NTH, false);
// extended functions
- d_equalityEngine->addFunctionKind(kind::STRING_STRCTN, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_CONTAINS, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_LEQ, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_SUBSTR, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_UPDATE, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_ITOS, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_STOI, eagerEval);
- d_equalityEngine->addFunctionKind(kind::STRING_STRIDOF, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_INDEXOF, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_INDEXOF_RE, eagerEval);
- d_equalityEngine->addFunctionKind(kind::STRING_STRREPL, eagerEval);
- d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_REPLACE, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_ALL, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_RE_ALL, eagerEval);
- d_equalityEngine->addFunctionKind(kind::STRING_STRREPLALL, eagerEval);
+ d_equalityEngine->addFunctionKind(kind::STRING_REPLACE_ALL, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_TOLOWER, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_TOUPPER, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_REV, eagerEval);
// Thus, str.update( s, n, r ) = skt
retNode = skt;
}
- else if (t.getKind() == kind::STRING_STRIDOF)
+ else if (t.getKind() == kind::STRING_INDEXOF)
{
// processing term: indexof( x, y, n )
Node x = t[0];
sc->mkSkolemCached(st, y, SkolemCache::SK_FIRST_CTN_POST, "iopost");
// ~contains( substr( x, n, len( x ) - n ), y )
- Node c11 = nm->mkNode(STRING_STRCTN, st, y).negate();
+ Node c11 = nm->mkNode(STRING_CONTAINS, st, y).negate();
// n > len( x )
Node c12 = nm->mkNode(GT, n, nm->mkNode(STRING_LENGTH, x));
// 0 > n
// ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y )
Node c32 =
nm->mkNode(
- STRING_STRCTN,
+ STRING_CONTAINS,
nm->mkNode(
STRING_CONCAT,
io2,
asserts.push_back(lemma);
retNode = skt;
}
- else if (t.getKind() == kind::STRING_STRREPL)
+ else if (t.getKind() == kind::STRING_REPLACE)
{
// processing term: replace( x, y, z )
Node x = t[0];
Node c1 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, z, x));
// contains( x, y )
- Node cond2 = nm->mkNode(kind::STRING_STRCTN, x, y);
+ Node cond2 = nm->mkNode(kind::STRING_CONTAINS, x, y);
// x = str.++( rp1, y, rp2 )
Node c21 = x.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, y, rp2));
// rpw = str.++( rp1, z, rp2 )
Node c22 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, rp1, z, rp2));
// ~contains( str.++( rp1, substr( y, 0, len(y)-1 ) ), y )
Node c23 =
- nm->mkNode(kind::STRING_STRCTN,
+ nm->mkNode(kind::STRING_CONTAINS,
nm->mkNode(
kind::STRING_CONCAT,
rp1,
// Thus, replace( x, y, z ) = rpw.
retNode = rpw;
}
- else if (t.getKind() == kind::STRING_STRREPLALL)
+ else if (t.getKind() == kind::STRING_REPLACE_ALL)
{
// processing term: replaceall( x, y, z )
Node x = t[0];
lem.push_back(rpaw.eqNode(nm->mkNode(APPLY_UF, us, zero)));
lem.push_back(usno.eqNode(rem));
lem.push_back(nm->mkNode(APPLY_UF, uf, zero).eqNode(zero));
- lem.push_back(nm->mkNode(STRING_STRIDOF, x, y, ufno).eqNode(negOne));
+ lem.push_back(nm->mkNode(STRING_INDEXOF, x, y, ufno).eqNode(negOne));
Node i = SkolemCache::mkIndexVar(t);
Node bvli = nm->mkNode(BOUND_VAR_LIST, i);
nm->mkNode(AND, nm->mkNode(GEQ, i, zero), nm->mkNode(LT, i, numOcc));
Node ufi = nm->mkNode(APPLY_UF, uf, i);
Node ufip1 = nm->mkNode(APPLY_UF, uf, nm->mkNode(PLUS, i, one));
- Node ii = nm->mkNode(STRING_STRIDOF, x, y, ufi);
+ Node ii = nm->mkNode(STRING_INDEXOF, x, y, ufi);
Node cc = nm->mkNode(
STRING_CONCAT,
nm->mkNode(STRING_SUBSTR, x, ufi, nm->mkNode(MINUS, ii, ufi)),
// Thus, (str.rev x) = r
retNode = r;
}
- else if (t.getKind() == kind::STRING_STRCTN)
+ else if (t.getKind() == kind::STRING_CONTAINS)
{
Node x = t[0];
Node s = t[1];
{
TypeNode tn;
Kind k = n.getKind();
- if (k == STRING_STRIDOF || k == STRING_INDEXOF_RE || k == STRING_LENGTH
- || k == STRING_STRCTN || k == SEQ_NTH || k == STRING_PREFIX
+ if (k == STRING_INDEXOF || k == STRING_INDEXOF_RE || k == STRING_LENGTH
+ || k == STRING_CONTAINS || k == SEQ_NTH || k == STRING_PREFIX
|| k == STRING_SUFFIX)
{
// owning string type is the type of first argument
}
}
- if ((arg == 1 && k == STRING_STRCTN) || (arg == 0 && k == STRING_SUBSTR))
+ if ((arg == 1 && k == STRING_CONTAINS) || (arg == 0 && k == STRING_SUBSTR))
{
// empty string
if (strings::Word::getLength(n) == 0)
return true;
}
}
- if ((arg != 0 && k == STRING_SUBSTR) || (arg == 2 && k == STRING_STRIDOF))
+ if ((arg != 0 && k == STRING_SUBSTR) || (arg == 2 && k == STRING_INDEXOF))
{
// negative integer
if (n.getConst<Rational>().sgn() < 0)
Evaluator eval;
{
- Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, one);
+ Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, one);
Node r = eval.eval(n, args, vals);
ASSERT_EQ(r, Rewriter::rewrite(n));
}
{
- Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, one);
+ Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, one);
Node r = eval.eval(n, args, vals);
ASSERT_EQ(r, Rewriter::rewrite(n));
}
{
- Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, empty, two);
+ Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, empty, two);
Node r = eval.eval(n, args, vals);
ASSERT_EQ(r, Rewriter::rewrite(n));
}
{
- Node n = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, a, two);
+ Node n = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, a, two);
Node r = eval.eval(n, args, vals);
ASSERT_EQ(r, Rewriter::rewrite(n));
}
// (str.replace "" s (str.substr "B" x x)))
Node lhs = d_nodeManager->mkNode(
kind::STRING_SUBSTR,
- d_nodeManager->mkNode(kind::STRING_STRREPL, empty, s, b),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, empty, s, b),
x,
x);
Node rhs = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
empty,
s,
d_nodeManager->mkNode(kind::STRING_SUBSTR, b, x, x));
// (str.replace (str.substr s 0 x) "A" "B")
Node substr_repl = d_nodeManager->mkNode(
kind::STRING_SUBSTR,
- d_nodeManager->mkNode(kind::STRING_STRREPL, s, a, b),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, s, a, b),
zero,
x);
Node repl_substr = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
d_nodeManager->mkNode(kind::STRING_SUBSTR, s, zero, x),
a,
b);
one);
substr_repl = d_nodeManager->mkNode(
kind::STRING_SUBSTR,
- d_nodeManager->mkNode(kind::STRING_STRREPL, s, substr_y, b),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, s, substr_y, b),
zero,
x);
repl_substr = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
d_nodeManager->mkNode(kind::STRING_SUBSTR, s, zero, x),
substr_y,
b);
// (str.++ (str.replace "A" x "") "A")
//
// (str.++ "A" (str.replace "A" x ""))
- Node repl_a_x_e = d_nodeManager->mkNode(kind::STRING_STRREPL, a, x, empty);
+ Node repl_a_x_e = d_nodeManager->mkNode(kind::STRING_REPLACE, a, x, empty);
Node repl_a = d_nodeManager->mkNode(kind::STRING_CONCAT, repl_a_x_e, a);
Node a_repl = d_nodeManager->mkNode(kind::STRING_CONCAT, a, repl_a_x_e);
sameNormalForm(repl_a, a_repl);
// (str.++ y (str.substr y 0 3) (str.replace "" x (str.substr y 0 3)) "A"
// (str.substr y 0 3))
Node z = d_nodeManager->mkNode(kind::STRING_SUBSTR, y, zero, three);
- Node repl_e_x_z = d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, z);
+ Node repl_e_x_z = d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, z);
repl_a = d_nodeManager->mkNode(kind::STRING_CONCAT, {y, repl_e_x_z, z, a, z});
a_repl = d_nodeManager->mkNode(kind::STRING_CONCAT, {y, z, repl_e_x_z, a, z});
sameNormalForm(repl_a, a_repl);
// "A" 0 i))
Node charat_a = d_nodeManager->mkNode(kind::STRING_CHARAT, a, i);
Node repl_e_x_s =
- d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, substr_a);
+ d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, substr_a);
Node repl_substr_a = d_nodeManager->mkNode(
kind::STRING_CONCAT, repl_e_x_s, substr_a, charat_a);
Node a_repl_substr = d_nodeManager->mkNode(
d_nodeManager->mkNode(kind::STRING_CONCAT, x, x));
Node concat2 = d_nodeManager->mkNode(
kind::STRING_CONCAT,
- {gh, x, d_nodeManager->mkNode(kind::STRING_STRREPL, x, gh, ij), ij});
+ {gh, x, d_nodeManager->mkNode(kind::STRING_REPLACE, x, gh, ij), ij});
Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1);
Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2);
ASSERT_EQ(res_concat1, res_concat2);
// (str.to.int (str.indexof "A" x 1))
//
// (str.to.int (str.indexof "B" x 1))
- Node a_idof_x = d_nodeManager->mkNode(kind::STRING_STRIDOF, a, x, two);
+ Node a_idof_x = d_nodeManager->mkNode(kind::STRING_INDEXOF, a, x, two);
Node itos_a_idof_x = d_nodeManager->mkNode(kind::STRING_ITOS, a_idof_x);
- Node b_idof_x = d_nodeManager->mkNode(kind::STRING_STRIDOF, b, x, two);
+ Node b_idof_x = d_nodeManager->mkNode(kind::STRING_INDEXOF, b, x, two);
Node itos_b_idof_x = d_nodeManager->mkNode(kind::STRING_ITOS, b_idof_x);
sameNormalForm(itos_a_idof_x, itos_b_idof_x);
//
// (str.indexof (str.++ "AAAD" x) y 3)
Node idof_abcd =
- d_nodeManager->mkNode(kind::STRING_STRIDOF,
+ d_nodeManager->mkNode(kind::STRING_INDEXOF,
d_nodeManager->mkNode(kind::STRING_CONCAT, abcd, x),
y,
three);
Node idof_aaad =
- d_nodeManager->mkNode(kind::STRING_STRIDOF,
+ d_nodeManager->mkNode(kind::STRING_INDEXOF,
d_nodeManager->mkNode(kind::STRING_CONCAT, aaad, x),
y,
three);
// (str.indexof (str.substr x 1 i) "A" i) ---> -1
Node idof_substr = d_nodeManager->mkNode(
- kind::STRING_STRIDOF,
+ kind::STRING_INDEXOF,
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, i),
a,
i);
//
// (+ 2 (str.indexof (str.++ "A" x y) "A" 0))
Node lhs = d_nodeManager->mkNode(
- kind::STRING_STRIDOF,
+ kind::STRING_INDEXOF,
d_nodeManager->mkNode(kind::STRING_CONCAT, {b, c, a, x, y}),
a,
zero);
kind::PLUS,
two,
d_nodeManager->mkNode(
- kind::STRING_STRIDOF,
+ kind::STRING_INDEXOF,
d_nodeManager->mkNode(kind::STRING_CONCAT, a, x, y),
a,
zero));
// (str.replace (str.replace x "B" x) x "A") -->
// (str.replace (str.replace x "B" "A") x "A")
Node repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, x),
+ kind::STRING_REPLACE,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, x),
x,
a);
Node repl_repl_short = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a),
+ kind::STRING_REPLACE,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, a),
x,
a);
sameNormalForm(repl_repl, repl_repl_short);
// (str.replace "A" (str.replace "B", x, "C") "D") --> "A"
repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
a,
- d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, c),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, c),
d);
sameNormalForm(repl_repl, a);
// (str.replace "A" (str.replace "B", x, "A") "D") -/-> "A"
repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
a,
- d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, a),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, a),
d);
differentNormalForms(repl_repl, a);
//
// (str.replace x (str.++ x y z) z)
Node xyz = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y, z);
- Node repl_x_xyz = d_nodeManager->mkNode(kind::STRING_STRREPL, x, xyz, y);
- Node repl_x_zyx = d_nodeManager->mkNode(kind::STRING_STRREPL, x, xyz, z);
+ Node repl_x_xyz = d_nodeManager->mkNode(kind::STRING_REPLACE, x, xyz, y);
+ Node repl_x_zyx = d_nodeManager->mkNode(kind::STRING_REPLACE, x, xyz, z);
sameNormalForm(repl_x_xyz, repl_x_zyx);
// (str.replace "" (str.++ x x) x) --> ""
Node repl_empty_xx =
- d_nodeManager->mkNode(kind::STRING_STRREPL,
+ d_nodeManager->mkNode(kind::STRING_REPLACE,
empty,
d_nodeManager->mkNode(kind::STRING_CONCAT, x, x),
x);
// (str.replace "AB" (str.++ x "A") x) --> (str.replace "AB" (str.++ x "A")
// "")
Node repl_ab_xa_x =
- d_nodeManager->mkNode(kind::STRING_STRREPL,
+ d_nodeManager->mkNode(kind::STRING_REPLACE,
d_nodeManager->mkNode(kind::STRING_CONCAT, a, b),
d_nodeManager->mkNode(kind::STRING_CONCAT, x, a),
x);
Node repl_ab_xa_e =
- d_nodeManager->mkNode(kind::STRING_STRREPL,
+ d_nodeManager->mkNode(kind::STRING_REPLACE,
d_nodeManager->mkNode(kind::STRING_CONCAT, a, b),
d_nodeManager->mkNode(kind::STRING_CONCAT, x, a),
empty);
// (str.replace "AB" (str.++ x "A") x) -/-> (str.replace "AB" (str.++ "A" x)
// "")
Node repl_ab_ax_e =
- d_nodeManager->mkNode(kind::STRING_STRREPL,
+ d_nodeManager->mkNode(kind::STRING_REPLACE,
d_nodeManager->mkNode(kind::STRING_CONCAT, a, b),
d_nodeManager->mkNode(kind::STRING_CONCAT, a, x),
empty);
// (str.replace "" (str.replace y x "A") y) ---> ""
repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
empty,
- d_nodeManager->mkNode(kind::STRING_STRREPL, y, x, a),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, y, x, a),
y);
sameNormalForm(repl_repl, empty);
// (str.replace "" (str.replace x y x) x) ---> ""
repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
empty,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x),
x);
sameNormalForm(repl_repl, empty);
// (str.replace "" (str.substr x 0 1) x) ---> ""
repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
empty,
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, zero, one),
x);
//
// (str.replace "" x y)
repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
empty,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x),
y);
- Node repl = d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y);
+ Node repl = d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, y);
sameNormalForm(repl_repl, repl);
// Same normal form:
//
// (str.replace "B" x "B"))
repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
b,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b),
b);
- repl = d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, b);
+ repl = d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, b);
sameNormalForm(repl_repl, repl);
// Different normal forms for:
//
// (str.replace "B" x "B")
repl_repl = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
b,
- d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, a),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, a),
b);
- repl = d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, b);
+ repl = d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, b);
differentNormalForms(repl_repl, repl);
{
//
// (str.++ "AB" (str.replace x "C" y))
Node lhs =
- d_nodeManager->mkNode(kind::STRING_STRREPL,
+ d_nodeManager->mkNode(kind::STRING_REPLACE,
d_nodeManager->mkNode(kind::STRING_CONCAT, ab, x),
c,
y);
Node rhs = d_nodeManager->mkNode(
kind::STRING_CONCAT,
ab,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, c, y));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, c, y));
sameNormalForm(lhs, rhs);
}
}
//
// (str.replace "A" (str.substr x 1 4) y z)
Node substr_3 = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
a,
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three),
z);
Node substr_4 = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
a,
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, four),
z);
//
// (str.replace "A" (str.++ y (str.substr x 1 4)) y z)
Node concat_substr_3 = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
a,
d_nodeManager->mkNode(
kind::STRING_CONCAT,
d_nodeManager->mkNode(kind::STRING_SUBSTR, x, one, three)),
z);
Node concat_substr_4 = d_nodeManager->mkNode(
- kind::STRING_STRREPL,
+ kind::STRING_REPLACE,
a,
d_nodeManager->mkNode(
kind::STRING_CONCAT,
// (str.contains "A" (str.++ a (str.replace "B", x, "C")) --> false
Node ctn_repl = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
+ kind::STRING_CONTAINS,
a,
d_nodeManager->mkNode(
kind::STRING_CONCAT,
a,
- d_nodeManager->mkNode(kind::STRING_STRREPL, b, x, c)));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, b, x, c)));
sameNormalForm(ctn_repl, f);
// (str.contains x (str.++ x x)) --> (= x "")
Node x_cnts_x_x = d_nodeManager->mkNode(
- kind::STRING_STRCTN, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, x));
+ kind::STRING_CONTAINS, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, x));
sameNormalForm(x_cnts_x_x, d_nodeManager->mkNode(kind::EQUAL, x, empty));
// Same normal form for:
//
// (and (str.contains (str.++ y x) (str.++ x y)) (= z ""))
Node yx_cnts_xzy = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
+ kind::STRING_CONTAINS,
yx,
d_nodeManager->mkNode(kind::STRING_CONCAT, x, z, y));
Node yx_cnts_xy =
d_nodeManager->mkNode(kind::AND,
d_nodeManager->mkNode(kind::EQUAL, z, empty),
- d_nodeManager->mkNode(kind::STRING_STRCTN, yx, xy));
+ d_nodeManager->mkNode(kind::STRING_CONTAINS, yx, xy));
sameNormalForm(yx_cnts_xzy, yx_cnts_xy);
// Same normal form for:
//
// (= (str.substr x n (str.len y)) y)
Node ctn_substr = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
+ kind::STRING_CONTAINS,
d_nodeManager->mkNode(kind::STRING_SUBSTR,
x,
n,
//
// (str.contains x y)
Node ctn_repl_y_x_y = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
+ kind::STRING_CONTAINS,
x,
- d_nodeManager->mkNode(kind::STRING_STRREPL, y, x, y));
- Node ctn_x_y = d_nodeManager->mkNode(kind::STRING_STRCTN, x, y);
+ d_nodeManager->mkNode(kind::STRING_REPLACE, y, x, y));
+ Node ctn_x_y = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, y);
sameNormalForm(ctn_repl_y_x_y, ctn_repl_y_x_y);
// Same normal form for:
//
// (= x (str.replace x y x))
Node ctn_repl_self = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
+ kind::STRING_CONTAINS,
x,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x));
Node eq_repl = d_nodeManager->mkNode(
- kind::EQUAL, x, d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x));
+ kind::EQUAL, x, d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x));
sameNormalForm(ctn_repl_self, eq_repl);
// (str.contains x (str.++ "A" (str.replace x y x))) ---> false
Node ctn_repl_self_f = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
+ kind::STRING_CONTAINS,
x,
d_nodeManager->mkNode(
kind::STRING_CONCAT,
a,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x)));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x)));
sameNormalForm(ctn_repl_self_f, f);
// Same normal form for:
//
// (= "" (str.replace "" x y))
Node ctn_repl_empty = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
+ kind::STRING_CONTAINS,
x,
- d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, y));
Node eq_repl_empty = d_nodeManager->mkNode(
kind::EQUAL,
empty,
- d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, y));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, y));
sameNormalForm(ctn_repl_empty, eq_repl_empty);
// Same normal form for:
//
// (= "" y)
Node ctn_x_x_y = d_nodeManager->mkNode(
- kind::STRING_STRCTN, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, y));
+ kind::STRING_CONTAINS, x, d_nodeManager->mkNode(kind::STRING_CONCAT, x, y));
Node eq_emp_y = d_nodeManager->mkNode(kind::EQUAL, empty, y);
sameNormalForm(ctn_x_x_y, eq_emp_y);
// (str.contains (str.++ y x) (str.++ x y))
//
// (= (str.++ y x) (str.++ x y))
- Node ctn_yxxy = d_nodeManager->mkNode(kind::STRING_STRCTN, yx, xy);
+ Node ctn_yxxy = d_nodeManager->mkNode(kind::STRING_CONTAINS, yx, xy);
Node eq_yxxy = d_nodeManager->mkNode(kind::EQUAL, yx, xy);
sameNormalForm(ctn_yxxy, eq_yxxy);
// (str.contains (str.replace x y x) x) ---> true
ctn_repl = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x),
x);
sameNormalForm(ctn_repl, t);
// (str.contains (str.replace (str.++ x y) z (str.++ y x)) x) ---> true
ctn_repl = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, xy, z, yx),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, xy, z, yx),
x);
sameNormalForm(ctn_repl, t);
// (str.contains (str.++ z (str.replace (str.++ x y) z (str.++ y x))) x)
// ---> true
ctn_repl = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
+ kind::STRING_CONTAINS,
d_nodeManager->mkNode(
kind::STRING_CONCAT,
z,
- d_nodeManager->mkNode(kind::STRING_STRREPL, xy, z, yx)),
+ d_nodeManager->mkNode(kind::STRING_REPLACE, xy, z, yx)),
x);
sameNormalForm(ctn_repl, t);
//
// (str.contains x y)
Node lhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x),
y);
- Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, y);
+ Node rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, y);
sameNormalForm(lhs, rhs);
// Same normal form for:
//
// (str.contains x "B")
lhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x),
b);
- rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, b);
+ rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, b);
sameNormalForm(lhs, rhs);
// Same normal form for:
// (str.contains x (str.substr z n 1))
Node substr_z = d_nodeManager->mkNode(kind::STRING_SUBSTR, z, n, one);
lhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, x),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, x),
substr_z);
- rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, substr_z);
+ rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, substr_z);
sameNormalForm(lhs, rhs);
// Same normal form for:
//
// (str.contains (str.replace x z y) y)
lhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, z),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, z),
z);
rhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, z, y),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, z, y),
y);
sameNormalForm(lhs, rhs);
//
// (str.contains (str.replace x "A" "") "A")
lhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b),
a);
rhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, empty),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, empty),
a);
sameNormalForm(lhs, rhs);
{
// (str.contains (str.++ x "A") (str.++ "B" x)) ---> false
Node ctn =
- d_nodeManager->mkNode(kind::STRING_STRCTN,
+ d_nodeManager->mkNode(kind::STRING_CONTAINS,
d_nodeManager->mkNode(kind::STRING_CONCAT, x, a),
d_nodeManager->mkNode(kind::STRING_CONCAT, b, x));
sameNormalForm(ctn, f);
//
// (str.contains x "GHI")
lhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, abc, def),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, abc, def),
ghi);
- rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, ghi);
+ rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, ghi);
sameNormalForm(lhs, rhs);
}
//
// (str.contains x "B")
lhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, abc, def),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, abc, def),
b);
- rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, b);
+ rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, b);
differentNormalForms(lhs, rhs);
}
//
// (str.contains x "ABC")
lhs = d_nodeManager->mkNode(
- kind::STRING_STRCTN,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, def),
+ kind::STRING_CONTAINS,
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, def),
abc);
- rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc);
+ rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, abc);
differentNormalForms(lhs, rhs);
}
// (or (= x "")
// (= x "A") (= x "B") (= x "C"))
Node cat = d_nodeManager->mkNode(kind::STRING_CHARAT, x, n);
- lhs = d_nodeManager->mkNode(kind::STRING_STRCTN, abc, cat);
+ lhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, abc, cat);
rhs = d_nodeManager->mkNode(kind::OR,
{d_nodeManager->mkNode(kind::EQUAL, cat, empty),
d_nodeManager->mkNode(kind::EQUAL, cat, a),
// inferEqsFromContains((str.replace x "B" "A"), x) returns something
// equivalent to (= (str.replace x "B" "A") x)
- Node repl = d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a);
+ Node repl = d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, a);
Node eq_repl_x = d_nodeManager->mkNode(kind::EQUAL, repl, x);
sameNormalForm(StringsEntail::inferEqsFromContains(repl, x), eq_repl_x);
Node empty_repl = d_nodeManager->mkNode(
kind::EQUAL,
empty,
- d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, b));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, empty, x, b));
Node empty_x = d_nodeManager->mkNode(
kind::NOT, d_nodeManager->mkNode(kind::EQUAL, x, empty));
sameNormalForm(empty_repl, empty_x);
Node empty_repl_xaa = d_nodeManager->mkNode(
kind::EQUAL,
empty,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, y, xxa));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, y, xxa));
Node empty_xy = d_nodeManager->mkNode(
kind::AND,
d_nodeManager->mkNode(kind::EQUAL, x, empty),
Node empty_repl_xxaxy = d_nodeManager->mkNode(
kind::EQUAL,
empty,
- d_nodeManager->mkNode(kind::STRING_STRREPL, xxa, x, y));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, xxa, x, y));
Node eq_xxa_repl = d_nodeManager->mkNode(
kind::EQUAL,
xxa,
- d_nodeManager->mkNode(kind::STRING_STRREPL, empty, y, x));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, empty, y, x));
sameNormalForm(empty_repl_xxaxy, f);
// Same normal form for:
//
// (= "A" (str.replace "" y x))
Node empty_repl_axy = d_nodeManager->mkNode(
- kind::EQUAL, empty, d_nodeManager->mkNode(kind::STRING_STRREPL, a, x, y));
+ kind::EQUAL, empty, d_nodeManager->mkNode(kind::STRING_REPLACE, a, x, y));
Node eq_a_repl = d_nodeManager->mkNode(
- kind::EQUAL, a, d_nodeManager->mkNode(kind::STRING_STRREPL, empty, y, x));
+ kind::EQUAL, a, d_nodeManager->mkNode(kind::STRING_REPLACE, empty, y, x));
sameNormalForm(empty_repl_axy, eq_a_repl);
// Same normal form for:
Node empty_repl_a = d_nodeManager->mkNode(
kind::EQUAL,
empty,
- d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, empty));
+ d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, empty));
Node prefix_a = d_nodeManager->mkNode(kind::STRING_PREFIX, x, a);
sameNormalForm(empty_repl_a, prefix_a);
//
// (= (str.++ x x a) y)
Node eq_xxa_repl_y = d_nodeManager->mkNode(
- kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_STRREPL, y, xxa, y));
+ kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_REPLACE, y, xxa, y));
Node eq_xxa_y = d_nodeManager->mkNode(kind::EQUAL, xxa, y);
sameNormalForm(eq_xxa_repl_y, eq_xxa_y);
// (= (str.++ x x a) (str.replace (str.++ x x a) "A" "B")) ---> false
Node eq_xxa_repl_xxa = d_nodeManager->mkNode(
- kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_STRREPL, xxa, a, b));
+ kind::EQUAL, xxa, d_nodeManager->mkNode(kind::STRING_REPLACE, xxa, a, b));
sameNormalForm(eq_xxa_repl_xxa, f);
// Same normal form for:
//
// (= x "")
Node eq_repl = d_nodeManager->mkNode(
- kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b), empty);
+ kind::EQUAL, d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b), empty);
Node eq_x = d_nodeManager->mkNode(kind::EQUAL, x, empty);
sameNormalForm(eq_repl, eq_x);
//
// (= (str.replace y "B" "A") "A")
Node lhs = d_nodeManager->mkNode(
- kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b), b);
+ kind::EQUAL, d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b), b);
Node rhs = d_nodeManager->mkNode(
- kind::EQUAL, d_nodeManager->mkNode(kind::STRING_STRREPL, x, b, a), a);
+ kind::EQUAL, d_nodeManager->mkNode(kind::STRING_REPLACE, x, b, a), a);
sameNormalForm(lhs, rhs);
}
}
{
- Node xrepl = d_nodeManager->mkNode(kind::STRING_STRREPL, x, a, b);
+ Node xrepl = d_nodeManager->mkNode(kind::STRING_REPLACE, x, a, b);
// Same normal form for:
//
x,
d_nodeManager->mkNode(kind::REGEXP_CONCAT,
{sig_star, sig_star, re_abc, sig_star}));
- Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc);
+ Node rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, abc);
sameNormalForm(lhs, rhs);
}
kind::STRING_IN_REGEXP,
x,
d_nodeManager->mkNode(kind::REGEXP_CONCAT, sig_star, re_abc));
- Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc);
+ Node rhs = d_nodeManager->mkNode(kind::STRING_CONTAINS, x, abc);
differentNormalForms(lhs, rhs);
}
}
kind::STRING_SUBSTR,
a,
zero,
- d_nodeManager->mkNode(kind::STRING_STRIDOF, a, b, zero));
+ d_nodeManager->mkNode(kind::STRING_INDEXOF, a, b, zero));
Node sc = d_nodeManager->mkNode(kind::STRING_SUBSTR, c, zero, n);
SkolemCache sk;
projects / cvc5.git / commitdiff