diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-11-09 16:36:33 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-10 00:36:33 +0000 |
| commit | 68d6329d38af159afa7dc9542ef8e04e4d5a3773 (patch) | |
| tree | 1f6e35d1d58e63f2b8b436dedccf152414439a58 | |
| parent | eea329d3e061e1e0e98585f8b68c8db851b46513 (diff) | |
sets: Rename set.intersection to set.inter. (#7622)
This further renames kind SET_INTERSECTION to SET_INTER.
74 files changed, 130 insertions, 130 deletions
diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst index 423a5d4b1..8bce6b72c 100644 --- a/docs/theories/sets-and-relations.rst +++ b/docs/theories/sets-and-relations.rst @@ -42,7 +42,9 @@ a `cvc5::api::Solver solver` object. | | | | | | | ``Term t = solver.mkTerm(Kind::SET_UNION, X, Y);`` | +----------------------+----------------------------------------------+-------------------------------------------------------------------------+ -| Intersection | ``(set.minus X Y)`` | ``Term t = solver.mkTerm(Kind::SET_MINUS, X, Y);`` | +| Intersection | ``(set.inter X Y)`` | ``Term t = solver.mkTerm(Kind::SET_INTER, X, Y);`` | ++----------------------+----------------------------------------------+-------------------------------------------------------------------------+ +| Minus | ``(set.minus X Y)`` | ``Term t = solver.mkTerm(Kind::SET_MINUS, X, Y);`` | +----------------------+----------------------------------------------+-------------------------------------------------------------------------+ | Membership | ``(set.member x X)`` | ``Term x = solver.mkConst(solver.getIntegerSort(), "x");`` | | | | | @@ -76,7 +78,7 @@ Semantics ^^^^^^^^^ The semantics of most of the above operators (e.g., ``set.union``, -``set.intersection``, difference) are straightforward. +``set.inter``, difference) are straightforward. The semantics for the universe set and complement are more subtle and explained in the following. diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp index a4bc12ec8..ff3546b6f 100644 --- a/examples/api/cpp/sets.cpp +++ b/examples/api/cpp/sets.cpp @@ -43,10 +43,10 @@ int main() Term C = slv.mkConst(set, "C"); Term unionAB = slv.mkTerm(SET_UNION, A, B); - Term lhs = slv.mkTerm(SET_INTERSECTION, unionAB, C); + Term lhs = slv.mkTerm(SET_INTER, unionAB, C); - Term intersectionAC = slv.mkTerm(SET_INTERSECTION, A, C); - Term intersectionBC = slv.mkTerm(SET_INTERSECTION, B, C); + Term intersectionAC = slv.mkTerm(SET_INTER, A, C); + Term intersectionBC = slv.mkTerm(SET_INTER, B, C); Term rhs = slv.mkTerm(SET_UNION, intersectionAC, intersectionBC); Term theorem = slv.mkTerm(EQUAL, lhs, rhs); @@ -77,7 +77,7 @@ int main() Term singleton_three = slv.mkTerm(SET_SINGLETON, three); Term one_two = slv.mkTerm(SET_UNION, singleton_one, singleton_two); Term two_three = slv.mkTerm(SET_UNION, singleton_two, singleton_three); - Term intersection = slv.mkTerm(SET_INTERSECTION, one_two, two_three); + Term intersection = slv.mkTerm(SET_INTER, one_two, two_three); Term x = slv.mkConst(integer, "x"); diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index bf487c617..31f20dfeb 100644 --- a/examples/api/python/sets.py +++ b/examples/api/python/sets.py @@ -40,10 +40,10 @@ if __name__ == "__main__": C = slv.mkConst(set_, "C") unionAB = slv.mkTerm(kinds.SetUnion, A, B) - lhs = slv.mkTerm(kinds.SetIntersection, unionAB, C) + lhs = slv.mkTerm(kinds.SetInter, unionAB, C) - intersectionAC = slv.mkTerm(kinds.SetIntersection, A, C) - intersectionBC = slv.mkTerm(kinds.SetIntersection, B, C) + intersectionAC = slv.mkTerm(kinds.SetInter, A, C) + intersectionBC = slv.mkTerm(kinds.SetInter, B, C) rhs = slv.mkTerm(kinds.SetUnion, intersectionAC, intersectionBC) theorem = slv.mkTerm(kinds.Equal, lhs, rhs) @@ -72,7 +72,7 @@ if __name__ == "__main__": singleton_three = slv.mkTerm(kinds.SetSingleton, three) one_two = slv.mkTerm(kinds.SetUnion, singleton_one, singleton_two) two_three = slv.mkTerm(kinds.SetUnion, singleton_two, singleton_three) - intersection = slv.mkTerm(kinds.SetIntersection, one_two, two_three) + intersection = slv.mkTerm(kinds.SetInter, one_two, two_three) x = slv.mkConst(integer, "x") diff --git a/examples/api/smtlib/sets.smt2 b/examples/api/smtlib/sets.smt2 index f8b30ae47..59d3cdc4f 100644 --- a/examples/api/smtlib/sets.smt2 +++ b/examples/api/smtlib/sets.smt2 @@ -10,8 +10,8 @@ (check-sat-assuming ( (distinct - (set.intersection (set.union A B) C) - (set.union (set.intersection A C) (set.intersection B C))) + (set.inter (set.union A B) C) + (set.union (set.inter A C) (set.inter B C))) ) ) @@ -27,7 +27,7 @@ ( (set.member x - (set.intersection + (set.inter (set.union (set.singleton 1) (set.singleton 2)) (set.union (set.singleton 2) (set.singleton 3)))) ) diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 69fc07837..0e1b93146 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -146,7 +146,7 @@ class Mapper { << " ( (s1 " << name << ") (s2 " << name << ") )" << " " << name << "" << " ((_ map and) s1 s2))" << endl; - setoperators[make_pair(t, kind::SET_INTERSECTION)] = + setoperators[make_pair(t, kind::SET_INTER)] = em->mkVar(std::string("intersection") + elementTypeAsString, em->mkFunctionType(t_t, t)); 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<Kind, cvc5::Kind> 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<cvc5::Kind, Kind, cvc5::kind::KindHashFunction> /* 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<Term>& 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<Kind> bin_kinds = {SET_UNION, SET_INTERSECTION, SET_MINUS}; + std::vector<Kind> bin_kinds = {SET_UNION, SET_INTER, SET_MINUS}; std::vector<TypeNode> 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; j<vs.size(); j++ ){ - bchildren.push_back( - NodeManager::currentNM() - ->mkNode(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<Node> 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<Node> 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<Node, Node>& r2mem = d_state.getMembers(r2); const std::map<Node, Node>& 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<Node> 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); diff --git a/test/regress/regress0/rels/addr_book_0.cvc.smt2 b/test/regress/regress0/rels/addr_book_0.cvc.smt2 index 70488b4eb..9bc85f268 100644 --- a/test/regress/regress0/rels/addr_book_0.cvc.smt2 +++ b/test/regress/regress0/rels/addr_book_0.cvc.smt2 @@ -33,7 +33,7 @@ (assert (set.member t_tup Target)) (assert (set.subset (rel.join (rel.join Book addr) Target) Name)) (assert (set.subset (rel.join Book names) Name)) -(assert (= (set.intersection Name Addr) (as set.empty (Set (Tuple Atom))))) +(assert (= (set.inter Name Addr) (as set.empty (Set (Tuple Atom))))) (assert (= (rel.join (set.singleton n_tup) (rel.join (set.singleton b1_tup) addr)) (as set.empty (Set (Tuple Atom))))) (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.union (rel.join _let_1 (rel.join (set.singleton b1_tup) addr)) (set.singleton t_tup))))) (assert (let ((_let_1 (set.singleton n_tup))) (= (rel.join _let_1 (rel.join (set.singleton b3_tup) addr)) (set.minus (rel.join _let_1 (rel.join (set.singleton b2_tup) addr)) (set.singleton t_tup))))) diff --git a/test/regress/regress0/rels/iden_0.cvc.smt2 b/test/regress/regress0/rels/iden_0.cvc.smt2 index 1cdeffbff..75dc80d22 100644 --- a/test/regress/regress0/rels/iden_0.cvc.smt2 +++ b/test/regress/regress0/rels/iden_0.cvc.smt2 @@ -21,5 +21,5 @@ (assert (set.member v x)) (assert (set.member a x)) (assert (= id (rel.iden t))) -(assert (not (set.member (tuple 1 1) (set.intersection id x)))) +(assert (not (set.member (tuple 1 1) (set.inter id x)))) (check-sat) diff --git a/test/regress/regress0/sets/complement3.cvc.smt2 b/test/regress/regress0/sets/complement3.cvc.smt2 index 20cfb36f8..2046b2fc9 100644 --- a/test/regress/regress0/sets/complement3.cvc.smt2 +++ b/test/regress/regress0/sets/complement3.cvc.smt2 @@ -8,7 +8,7 @@ (declare-fun C4 () (Set (Tuple Atom))) (declare-fun ATOM_UNIV () (Set (Tuple Atom))) (declare-fun V1 () Atom) -(assert (= C32 (set.intersection (set.complement C2) (set.complement C4)))) +(assert (= C32 (set.inter (set.complement C2) (set.complement C4)))) (assert (set.member (tuple V1) (set.complement C32))) (assert (= ATOM_UNIV (as set.universe (Set (Tuple Atom))))) (assert (set.member (tuple V1) ATOM_UNIV)) diff --git a/test/regress/regress0/sets/cvc-sample.cvc.smt2 b/test/regress/regress0/sets/cvc-sample.cvc.smt2 index 9ee199b43..9c89df0c6 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc.smt2 +++ b/test/regress/regress0/sets/cvc-sample.cvc.smt2 @@ -20,12 +20,12 @@ (declare-fun e () Int) (assert (= a (set.singleton 5))) (assert (= c (set.union a b))) -(assert (not (= c (set.intersection a b)))) +(assert (not (= c (set.inter a b)))) (assert (= c (set.minus a b))) (assert (set.subset a b)) (assert (set.member e c)) (assert (set.member e a)) -(assert (set.member e (set.intersection a b))) +(assert (set.member e (set.inter a b))) (push 1) (assert true) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 index 0ecd32bf8..c93b18857 100644 --- a/test/regress/regress0/sets/eqtest.smt2 +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -10,9 +10,9 @@ (declare-fun H () (Set Int) ) (declare-fun I () (Set Int) ) (declare-fun x () Int) -(assert (set.member x (set.intersection (set.union A B) C))) +(assert (set.member x (set.inter (set.union A B) C))) (assert (not (set.member x G))) (assert (= (set.union A B) D)) -(assert (= C (set.intersection E F))) +(assert (= C (set.inter E F))) (assert (and (= F H) (= G H) (= H I))) (check-sat) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 index 7e2f627ae..76592a691 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 index f6fd4bd53..b0172db39 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 index f70d59b16..1538a2e9f 100644 --- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 +++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 @@ -66,7 +66,7 @@ (assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_38$0 sk_?X_37$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_38$0 sk_?X_37$0)) :named precondition_of_rec_copy_loop_34_11_19)) (assert (! (= old_cp_2$0 cp$0) :named assign_41_4)) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 index 6857e5147..66f843c9d 100644 --- a/test/regress/regress0/sets/sets-inter.smt2 +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -5,7 +5,7 @@ (declare-fun b () (Set Int)) (declare-fun x () Int) ;(assert (not (set.member x a))) -(assert (set.member x (set.intersection a b))) +(assert (set.member x (set.inter a b))) (assert (not (set.member x b))) (check-sat) (exit) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index 4a49bef07..0020e5c55 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -8,7 +8,7 @@ (declare-fun x () Int) (assert (set.member x (set.union A B))) -(assert (not (set.member x (set.intersection A B)))) +(assert (not (set.member x (set.inter A B)))) (assert (not (set.member x (set.minus A B)))) ;(assert (not (set.member x (set.minus B A)))) ;(assert (set.member x B)) diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2 index 20832c573..00546eee2 100644 --- a/test/regress/regress0/sets/sets-poly-int-real.smt2 +++ b/test/regress/regress0/sets/sets-poly-int-real.smt2 @@ -11,7 +11,7 @@ (assert (= t1 (set.union s (set.singleton 2.5)))) (assert (= t2 (set.union s (set.singleton 2.0)))) (assert (= t3 (set.union r3 (set.singleton 2.5)))) -(assert (= (set.intersection r1 r2) (set.intersection s (set.singleton 0.0)))) +(assert (= (set.inter r1 r2) (set.inter s (set.singleton 0.0)))) (assert (not (= r1 (as set.empty (Set Real))))) (check-sat) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index 3dcafae08..4a11bcc78 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -15,12 +15,12 @@ (declare-fun e () Int) (assert (= a (set.singleton 5))) (assert (= c (set.union a b) )) -(assert (not (= c (set.intersection a b) ))) +(assert (not (= c (set.inter a b) ))) (assert (= c (set.minus a b) )) (assert (set.subset a b)) (assert (set.member e c)) (assert (set.member e a)) -(assert (set.member e (set.intersection a b))) +(assert (set.member e (set.inter a b))) (check-sat) (pop 1) diff --git a/test/regress/regress0/sets/sharing-simp.smt2 b/test/regress/regress0/sets/sharing-simp.smt2 index be746be1d..a591792cf 100644 --- a/test/regress/regress0/sets/sharing-simp.smt2 +++ b/test/regress/regress0/sets/sharing-simp.smt2 @@ -9,7 +9,7 @@ (assert (set.member x A)) (assert (set.member y B)) -(assert (or (= C (set.intersection A B)) (= D (set.intersection A B)))) +(assert (or (= C (set.inter A B)) (= D (set.inter A B)))) (check-sat) diff --git a/test/regress/regress1/quantifiers/set8.smt2 b/test/regress/regress1/quantifiers/set8.smt2 index 209b213c1..17eea7b0a 100644 --- a/test/regress/regress1/quantifiers/set8.smt2 +++ b/test/regress/regress1/quantifiers/set8.smt2 @@ -15,12 +15,12 @@ (assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (set.subset ?s1 ?s2) (set.subset ?s2 ?s1))))) (declare-fun union (Set Set) Set) (assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (union ?s1 ?s2)) (or (set.member ?x ?s1) (set.member ?x ?s2))))) -(declare-fun set.intersection (Set Set) Set) -(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (set.intersection ?s1 ?s2)) (and (set.member ?x ?s1) (set.member ?x ?s2))))) +(declare-fun set.inter (Set Set) Set) +(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (set.inter ?s1 ?s2)) (and (set.member ?x ?s1) (set.member ?x ?s2))))) (declare-fun difference (Set Set) Set) (assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (set.member ?x (difference ?s1 ?s2)) (and (set.member ?x ?s1) (not (set.member ?x ?s2)))))) (declare-fun a () Set) (declare-fun b () Set) -(assert (not (seteq (set.intersection a b) (set.intersection b a)))) +(assert (not (seteq (set.inter a b) (set.inter b a)))) (check-sat) (exit) diff --git a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 index 7e80fdd70..8269daf42 100644 --- a/test/regress/regress1/rels/rel_complex_3.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_3.cvc.smt2 @@ -20,12 +20,12 @@ (assert (= r (rel.join x y))) (declare-fun e () (Tuple Int Int)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 index 9a35f336e..134a99c73 100644 --- a/test/regress/regress1/rels/rel_complex_4.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_4.cvc.smt2 @@ -24,12 +24,12 @@ (assert (= w (set.singleton e))) (assert (set.subset (rel.transpose w) y)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 index fc2d73235..ed894518e 100644 --- a/test/regress/regress1/rels/rel_complex_5.cvc.smt2 +++ b/test/regress/regress1/rels/rel_complex_5.cvc.smt2 @@ -26,12 +26,12 @@ (assert (let ((_let_1 (set.singleton a))) (= w (rel.product _let_1 _let_1)))) (assert (set.subset (rel.transpose w) y)) (assert (not (set.member e r))) -(assert (not (= z (set.intersection x y)))) +(assert (not (= z (set.inter x y)))) (assert (= z (set.minus x y))) (assert (set.subset x y)) (assert (set.member e (rel.join r z))) (assert (set.member e x)) -(assert (set.member e (set.intersection x y))) +(assert (set.member e (set.inter x y))) (push 1) (assert true) diff --git a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 index 144566fc5..e5b92a4fc 100644 --- a/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 +++ b/test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 @@ -12,7 +12,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 index 9a2521520..206450142 100644 --- a/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 +++ b/test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 index b2732dbd2..fe7e7d7ac 100644 --- a/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 +++ b/test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 index ee24367c3..078b98eef 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 index b0cfe4888..756f0430c 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 index 9ac15e9a4..1e45c21e9 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) (define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (set.subset s1 s2)) (declare-fun z3v66 () Int) diff --git a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 index 68ed72a93..a3fd883b6 100644 --- a/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 +++ b/test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 @@ -6,7 +6,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/card-3.smt2 b/test/regress/regress1/sets/card-3.smt2 index 383395b0d..bbcf1c489 100644 --- a/test/regress/regress1/sets/card-3.smt2 +++ b/test/regress/regress1/sets/card-3.smt2 @@ -8,5 +8,5 @@ (assert (>= (set.card (set.union s u)) 8)) (assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (check-sat) diff --git a/test/regress/regress1/sets/card-4.smt2 b/test/regress/regress1/sets/card-4.smt2 index 019b16a09..9f0e96dc5 100644 --- a/test/regress/regress1/sets/card-4.smt2 +++ b/test/regress/regress1/sets/card-4.smt2 @@ -8,7 +8,7 @@ (assert (>= (set.card (set.union s u)) 8)) ;(assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (declare-fun x1 () E) (declare-fun x2 () E) (declare-fun x3 () E) diff --git a/test/regress/regress1/sets/card-5.smt2 b/test/regress/regress1/sets/card-5.smt2 index c24ca974a..51ad7971c 100644 --- a/test/regress/regress1/sets/card-5.smt2 +++ b/test/regress/regress1/sets/card-5.smt2 @@ -8,7 +8,7 @@ (assert (>= (set.card (set.union s u)) 8)) ;(assert (<= (set.card (set.union t u)) 5)) (assert (<= (set.card s) 5)) -(assert (= (as set.empty (Set E)) (set.intersection t u))) +(assert (= (as set.empty (Set E)) (set.inter t u))) (declare-fun x1 () E) (declare-fun x2 () E) (declare-fun x3 () E) diff --git a/test/regress/regress1/sets/card-6.smt2 b/test/regress/regress1/sets/card-6.smt2 index b0ef3a3b9..fc2d34acc 100644 --- a/test/regress/regress1/sets/card-6.smt2 +++ b/test/regress/regress1/sets/card-6.smt2 @@ -7,7 +7,7 @@ (assert (and (= (as set.empty (Set E)) - (set.intersection A B)) + (set.inter A B)) (set.subset C (set.union A B)) (>= (set.card C) 5) (<= (set.card A) 2) diff --git a/test/regress/regress1/sets/comp-intersect.smt2 b/test/regress/regress1/sets/comp-intersect.smt2 index 60d9046bd..5f6f7576b 100644 --- a/test/regress/regress1/sets/comp-intersect.smt2 +++ b/test/regress/regress1/sets/comp-intersect.smt2 @@ -9,6 +9,6 @@ (assert (= x (set.comprehension ((z Int)) (> z 4) (* 5 z)))) (assert (= y (set.comprehension ((z Int)) (< z 10) (+ (* 5 z) 1)))) -(assert (not (= (set.intersection x y) (as set.empty (Set Int))))) +(assert (not (= (set.inter x y) (as set.empty (Set Int))))) (check-sat) diff --git a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 index 7c5e09b5a..93d359b60 100644 --- a/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 +++ b/test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -7,7 +7,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 index aa5b62d09..ec82ddb8b 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2 @@ -7,6 +7,6 @@ (declare-fun universe () (Set Bool)) (assert (= (set.card A) 2)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set Bool)))) +(assert (= (set.inter A B) (as set.empty (Set Bool)))) (assert (= universe (as set.universe (Set Bool)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 index 91bf1905a..0003349b3 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2 @@ -8,7 +8,7 @@ (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 2)) +(assert (= (set.card (set.inter A B)) 2)) (assert (= (set.card (set.minus A B)) 3)) (assert (= (set.card (set.minus B A)) 3)) (assert (= universe (as set.universe (Set (_ BitVec 3))))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 index adbe51507..5808c4ec7 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2 @@ -9,7 +9,7 @@ (assert (= (set.card A) 3)) (assert (= (set.card B) 3)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= (set.card (set.minus A B)) 2)) (assert (= (set.card (set.minus B A)) 2)) (assert (not (set.member x A))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 index 2ccbc8a58..81c49e1e3 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2 @@ -9,7 +9,7 @@ (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) (assert (not (= A B))) -(assert (= (set.card (set.intersection A B)) 2)) +(assert (= (set.card (set.inter A B)) 2)) (assert (= (set.card (set.minus A B)) 3)) (assert (= (set.card (set.minus B A)) 3)) (assert (= universe (as set.universe (Set (_ BitVec 3))))) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 index 4c113c84b..62c0bc224 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2 @@ -9,6 +9,6 @@ (declare-fun x () Rec) (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= universe (as set.universe (Set Rec)))) (check-sat) diff --git a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 index 4c9bdadd5..70e3a88d8 100644 --- a/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 +++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2 @@ -8,6 +8,6 @@ (declare-fun universe () (Set Rec)) (assert (= (set.card A) 9)) (assert (= (set.card B) 9)) -(assert (= (set.card (set.intersection A B)) 1)) +(assert (= (set.card (set.inter A B)) 1)) (assert (= universe (as set.universe (Set Rec)))) (check-sat) diff --git a/test/regress/regress1/sets/fuzz14418.smt2 b/test/regress/regress1/sets/fuzz14418.smt2 index 2fb60cb72..b09cf1151 100644 --- a/test/regress/regress1/sets/fuzz14418.smt2 +++ b/test/regress/regress1/sets/fuzz14418.smt2 @@ -34,7 +34,7 @@ (let ((e14 (set.minus v2 v2))) (let ((e15 (f1 v1 v4 v1))) (let ((e16 (f1 e14 v1 v4))) -(let ((e17 (set.intersection e16 e15))) +(let ((e17 (set.inter e16 e15))) (let ((e18 (f1 v4 e15 v2))) (let ((e19 (ite (p1 e13) (set.singleton 1) (set.singleton 0)))) (let ((e20 (set.member v0 e17))) diff --git a/test/regress/regress1/sets/fuzz15201.smt2 b/test/regress/regress1/sets/fuzz15201.smt2 index 3094a8d84..bdcbe7d59 100644 --- a/test/regress/regress1/sets/fuzz15201.smt2 +++ b/test/regress/regress1/sets/fuzz15201.smt2 @@ -29,9 +29,9 @@ (let ((e16 (set.minus v2 v1))) (let ((e17 (set.minus v1 v2))) (let ((e18 (set.union e17 e17))) -(let ((e19 (set.intersection e17 v1))) -(let ((e20 (set.intersection e17 e18))) -(let ((e21 (set.intersection v1 e16))) +(let ((e19 (set.inter e17 v1))) +(let ((e20 (set.inter e17 e18))) +(let ((e21 (set.inter v1 e16))) (let ((e22 (set.minus e20 e16))) (let ((e23 (ite (p1 v2 e18 e21) (set.singleton 1) (set.singleton 0)))) (let ((e24 (set.minus e17 e23))) diff --git a/test/regress/regress1/sets/fuzz31811.smt2 b/test/regress/regress1/sets/fuzz31811.smt2 index e86901f9a..ca028488a 100644 --- a/test/regress/regress1/sets/fuzz31811.smt2 +++ b/test/regress/regress1/sets/fuzz31811.smt2 @@ -28,19 +28,19 @@ (let ((e10 (f0 v0 e8 e8))) (let ((e11 (ite (p1 v1) (set.singleton 1) (set.singleton 0)))) (let ((e12 (set.union v3 v3))) -(let ((e13 (set.intersection v3 v1))) +(let ((e13 (set.inter v3 v1))) (let ((e14 (ite (p1 v3) (set.singleton 1) (set.singleton 0)))) -(let ((e15 (set.intersection v2 e14))) +(let ((e15 (set.inter v2 e14))) (let ((e16 (ite (p1 e11) (set.singleton 1) (set.singleton 0)))) (let ((e17 (ite (p1 v4) (set.singleton 1) (set.singleton 0)))) (let ((e18 (set.union e15 v2))) (let ((e19 (ite (p1 e16) (set.singleton 1) (set.singleton 0)))) -(let ((e20 (set.intersection e18 v3))) +(let ((e20 (set.inter e18 v3))) (let ((e21 (set.minus v4 e12))) (let ((e22 (set.union v3 v2))) (let ((e23 (set.minus e12 v4))) (let ((e24 (set.minus v3 e16))) -(let ((e25 (set.intersection e19 e20))) +(let ((e25 (set.inter e19 e20))) (let ((e26 (ite (p1 e15) (set.singleton 1) (set.singleton 0)))) (let ((e27 (set.minus e17 e15))) (let ((e28 (f1 e23 e12))) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 index f6d032f11..57f4344c6 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2 @@ -7,6 +7,6 @@ (assert (= (set.card universe) 3)) (assert (= (set.card A) 2)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int))))) +(assert (= (set.inter A B) (as set.empty (Set (Array Int Int))))) (assert (= universe (as set.universe (Set (Array Int Int))))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 index d7e6a758c..76828576e 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2 @@ -7,6 +7,6 @@ (assert (= (set.card universe) 3)) (assert (= (set.card A) 1)) (assert (= (set.card B) 2)) -(assert (= (set.intersection A B) (as set.empty (Set (Array Int Int))))) +(assert (= (set.inter A B) (as set.empty (Set (Array Int Int))))) (assert (= universe (as set.universe (Set (Array Int Int))))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 index c649c9be2..2cf5e566d 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2 @@ -7,6 +7,6 @@ (declare-const B (Set Int)) (assert (= (set.card A) 6)) (assert (= (set.card B) 5)) -(assert (= (set.intersection A B) (as set.empty (Set Int)))) +(assert (= (set.inter A B) (as set.empty (Set Int)))) (assert (= universe (as set.universe (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 index b3958e79e..8668b9c27 100644 --- a/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 +++ b/test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2 @@ -7,6 +7,6 @@ (declare-const B (Set Int)) (assert (= (set.card A) 5)) (assert (= (set.card B) 5)) -(assert (= (set.intersection A B) (as set.empty (Set Int)))) +(assert (= (set.inter A B) (as set.empty (Set Int)))) (assert (= universe (as set.universe (Set Int)))) (check-sat) diff --git a/test/regress/regress1/sets/insert_invariant_37_2.smt2 b/test/regress/regress1/sets/insert_invariant_37_2.smt2 index cac805531..a8f117062 100644 --- a/test/regress/regress1/sets/insert_invariant_37_2.smt2 +++ b/test/regress/regress1/sets/insert_invariant_37_2.smt2 @@ -723,7 +723,7 @@ (assert (! (not (set.member null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1)) (assert (! (or (= prev_2$0 curr_2$0) - (set.member sk_?e_1$0 (set.intersection sk_?X_4$0 sk_?X_3$0)) + (set.member sk_?e_1$0 (set.inter sk_?X_4$0 sk_?X_3$0)) (and (set.member sk_?e_1$0 sk_FP$0) (not (set.member sk_?e_1$0 FP$0))) (and (set.member sk_?e$0 (set.union c1_2$0 c2_2$0)) (not (set.member sk_?e$0 content$0))) (and (set.member sk_?e$0 c1_2$0) diff --git a/test/regress/regress1/sets/issue2904.smt2 b/test/regress/regress1/sets/issue2904.smt2 index c39ea09ba..d2ffdbd7c 100644 --- a/test/regress/regress1/sets/issue2904.smt2 +++ b/test/regress/regress1/sets/issue2904.smt2 @@ -21,6 +21,6 @@ (assert (> n (+ (* 2 f) m))) -(assert (>= (set.card (set.minus UNIVERALSET (set.intersection (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n)) +(assert (>= (set.card (set.minus UNIVERALSET (set.inter (set.minus UNIVERALSET b) (set.minus UNIVERALSET c)))) n)) (check-sat) diff --git a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 index fd3bd62eb..f57837d05 100644 --- a/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 +++ b/test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2 @@ -2,6 +2,6 @@ (set-info :status unsat) (declare-fun st1 () (Set Int)) (declare-fun st7 () (Set Int)) -(assert (> 0 (set.card (set.intersection st1 (set.union st7 st1))))) +(assert (> 0 (set.card (set.inter st1 (set.union st7 st1))))) (assert (set.subset st1 st7)) (check-sat) diff --git a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 index bc2f103d2..55b4ac581 100644 --- a/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 +++ b/test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2 @@ -2,7 +2,7 @@ (set-info :status unsat) (declare-fun st3 () (Set String)) (declare-fun st9 () (Set String)) -(assert (set.is_singleton (set.intersection st3 st9))) -(assert (< 1 (set.card (set.intersection st3 st9)))) +(assert (set.is_singleton (set.inter st3 st9))) +(assert (< 1 (set.card (set.inter st3 st9)))) (assert (set.is_singleton st9)) (check-sat) diff --git a/test/regress/regress1/sets/issue4391-card-lasso.smt2 b/test/regress/regress1/sets/issue4391-card-lasso.smt2 index f7a720436..76e27f5b0 100644 --- a/test/regress/regress1/sets/issue4391-card-lasso.smt2 +++ b/test/regress/regress1/sets/issue4391-card-lasso.smt2 @@ -11,6 +11,6 @@ (assert (= (set.card b) d)) (assert (= (set.card c) 0)) (assert (= 0 (mod 0 d))) -(assert (> (set.card (set.minus e (set.intersection (set.intersection e b) (set.minus e c)))) 1)) +(assert (> (set.card (set.minus e (set.inter (set.inter e b) (set.minus e c)))) 1)) (check-sat) diff --git a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 index ae71a1edb..a5ee519f5 100644 --- a/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 +++ b/test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2 @@ -27,7 +27,7 @@ (define-fun smt_set_mem ((x Elt) (s mySet)) Bool (set.member x s)) (define-fun smt_set_add ((s mySet) (x Elt)) mySet (set.union s (set.singleton x))) (define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (set.union s1 s2)) -(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.intersection s1 s2)) +(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (set.inter s1 s2)) ;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s)) (define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (set.minus s1 s2)) ;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2))) diff --git a/test/regress/regress1/sets/remove_check_free_31_6.smt2 b/test/regress/regress1/sets/remove_check_free_31_6.smt2 index c2ff1da23..9c2bc9be7 100644 --- a/test/regress/regress1/sets/remove_check_free_31_6.smt2 +++ b/test/regress/regress1/sets/remove_check_free_31_6.smt2 @@ -230,7 +230,7 @@ (assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0)) :named invariant_18_4_69)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_27$0 sk_?X_28$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_27$0 sk_?X_28$0)) :named invariant_18_4_70)) (assert (! (= Alloc$0 (set.union FP_Caller$0 Alloc$0)) @@ -246,7 +246,7 @@ (assert (! (= FP_2$0 (set.union (set.minus FP$0 FP_1$0) - (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))) + (set.union (set.inter Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0)))) :named framecondition_of_remove_loop_18_4_17)) (assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0) @@ -311,7 +311,7 @@ (assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74)) -(assert (! (= (as set.empty SetLoc) (set.intersection sk_?X_32$0 sk_?X_31$0)) +(assert (! (= (as set.empty SetLoc) (set.inter sk_?X_32$0 sk_?X_31$0)) :named invariant_18_4_75)) (assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76)) @@ -320,7 +320,7 @@ :named invariant_18_4_77)) (assert (! (= sk_?X_29$0 - (set.union (set.intersection Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))) + (set.union (set.inter Alloc$0 FP_1$0) (set.minus Alloc$0 Alloc$0))) :named invariant_18_4_78)) (assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0)) diff --git a/test/regress/regress1/sym/sym5.smt2 b/test/regress/regress1/sym/sym5.smt2 index cf9cbe092..16b44d115 100644 --- a/test/regress/regress1/sym/sym5.smt2 +++ b/test/regress/regress1/sym/sym5.smt2 @@ -13,6 +13,6 @@ (assert (set.subset A (set.insert g h i (set.singleton f)))) (assert (= C (set.minus A B) )) (assert (set.subset B A)) -(assert (= C (set.intersection A B))) +(assert (= C (set.inter A B))) (assert (set.member j C)) (check-sat) diff --git a/test/regress/regress1/trim.cvc.smt2 b/test/regress/regress1/trim.cvc.smt2 index f05e08572..d823e565d 100644 --- a/test/regress/regress1/trim.cvc.smt2 +++ b/test/regress/regress1/trim.cvc.smt2 @@ -18,9 +18,9 @@ (declare-fun ic0_c () (Set myType)) (assert (forall ((r myType)) (=> (set.member r ic0_i) (forall ((r2 myType)) (=> (set.member r2 (neg (select d r))) (set.member r2 ic0_c)))))) (assert (set.subset (set.singleton A) ic0_i)) -(assert (or (exists ((e0 myType)) (=> (set.member e0 ic0_i) (set.subset (select l A) (select l e0)))) (set.subset (set.intersection ic0_i ic0_c) emptymyTypeSet))) +(assert (or (exists ((e0 myType)) (=> (set.member e0 ic0_i) (set.subset (select l A) (select l e0)))) (set.subset (set.inter ic0_i ic0_c) emptymyTypeSet))) (declare-fun ic1_i () (Set myType)) (declare-fun ic1_c () (Set myType)) (assert (forall ((r myType)) (=> (set.member r (pos (select d B))) (set.member r ic1_i)))) -(assert (or (exists ((e1 myType)) (=> (set.member e1 ic1_i) (set.subset (select l B) (select l e1)))) (set.subset (set.intersection ic1_i ic1_c) emptymyTypeSet))) +(assert (or (exists ((e1 myType)) (=> (set.member e1 ic1_i) (set.subset (select l B) (select l e1)))) (set.subset (set.inter ic1_i ic1_c) emptymyTypeSet))) (check-sat) |