From: Andrew Reynolds Date: Mon, 28 Jun 2021 20:45:51 +0000 (-0500) Subject: Rename internal string kinds to match API (#6797) X-Git-Tag: cvc5-1.0.0~1551 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ca7aa981af4c6229746aa0c1b3f3f67ddb68b23;p=cvc5.git Rename internal string kinds to match API (#6797) This commit replaces (old) internal string kind names to match the API / smt2 standard names. --- 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 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 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::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() ? 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(); @@ -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" -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" typerule STRING_REPLACE_RE_ALL "SimpleTypeRule" 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()) { - 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()) { - 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().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 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 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 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()) { - 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()) { 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& 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().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;