From 68d6329d38af159afa7dc9542ef8e04e4d5a3773 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 9 Nov 2021 16:36:33 -0800 Subject: sets: Rename set.intersection to set.inter. (#7622) This further renames kind SET_INTERSECTION to SET_INTER. --- src/api/cpp/cvc5.cpp | 4 ++-- src/api/cpp/cvc5_kind.h | 2 +- src/parser/smt2/smt2.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 2 +- .../quantifiers/ematching/trigger_term_info.cpp | 2 +- src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 2 +- src/theory/quantifiers/term_database.cpp | 2 +- src/theory/quantifiers/term_util.cpp | 8 ++++---- src/theory/sep/theory_sep.cpp | 20 +++++++++----------- src/theory/sets/cardinality_extension.cpp | 18 +++++++++--------- src/theory/sets/kinds | 4 ++-- src/theory/sets/solver_state.cpp | 2 +- src/theory/sets/term_registry.cpp | 2 +- src/theory/sets/theory_sets.cpp | 2 +- src/theory/sets/theory_sets_private.cpp | 4 ++-- src/theory/sets/theory_sets_rewriter.cpp | 10 +++++----- src/theory/sets/theory_sets_type_rules.cpp | 4 ++-- 17 files changed, 44 insertions(+), 46 deletions(-) (limited to 'src') diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 797d2e473..ae0ee2ceb 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -275,7 +275,7 @@ const static std::unordered_map s_kinds{ /* Sets ---------------------------------------------------------------- */ {SET_EMPTY, cvc5::Kind::SET_EMPTY}, {SET_UNION, cvc5::Kind::SET_UNION}, - {SET_INTERSECTION, cvc5::Kind::SET_INTERSECTION}, + {SET_INTER, cvc5::Kind::SET_INTER}, {SET_MINUS, cvc5::Kind::SET_MINUS}, {SET_SUBSET, cvc5::Kind::SET_SUBSET}, {SET_MEMBER, cvc5::Kind::SET_MEMBER}, @@ -585,7 +585,7 @@ const static std::unordered_map /* Sets ------------------------------------------------------------ */ {cvc5::Kind::SET_EMPTY, SET_EMPTY}, {cvc5::Kind::SET_UNION, SET_UNION}, - {cvc5::Kind::SET_INTERSECTION, SET_INTERSECTION}, + {cvc5::Kind::SET_INTER, SET_INTER}, {cvc5::Kind::SET_MINUS, SET_MINUS}, {cvc5::Kind::SET_SUBSET, SET_SUBSET}, {cvc5::Kind::SET_MEMBER, SET_MEMBER}, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 162ec24e7..90a57317d 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -2139,7 +2139,7 @@ enum Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - SET_INTERSECTION, + SET_INTER, /** * Set subtraction. * diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 7add605c5..ef784746c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -594,7 +594,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) d_solver->mkUniverseSet(d_solver->getBooleanSort())); addOperator(api::SET_UNION, "set.union"); - addOperator(api::SET_INTERSECTION, "set.intersection"); + addOperator(api::SET_INTER, "set.inter"); addOperator(api::SET_MINUS, "set.minus"); addOperator(api::SET_SUBSET, "set.subset"); addOperator(api::SET_MEMBER, "set.member"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5d4387658..8ed4929e5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1061,7 +1061,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) // set theory case kind::SET_UNION: return "set.union"; - case kind::SET_INTERSECTION: return "set.intersection"; + case kind::SET_INTER: return "set.inter"; case kind::SET_MINUS: return "set.minus"; case kind::SET_SUBSET: return "set.subset"; case kind::SET_MEMBER: return "set.member"; diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 75a353dbe..24efc60c3 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -54,7 +54,7 @@ bool TriggerTermInfo::isAtomicTriggerKind(Kind k) // where these two things require those kinds respectively. return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR || k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL - || k == APPLY_TESTER || k == SET_UNION || k == SET_INTERSECTION + || k == APPLY_TESTER || k == SET_UNION || k == SET_INTER || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER || k == SET_SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY || k == STRING_LENGTH diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 034f5f23c..99170427e 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -990,7 +990,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdts[i].addConstructor(lambda, "singleton", cargsSingleton); // add for union, difference, intersection - std::vector bin_kinds = {SET_UNION, SET_INTERSECTION, SET_MINUS}; + std::vector bin_kinds = {SET_UNION, SET_INTER, SET_MINUS}; std::vector cargsBinary; cargsBinary.push_back(unres_t); cargsBinary.push_back(unres_t); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5c9e91d32..0408d27da 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -186,7 +186,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) Node TermDb::getMatchOperator( Node n ) { Kind k = n.getKind(); //datatype operators may be parametric, always assume they are - if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTERSECTION + if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTER || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER || k == SET_SINGLETON || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR || k == APPLY_TESTER || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index de4c56552..704951f52 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -283,7 +283,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) { if (reqNAry) { - if (k == SET_UNION || k == SET_INTERSECTION) + if (k == SET_UNION || k == SET_INTER) { return false; } @@ -292,7 +292,7 @@ bool TermUtil::isAssoc(Kind k, bool reqNAry) || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR || k == BITVECTOR_XNOR || k == BITVECTOR_CONCAT || k == STRING_CONCAT - || k == SET_UNION || k == SET_INTERSECTION || k == RELATION_JOIN + || k == SET_UNION || k == SET_INTER || k == RELATION_JOIN || k == RELATION_PRODUCT || k == SEP_STAR; } @@ -300,7 +300,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) { if (reqNAry) { - if (k == SET_UNION || k == SET_INTERSECTION) + if (k == SET_UNION || k == SET_INTER) { return false; } @@ -308,7 +308,7 @@ bool TermUtil::isComm(Kind k, bool reqNAry) return k == EQUAL || k == PLUS || k == MULT || k == NONLINEAR_MULT || k == AND || k == OR || k == XOR || k == BITVECTOR_ADD || k == BITVECTOR_MULT || k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_XOR - || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTERSECTION + || k == BITVECTOR_XNOR || k == SET_UNION || k == SET_INTER || k == SEP_STAR; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 218c09804..3ee4fa012 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -385,7 +385,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) { for (size_t j = (i + 1); j < lsize; j++) { - Node s = nm->mkNode(SET_INTERSECTION, labels[i], labels[j]); + Node s = nm->mkNode(SET_INTER, labels[i], labels[j]); Node ilem = s.eqNode(empSet); Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, disjoint : " << ilem @@ -401,7 +401,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, union : " << ulem << std::endl; c_lems.push_back(ulem); - Node s = nm->mkNode(SET_INTERSECTION, slbl, labels[0]); + Node s = nm->mkNode(SET_INTER, slbl, labels[0]); Node ilem = s.eqNode(empSet); Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl; @@ -1427,10 +1427,9 @@ Node TheorySep::instantiateLabel(Node n, Node sub_lbl = itl->second; Node lbl_mval = d_label_model[sub_lbl].getValue( rtn ); for( unsigned j=0; jmkNode(kind::SET_INTERSECTION, lbl_mval, vs[j]) - .eqNode(empSet)); + bchildren.push_back(NodeManager::currentNM() + ->mkNode(kind::SET_INTER, lbl_mval, vs[j]) + .eqNode(empSet)); } vs.push_back( lbl_mval ); if( vsu.isNull() ){ @@ -1476,11 +1475,10 @@ Node TheorySep::instantiateLabel(Node n, //disjoint constraints Node sub_lbl_0 = d_label_map[n][lbl][0]; Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn ); - wchildren.push_back( - NodeManager::currentNM() - ->mkNode(kind::SET_INTERSECTION, lbl_mval_0, lbl) - .eqNode(empSet) - .negate()); + wchildren.push_back(NodeManager::currentNM() + ->mkNode(kind::SET_INTER, lbl_mval_0, lbl) + .eqNode(empSet) + .negate()); //return the lemma wchildren.push_back( children[0].negate() ); diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index f65c41b53..c35eaf49a 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -242,7 +242,7 @@ void CardinalityExtension::checkRegister() // if setminus, do for intersection instead if (n.getKind() == SET_MINUS) { - n = rewrite(nm->mkNode(SET_INTERSECTION, n[0], n[1])); + n = rewrite(nm->mkNode(SET_INTER, n[0], n[1])); } registerCardinalityTerm(n); } @@ -268,7 +268,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n) NodeManager* nm = NodeManager::currentNM(); Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl; std::vector cterms; - if (n.getKind() == SET_INTERSECTION) + if (n.getKind() == SET_INTER) { for (unsigned e = 0; e < 2; e++) { @@ -381,7 +381,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, for (const Node& n : nvsets) { Kind nk = n.getKind(); - if (nk != SET_INTERSECTION && nk != SET_MINUS) + if (nk != SET_INTER && nk != SET_MINUS) { continue; } @@ -389,7 +389,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, << std::endl; std::vector sib; unsigned true_sib = 0; - if (n.getKind() == SET_INTERSECTION) + if (n.getKind() == SET_INTER) { d_localBase[n] = n; for (unsigned e = 0; e < 2; e++) @@ -401,7 +401,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, } else { - Node si = rewrite(nm->mkNode(SET_INTERSECTION, n[0], n[1])); + Node si = rewrite(nm->mkNode(SET_INTER, n[0], n[1])); sib.push_back(si); d_localBase[n] = si; Node osm = rewrite(nm->mkNode(SET_MINUS, n[1], n[0])); @@ -490,7 +490,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, << "Sibling " << sib[si] << " is already empty." << std::endl; } } - if (!is_union && nk == SET_INTERSECTION && !u.isNull()) + if (!is_union && nk == SET_INTER && !u.isNull()) { // union is equal to other parent if (!d_state.areEqual(u, n[1 - e])) @@ -578,7 +578,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, << " are equal, ids = " << card_parent_ids[l] << " " << card_parent_ids[k] << std::endl; dup = true; - if (n.getKind() != SET_INTERSECTION) + if (n.getKind() != SET_INTER) { continue; } @@ -817,7 +817,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, Node r1 = e == 0 ? o0 : o1; Node r2 = e == 0 ? o1 : o0; // check if their intersection exists modulo equality - Node r1r2i = d_state.getBinaryOpTerm(SET_INTERSECTION, r1, r2); + Node r1r2i = d_state.getBinaryOpTerm(SET_INTER, r1, r2); if (!r1r2i.isNull()) { Trace("sets-nf-debug") @@ -838,7 +838,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, Assert(o0 != o1); Node kca = d_treg.getProxy(o0); Node kcb = d_treg.getProxy(o1); - Node intro = rewrite(nm->mkNode(SET_INTERSECTION, kca, kcb)); + Node intro = rewrite(nm->mkNode(SET_INTER, kca, kcb)); Trace("sets-nf") << " Intro split : " << o0 << " against " << o1 << ", term is " << intro << std::endl; intro_sets.push_back(intro); diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index f5ed7cd87..71d5fce4a 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -37,7 +37,7 @@ enumerator SET_TYPE \ # operators operator SET_UNION 2 "set union" -operator SET_INTERSECTION 2 "set intersection" +operator SET_INTER 2 "set intersection" operator SET_MINUS 2 "set subtraction" operator SET_SUBSET 2 "subset predicate; first parameter a subset of second" operator SET_MEMBER 2 "set membership predicate; first parameter a member of second" @@ -88,7 +88,7 @@ operator RELATION_JOIN_IMAGE 2 "relation join image" operator RELATION_IDEN 1 "relation identity" typerule SET_UNION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule -typerule SET_INTERSECTION ::cvc5::theory::sets::SetsBinaryOperatorTypeRule +typerule SET_INTER ::cvc5::theory::sets::SetsBinaryOperatorTypeRule typerule SET_MINUS ::cvc5::theory::sets::SetsBinaryOperatorTypeRule typerule SET_SUBSET ::cvc5::theory::sets::SubsetTypeRule typerule SET_MEMBER ::cvc5::theory::sets::MemberTypeRule diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp index 023a8a6af..3f619dcad 100644 --- a/src/theory/sets/solver_state.cpp +++ b/src/theory/sets/solver_state.cpp @@ -90,7 +90,7 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n) } } } - else if (nk == SET_SINGLETON || nk == SET_UNION || nk == SET_INTERSECTION + else if (nk == SET_SINGLETON || nk == SET_UNION || nk == SET_INTER || nk == SET_MINUS || nk == SET_EMPTY || nk == SET_UNIVERSE) { if (nk == SET_SINGLETON) diff --git a/src/theory/sets/term_registry.cpp b/src/theory/sets/term_registry.cpp index 41fe0b4c8..d4b5aa824 100644 --- a/src/theory/sets/term_registry.cpp +++ b/src/theory/sets/term_registry.cpp @@ -44,7 +44,7 @@ TermRegistry::TermRegistry(Env& env, Node TermRegistry::getProxy(Node n) { Kind nk = n.getKind(); - if (nk != SET_EMPTY && nk != SET_SINGLETON && nk != SET_INTERSECTION + if (nk != SET_EMPTY && nk != SET_SINGLETON && nk != SET_INTER && nk != SET_MINUS && nk != SET_UNION && nk != SET_UNIVERSE) { return n; diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index b2eb80f75..c3d0b9bbe 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -76,7 +76,7 @@ void TheorySets::finishInit() // functions we are doing congruence over d_equalityEngine->addFunctionKind(SET_SINGLETON); d_equalityEngine->addFunctionKind(SET_UNION); - d_equalityEngine->addFunctionKind(SET_INTERSECTION); + d_equalityEngine->addFunctionKind(SET_INTER); d_equalityEngine->addFunctionKind(SET_MINUS); d_equalityEngine->addFunctionKind(SET_MEMBER); d_equalityEngine->addFunctionKind(SET_SUBSET); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 7b596be86..50ff3f09c 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -523,7 +523,7 @@ void TheorySetsPrivate::checkUpwardsClosure() // see if there are members in second argument const std::map& r2mem = d_state.getMembers(r2); const std::map& r2nmem = d_state.getNegativeMembers(r2); - if (!r2mem.empty() || k != kind::SET_INTERSECTION) + if (!r2mem.empty() || k != kind::SET_INTER) { Trace("sets-debug") << "Checking " << term << ", members = " << (!r1mem.empty()) @@ -546,7 +546,7 @@ void TheorySetsPrivate::checkUpwardsClosure() { valid = true; } - else if (k == kind::SET_INTERSECTION) + else if (k == kind::SET_INTER) { // conclude x is in term // if also existing in members of r2 diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 181a659c5..277b6bc84 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -81,7 +81,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { nm->mkNode(kind::EQUAL, node[0], node[1][0])); } else if (node[1].getKind() == kind::SET_UNION - || node[1].getKind() == kind::SET_INTERSECTION + || node[1].getKind() == kind::SET_INTER || node[1].getKind() == kind::SET_MINUS) { std::vector children; @@ -157,7 +157,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { else if (node[1].getKind() == kind::SET_MINUS && node[1][0] == node[0]) { // (setminus A (setminus A B)) = (intersection A B) - Node intersection = nm->mkNode(SET_INTERSECTION, node[0], node[1][1]); + Node intersection = nm->mkNode(SET_INTER, node[0], node[1][1]); return RewriteResponse(REWRITE_AGAIN, intersection); } else if (node[1].getKind() == kind::SET_UNIVERSE) @@ -185,7 +185,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { break; } // kind::SET_MINUS - case kind::SET_INTERSECTION: + case kind::SET_INTER: { if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; @@ -289,7 +289,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager::currentNM()->mkNode( kind::SET_CARD, NodeManager::currentNM()->mkNode( - kind::SET_INTERSECTION, node[0][0], node[0][1]))); + kind::SET_INTER, node[0][0], node[0][1]))); return RewriteResponse(REWRITE_DONE, ret ); } else if (node[0].getKind() == kind::SET_MINUS) @@ -300,7 +300,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { NodeManager::currentNM()->mkNode( kind::SET_CARD, NodeManager::currentNM()->mkNode( - kind::SET_INTERSECTION, node[0][0], node[0][1]))); + kind::SET_INTER, node[0][0], node[0][1]))); return RewriteResponse(REWRITE_DONE, ret ); } break; diff --git a/src/theory/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index 0793f011b..6602e7d03 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -30,7 +30,7 @@ TypeNode SetsBinaryOperatorTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) { - Assert(n.getKind() == kind::SET_UNION || n.getKind() == kind::SET_INTERSECTION + Assert(n.getKind() == kind::SET_UNION || n.getKind() == kind::SET_INTER || n.getKind() == kind::SET_MINUS); TypeNode setType = n[0].getType(check); if (check) @@ -57,7 +57,7 @@ bool SetsBinaryOperatorTypeRule::computeIsConst(NodeManager* nodeManager, TNode n) { // only SET_UNION has a const rule in kinds. - // SET_INTERSECTION and SET_MINUS are not used in the canonical representation + // SET_INTER and SET_MINUS are not used in the canonical representation // of sets and therefore they do not have const rules in kinds Assert(n.getKind() == kind::SET_UNION); return NormalForm::checkNormalConstant(n); -- cgit v1.2.3