summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-06-28 15:45:51 -0500
committerGitHub <noreply@github.com>2021-06-28 20:45:51 +0000
commit8ca7aa981af4c6229746aa0c1b3f3f67ddb68b23 (patch)
tree7c354da7ce9d0023565fcbbae83bde222da53dea
parent43fffe772a89537dfecea7e63352a03b922a0fbc (diff)
Rename internal string kinds to match API (#6797)
This commit replaces (old) internal string kind names to match the API / smt2 standard names.
Diffstat
-rw-r--r--src/api/cpp/cvc5.cpp32
-rw-r--r--src/printer/smt2/smt2_printer.cpp16
-rw-r--r--src/theory/datatypes/sygus_extension.cpp4
-rw-r--r--src/theory/evaluator.cpp6
-rw-r--r--src/theory/quantifiers/sygus/sygus_invariance.cpp2
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_io.cpp2
-rw-r--r--src/theory/quantifiers/term_util.cpp4
-rw-r--r--src/theory/strings/arith_entail.cpp4
-rw-r--r--src/theory/strings/extf_solver.cpp24
-rw-r--r--src/theory/strings/kinds16
-rw-r--r--src/theory/strings/regexp_elim.cpp2
-rw-r--r--src/theory/strings/sequences_rewriter.cpp123
-rw-r--r--src/theory/strings/skolem_cache.cpp2
-rw-r--r--src/theory/strings/strings_entail.cpp10
-rw-r--r--src/theory/strings/term_registry.cpp16
-rw-r--r--src/theory/strings/theory_strings.cpp10
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp20
-rw-r--r--src/theory/strings/theory_strings_utils.cpp4
-rw-r--r--src/theory/subs_minimize.cpp4
-rw-r--r--test/unit/theory/evaluator_white.cpp8
-rw-r--r--test/unit/theory/sequences_rewriter_white.cpp240
-rw-r--r--test/unit/theory/theory_strings_skolem_cache_black.cpp2
22 files changed, 276 insertions, 275 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0228f6045..5a34f1453 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -312,11 +312,11 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
{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},
@@ -352,10 +352,10 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
{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},
@@ -620,11 +620,11 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
{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},
@@ -3208,10 +3208,10 @@ Kind Term::getKindHelper() const
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;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9f19acaab..28139400b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -720,11 +720,11 @@ void Smt2Printer::toStream(std::ostream& out,
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:
@@ -1329,12 +1329,12 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
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";
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 45d996b55..ee96b95d8 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -764,12 +764,12 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
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);
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 07a4e4b85..2a274426f 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -572,7 +572,7 @@ EvalResult Evaluator::evalInternal(
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;
@@ -580,7 +580,7 @@ EvalResult Evaluator::evalInternal(
break;
}
- case kind::STRING_STRIDOF:
+ case kind::STRING_INDEXOF:
{
const String& s = results[currNode[0]].d_str;
Integer s_len(s.size());
@@ -606,7 +606,7 @@ EvalResult Evaluator::evalInternal(
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;
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 78f5c49e6..cb7e2b84e 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -221,7 +221,7 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
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())
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 4cf0e6bb4..8c8f5ccd4 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -952,7 +952,7 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude(
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)
{
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 746cc7f11..c9fced3be 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -533,7 +533,7 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
return mkTypeValue(NodeManager::currentNM()->stringType(), 0);
}
}
- else if (ik == STRING_STRIDOF)
+ else if (ik == STRING_INDEXOF)
{
if (arg == 0 || arg == 1)
{
@@ -564,7 +564,7 @@ Node TermUtil::isSingularArg(Node n, Kind ik, unsigned arg)
{
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);
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp
index 66e3cf634..6a0eea41a 100644
--- a/src/theory/strings/arith_entail.cpp
+++ b/src/theory/strings/arith_entail.cpp
@@ -435,7 +435,7 @@ void ArithEntail::getArithApproximations(Node a,
}
}
}
- 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 ) )
@@ -506,7 +506,7 @@ void ArithEntail::getArithApproximations(Node a,
}
}
}
- else if (ak == STRING_STRIDOF)
+ else if (ak == STRING_INDEXOF)
{
// over,under-approximations for indexof( x, y, n )
if (isOverApprox)
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index fc8fb15b0..98f7d7d7c 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -52,15 +52,15 @@ ExtfSolver::ExtfSolver(SolverState& s,
{
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);
@@ -101,7 +101,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
{
pol = d_extfInfoTmp[n].d_const.getConst<bool>() ? 1 : -1;
}
- if (k == STRING_STRCTN)
+ if (k == STRING_CONTAINS)
{
if (pol == 1)
{
@@ -167,7 +167,7 @@ bool ExtfSolver::doReduction(int effort, Node n)
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];
@@ -191,9 +191,9 @@ bool ExtfSolver::doReduction(int effort, Node n)
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);
@@ -509,7 +509,7 @@ void ExtfSolver::checkExtfInference(Node n,
// 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>();
@@ -539,7 +539,7 @@ void ExtfSolver::checkExtfInference(Node n,
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))
@@ -600,7 +600,7 @@ void ExtfSolver::checkExtfInference(Node n,
{
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).
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 743a5c006..aa95ef2f8 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -18,13 +18,13 @@ operator STRING_LENGTH 1 "string length"
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"
@@ -149,11 +149,11 @@ typerule STRING_LENGTH ::cvc5::theory::strings::StringStrToIntTypeRule
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
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 45b1f62fb..18a5b049a 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -264,7 +264,7 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
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);
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index f63b416ff..423209122 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -293,7 +293,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
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])
@@ -351,7 +351,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
// ------- 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];
@@ -360,7 +360,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
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);
}
@@ -377,7 +377,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node)
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);
}
}
@@ -581,7 +581,7 @@ Node SequencesRewriter::rewriteLength(Node node)
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]));
@@ -1288,7 +1288,7 @@ Node SequencesRewriter::rewriteMembership(TNode node)
&& 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);
}
}
@@ -1454,11 +1454,11 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node)
{
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);
}
@@ -1466,11 +1466,11 @@ RewriteResponse SequencesRewriter::postRewrite(TNode 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);
}
@@ -1735,7 +1735,7 @@ Node SequencesRewriter::rewriteSubstr(Node 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)
@@ -1746,7 +1746,7 @@ Node SequencesRewriter::rewriteSubstr(Node node)
&& 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]);
@@ -1958,7 +1958,7 @@ Node SequencesRewriter::rewriteUpdate(Node node)
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])
@@ -2040,23 +2040,23 @@ Node SequencesRewriter::rewriteContains(Node node)
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" ) --->
@@ -2088,13 +2088,13 @@ Node SequencesRewriter::rewriteContains(Node node)
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
@@ -2202,10 +2202,10 @@ Node SequencesRewriter::rewriteContains(Node node)
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);
@@ -2226,7 +2226,7 @@ Node SequencesRewriter::rewriteContains(Node node)
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())
{
@@ -2235,7 +2235,7 @@ Node SequencesRewriter::rewriteContains(Node node)
{
// (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);
}
}
@@ -2245,7 +2245,7 @@ Node SequencesRewriter::rewriteContains(Node node)
// (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);
}
@@ -2253,7 +2253,7 @@ Node SequencesRewriter::rewriteContains(Node node)
// 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);
}
}
@@ -2262,9 +2262,10 @@ Node SequencesRewriter::rewriteContains(Node node)
// (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);
}
@@ -2278,21 +2279,21 @@ Node SequencesRewriter::rewriteContains(Node node)
{
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);
}
@@ -2315,7 +2316,7 @@ Node SequencesRewriter::rewriteContains(Node node)
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)
@@ -2381,7 +2382,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
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);
}
}
@@ -2438,7 +2439,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
// 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);
}
@@ -2451,7 +2452,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
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]));
@@ -2479,7 +2480,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
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);
}
}
@@ -2511,7 +2512,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
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);
}
}
@@ -2524,7 +2525,7 @@ Node SequencesRewriter::rewriteIndexof(Node node)
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);
@@ -2589,7 +2590,7 @@ Node SequencesRewriter::rewriteIndexofRe(Node node)
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]))
@@ -2671,7 +2672,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
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);
}
}
@@ -2683,7 +2684,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
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())
{
@@ -2717,7 +2718,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
// 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]));
@@ -2773,14 +2774,14 @@ Node SequencesRewriter::rewriteReplace(Node node)
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);
}
}
@@ -2801,7 +2802,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
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]));
@@ -2845,7 +2846,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
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]);
@@ -2853,7 +2854,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
}
}
- if (node[0].getKind() == STRING_STRREPL)
+ if (node[0].getKind() == STRING_REPLACE)
{
Node x = node[0];
Node y = node[1];
@@ -2893,8 +2894,8 @@ Node SequencesRewriter::rewriteReplace(Node node)
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);
@@ -2903,7 +2904,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
}
}
- if (node[1].getKind() == STRING_STRREPL)
+ if (node[1].getKind() == STRING_REPLACE)
{
if (node[1][0] == node[0])
{
@@ -2941,7 +2942,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
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);
@@ -2979,11 +2980,11 @@ Node SequencesRewriter::rewriteReplace(Node node)
}
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])
{
@@ -2993,7 +2994,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
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);
}
}
@@ -3053,7 +3054,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
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
@@ -3076,7 +3077,7 @@ Node SequencesRewriter::rewriteReplace(Node node)
Node SequencesRewriter::rewriteReplaceAll(Node node)
{
- Assert(node.getKind() == STRING_STRREPLALL);
+ Assert(node.getKind() == STRING_REPLACE_ALL);
TypeNode stype = node.getType();
@@ -3129,7 +3130,7 @@ Node SequencesRewriter::rewriteReplaceAll(Node node)
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])
{
@@ -3139,7 +3140,7 @@ Node SequencesRewriter::rewriteReplaceInternal(Node node)
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);
}
@@ -3347,7 +3348,7 @@ Node SequencesRewriter::rewritePrefixSuffix(Node n)
// (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);
}
}
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp
index 913518bc8..34cb45455 100644
--- a/src/theory/strings/skolem_cache.cpp
+++ b/src/theory/strings/skolem_cache.cpp
@@ -257,7 +257,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b)
{
// 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)
diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp
index a527d99dc..3fa11cc24 100644
--- a/src/theory/strings/strings_entail.cpp
+++ b/src/theory/strings/strings_entail.cpp
@@ -471,7 +471,7 @@ bool StringsEntail::componentContainsBase(
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
@@ -675,7 +675,7 @@ bool StringsEntail::stripConstantEndpoints(std::vector<Node>& n1,
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)
{
@@ -688,7 +688,7 @@ Node StringsEntail::checkContains(Node a, Node b, bool 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());
@@ -839,7 +839,7 @@ Node StringsEntail::getMultisetApproximation(Node a)
{
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]));
}
@@ -865,7 +865,7 @@ Node StringsEntail::getStringOrEmpty(Node n)
{
switch (n.getKind())
{
- case STRING_STRREPL:
+ case STRING_REPLACE:
{
if (Word::isEmpty(n[0]))
{
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 8c5805b37..1b77308d7 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -88,7 +88,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
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))
@@ -107,7 +107,7 @@ Node TermRegistry::eagerReduce(Node t, SkolemCache* sc)
// (>= (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 =
@@ -148,10 +148,10 @@ void TermRegistry::preRegisterTerm(TNode n)
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)
{
@@ -230,7 +230,7 @@ void TermRegistry::preRegisterTerm(TNode n)
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);
@@ -310,7 +310,7 @@ void TermRegistry::registerTerm(Node n, int effort)
// 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);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index f0763e153..8de43fd55 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -126,19 +126,19 @@ void TheoryStrings::finishInit()
// `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);
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index dbb6d4cf3..5f21d6e65 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -183,7 +183,7 @@ Node StringsPreprocess::reduce(Node t,
// 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];
@@ -205,7 +205,7 @@ Node StringsPreprocess::reduce(Node t,
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
@@ -225,7 +225,7 @@ Node StringsPreprocess::reduce(Node t,
// ~contains( str.++( io2, substr( y, 0, len( y ) - 1) ), y )
Node c32 =
nm->mkNode(
- STRING_STRCTN,
+ STRING_CONTAINS,
nm->mkNode(
STRING_CONCAT,
io2,
@@ -541,7 +541,7 @@ Node StringsPreprocess::reduce(Node t,
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];
@@ -561,14 +561,14 @@ Node StringsPreprocess::reduce(Node t,
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,
@@ -602,7 +602,7 @@ Node StringsPreprocess::reduce(Node t,
// 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];
@@ -629,7 +629,7 @@ Node StringsPreprocess::reduce(Node t,
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);
@@ -637,7 +637,7 @@ Node StringsPreprocess::reduce(Node t,
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)),
@@ -932,7 +932,7 @@ Node StringsPreprocess::reduce(Node t,
// 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];
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index c763557ca..cfe126ef3 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -383,8 +383,8 @@ TypeNode getOwnerStringType(Node n)
{
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
diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index 02fa85faa..2ec945963 100644
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -447,7 +447,7 @@ bool SubstitutionMinimize::isSingularArg(Node n, Kind k, unsigned arg)
}
}
- 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)
@@ -455,7 +455,7 @@ bool SubstitutionMinimize::isSingularArg(Node n, Kind k, unsigned arg)
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)
diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp
index 25ffa0572..a1f56eaba 100644
--- a/test/unit/theory/evaluator_white.cpp
+++ b/test/unit/theory/evaluator_white.cpp
@@ -109,25 +109,25 @@ TEST_F(TestTheoryWhiteEvaluator, strIdOf)
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));
}
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index c5a5924d4..77671dc34 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -296,11 +296,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
// (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));
@@ -313,11 +313,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
// (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);
@@ -335,11 +335,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
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);
@@ -380,7 +380,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat)
// (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);
@@ -393,7 +393,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat)
// (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);
@@ -419,7 +419,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat)
// "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(
@@ -454,7 +454,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite)
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);
@@ -486,9 +486,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
// (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);
@@ -498,12 +498,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
//
// (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);
@@ -511,7 +511,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
// (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);
@@ -524,7 +524,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
//
// (+ 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);
@@ -532,7 +532,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
kind::PLUS,
two,
d_nodeManager->mkNode(
- kind::STRING_STRIDOF,
+ kind::STRING_INDEXOF,
d_nodeManager->mkNode(kind::STRING_CONCAT, a, x, y),
a,
zero));
@@ -561,30 +561,30 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
// (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);
@@ -594,13 +594,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
//
// (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);
@@ -609,12 +609,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
// (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);
@@ -623,7 +623,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
// (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);
@@ -631,23 +631,23 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
// (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);
@@ -659,11 +659,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
//
// (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:
@@ -672,11 +672,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
//
// (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:
@@ -685,11 +685,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
//
// (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);
{
@@ -699,14 +699,14 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
//
// (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);
}
}
@@ -988,12 +988,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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);
@@ -1005,7 +1005,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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,
@@ -1013,7 +1013,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
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,
@@ -1024,17 +1024,17 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
// (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:
@@ -1043,13 +1043,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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:
@@ -1058,7 +1058,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (= (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,
@@ -1079,10 +1079,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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:
@@ -1091,21 +1091,21 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (= 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:
@@ -1114,13 +1114,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (= "" (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:
@@ -1129,7 +1129,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (= "" 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);
@@ -1138,32 +1138,32 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
// (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);
@@ -1173,10 +1173,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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:
@@ -1185,10 +1185,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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:
@@ -1198,10 +1198,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
// (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:
@@ -1210,12 +1210,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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);
@@ -1225,19 +1225,19 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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);
@@ -1250,10 +1250,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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);
}
@@ -1264,10 +1264,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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);
}
@@ -1278,10 +1278,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
//
// (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);
}
@@ -1293,7 +1293,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
// (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),
@@ -1337,7 +1337,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains)
// 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);
@@ -1412,7 +1412,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
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);
@@ -1425,7 +1425,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
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),
@@ -1437,11 +1437,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
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:
@@ -1450,9 +1450,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
//
// (= "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:
@@ -1463,7 +1463,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
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);
@@ -1509,13 +1509,13 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
//
// (= (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:
@@ -1524,7 +1524,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
//
// (= 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);
@@ -1535,9 +1535,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
//
// (= (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);
}
@@ -1644,7 +1644,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
}
{
- 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:
//
@@ -1805,7 +1805,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership)
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);
}
@@ -1822,7 +1822,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership)
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);
}
}
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp
index 24cbd166e..62de21797 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.cpp
+++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp
@@ -43,7 +43,7 @@ TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback