sets: Rename set.intersection to set.inter. (#7622)

This further renames kind SET_INTERSECTION to SET_INTER.

diff --git a/docs/theories/sets-and-relations.rst b/docs/theories/sets-and-relations.rst
index 423a5d4b17b5c82e38f4fbf6a35961775becb30e..8bce6b72c80783c9867215f098eac0ee26a9e7c8 100644 (file)
--- 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 a4bc12ec82dedda62a31af7f740b42d9e5ff7033..ff3546b6fa8111f2fbda8e33295e0246ceeca4ca 100644 (file)
--- 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 bf487c617e733e4011d54ee04d80cc650a65988a..31f20dfeb51f74988fc85c072bde2ef8b5a6f95f 100644 (file)
--- 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 f8b30ae4777d1dd7771f96fb36831495d1ed781d..59d3cdc4f7bbc81e708ffe6961cb4084400e777f 100644 (file)
--- 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 69fc07837dd9e199e92480dc2efecaf9fda4e945..0e1b931463641dfd10dc3388cf7543a7361e45d2 100644 (file)
--- 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 797d2e473d2083c5dbef37215b4e372442bbf9ca..ae0ee2ceb70bfe2a929a5d08d4243de00a6843ee 100644 (file)
--- 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 162ec24e7260b24190f3dd9ba4e4628224632186..90a57317df60d091ac54cca7a0f7c56b2dfa4de1 100644 (file)
--- 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 7add605c5623c678d73382aa683144a5a2d091a2..ef784746ccebf561f0c6f696cc3696762c5c4c91 100644 (file)
--- 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 5d4387658ad339f6e9b3a135bd7d69d298a7cf8d..8ed4929e593aec9d29a94c27d6c8069d2976f0ae 100644 (file)
--- 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 75a353dbe5842e755d4f7b16776622c3e9a890f5..24efc60c3cc716b5a55ae843f7f87dd0c02be76c 100644 (file)
--- 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 034f5f23cee1b0d5fc18519cde85a63115c448da..99170427e19d1ec1ebac9b2919793a0bf0397458 100644 (file)
--- 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 5c9e91d32cea1c05803f6cdb2fa30811e462d4be..0408d27daeadb6dec9e115bbfa6b0be890d00dfc 100644 (file)
--- 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 de4c56552191154b40d06a4a791d8c6a25389288..704951f521f3869910aa2a55d982c1128a4a04ea 100644 (file)
--- 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 218c0980449f3ca421a242ac146e761c23c0dfc1..3ee4fa0120c313edc2374c85142ef124dc018434 100644 (file)
--- 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 f65c41b53e81fca9d1d5967d80f2a4a6a37da7d1..c35eaf49a55d698be7a360aa99fa2ec9e1533033 100644 (file)
--- 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 f5ed7cd872671437a5a815e7d512a63617798ed3..71d5fce4ad5b9b09bbf78236be64880d8c8dfe32 100644 (file)
--- 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 023a8a6af98ab21d6b25e7d9a343995c6894a5a1..3f619dcade2f24b75a571e0c562c5ed2e8225e78 100644 (file)
--- 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 41fe0b4c81e1649bcb3c5ce1c9ee784e17cbd551..d4b5aa824b8eeb86eb762508d83d6b53070d1560 100644 (file)
--- 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 b2eb80f758e45b874154c30ff756789d930fb63b..c3d0b9bbe6540204214705188203143d2e3fccec 100644 (file)
--- 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 7b596be86086fafd601d523759931bd1adc9dfce..50ff3f09c3e431b91da6b00af84d0a6b6ccdf0e7 100644 (file)
--- 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 181a659c5d58752f83a1a242cff8a4a28f2a8809..277b6bc840ec372669d6b8581591c50c14938f76 100644 (file)
--- 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 0793f011b854be3a539cc7829cac5adc612eff53..6602e7d033ec244b1e104a944b1df6ee9a89e730 100644 (file)
--- 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 70488b4eb4772ff450d399cfb307eea5fed3a20b..9bc85f268da50d564b29cf6a7a9d37d3128435e5 100644 (file)
--- 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 1cdeffbfff6575810a0f7f3ec7cf4ab3c364f042..75dc80d227ddb03a136e496c65a17af0f9c1cbfd 100644 (file)
--- 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 20cfb36f8fda7703b8258ee6850f85fd276bb60b..2046b2fc9601bde1bf9a802b3d4fd622c87c8e45 100644 (file)
--- 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 9ee199b43ac9d73330f236662eede1d24404f32f..9c89df0c6a5ab353dfe2375f49828a76699e5861 100644 (file)
--- 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 0ecd32bf8f72322b48ed5ab6a5835133e405d088..c93b18857a5e500a467b86e24fc700fa37a0eb9d 100644 (file)
--- 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 7e2f627ae76dbba9b87f1d3f5cc059f11ca6578c..76592a691ebef78792d31f73e72e3a67ffc9ad2d 100644 (file)
--- 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 f6fd4bd5332f621e65e47e11b36da7e22d1f5559..b0172db399414e6670c47b1ac76e7b957aad6487 100644 (file)
--- 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 f70d59b16246d98b289143dc7cd67f1f9a57c125..1538a2e9f1495d2fa1216a8ed0e47127f55d28dc 100644 (file)
--- 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 6857e5147a1670b2d0a1535f4d0efa0d20ef89f2..66f843c9dbd2d5cad89deafa18a161c06190d07f 100644 (file)
--- 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 4a49bef0715b6128ad26ba0bc25035875e8360f6..0020e5c5576a37b1da66eb9d2d98ece90359af53 100644 (file)
--- 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 20832c573264bc59236113a13fcd69501f7e2a63..00546eee2c72686259ba672456939be578c593ee 100644 (file)
--- 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 3dcafae086fa89a6410cc28755cf0537deb481e6..4a11bcc78a001e30b31fa5fbda7f9d8136c12053 100644 (file)
--- 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 be746be1d629b0199837ed2515b29ce05cd7e458..a591792cf70f52f602ae89ed81a7866116e4d72b 100644 (file)
--- 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 209b213c16342e9cb56a0e13c2cbcd15e15d97a0..17eea7b0a389f04484d4307df30b408d86d876ac 100644 (file)
--- 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 7e80fdd70a12994dd35634665ddbcf66c5b028fb..8269daf426aa91a4c6165bcc7a5bf13a21ac6f12 100644 (file)
--- 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 9a35f336e3f8e26d149f8459a74cfff56655f548..134a99c73371b4e50b8ed2a8751f2450ae6aa20f 100644 (file)
--- 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 fc2d73235d6e93fe48fce31cbf132301bc839fab..ed894518e8c8b8727ca123c5e9d86a0c4da60948 100644 (file)
--- 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 144566fc593df89ce8aada849cb4a4a9471b7523..e5b92a4fc7d344a8cffc2689362ea4c28980c50c 100644 (file)
--- 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 9a2521520ad2017fe24c3732980530f03abd387f..206450142147d62c58d9b33018a60ded00f1d119 100644 (file)
--- 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 b2732dbd2cda8dbfb99965ff6a987c8a534eb9c4..fe7e7d7acded3e9836806735bd46122f6f7c9639 100644 (file)
--- 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 ee24367c3e1030a6e239ad5ac8bfa488b52d63be..078b98eef85079106229727d0ec8fa6cd0800a3f 100644 (file)
--- 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 b0cfe4888693181afa1b000244987ad0a7814bd3..756f0430cbc6a0f94d46558dd4741b7d49da0126 100644 (file)
--- 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 9ac15e9a405a26317e6bd8eadfd1340c8632b3a3..1e45c21e9c557346ae384dc4e65c95a596f134a7 100644 (file)
--- 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 68ed72a93874d06e86ee9a5bad6b5a1807182814..a3fd883b61a89bf668e1fe9db5a88edab8b5e4d0 100644 (file)
--- 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 383395b0d831104f2da5be9756985ca3626f9517..bbcf1c4898afa6ca0f45f572fbb9e5f7335954e9 100644 (file)
--- 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 019b16a097b0c8aa4ffee0c67b763cf3f2aafe77..9f0e96dc57b08a3ce533b64b4da3747ab510e176 100644 (file)
--- 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 c24ca974a1918e544012e291809854cc4ec53dc5..51ad7971c781ea7be0f91deea6ec5943d09d4b85 100644 (file)
--- 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 b0ef3a3b9c074f0fd1e7e79f44f08743662f09f1..fc2d34acc4cd9109d8fa55d913ba03a05415665b 100644 (file)
--- 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 60d9046bd1832e3e4b75507b9d1bd9edb01de34b..5f6f7576beab60a18ea611033ae569b85342746e 100644 (file)
--- 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 7c5e09b5af6abe4c53dafb2e49c658dd7f7e55de..93d359b606ae851d5848ab8961d57888f141b258 100644 (file)
--- 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 aa5b62d09534f915d76ce5d0dc010f4411211151..ec82ddb8b00845a26bb001d0e9bafd81e195e634 100644 (file)
--- 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 91bf1905a0129d91c52477e32b839c6ba39f45b3..0003349b338d8859548d5f928eed59a4cc9e6442 100644 (file)
--- 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 adbe515077551713c34d1292c29df7b07f05e102..5808c4ec736013ece837f7840fcd109901b50760 100644 (file)
--- 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 2ccbc8a58fe23554404e8aab75e938a9909094d8..81c49e1e39e3bd1e00bd333450dfde42c0242033 100644 (file)
--- 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 4c113c84b7ef010b37c47f97cabd045366495629..62c0bc224895475e5b598f1271dd7a566f9d68ad 100644 (file)
--- 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 4c9bdadd58ae7c06935c53ba6ff05c04b51d1692..70e3a88d850f7dc2c0f52bce27844c5abe1f18ee 100644 (file)
--- 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 2fb60cb7237eff6496a85bffc681a2b8dc490250..b09cf1151a7b7ee6d2605fb2247bdb5bcfb21b5e 100644 (file)
--- 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 3094a8d8400ce2dbfaada24847f04f1a30ace846..bdcbe7d592dd51f25accb65885d9473a698f4c10 100644 (file)
--- 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 e86901f9a42fceeea58a02393df26b71d290c1e3..ca028488ace5306558c2c01fb7877f0b756c39f5 100644 (file)
--- 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 f6d032f113dfe3e6ffa5413e8625f0e28f17a418..57f4344c6158ec75dc3e1b83b019027c2d8f48d4 100644 (file)
--- 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 d7e6a758cff0f878a241e7477c87a442b1612f00..76828576ec2db8c04dfbba34dbd7984e50cce62f 100644 (file)
--- 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 c649c9be20eb0b6e7f5a7cc6f0fc5166ae395e15..2cf5e566d729c1d43c1653d6a6837b38ef00e9de 100644 (file)
--- 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 b3958e79e7efe2f2e0c592d2e038b3864a3ec29a..8668b9c271b53ee24c9fe2f06b2a075e889267ce 100644 (file)
--- 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 cac805531c3a67d4bf73972335a9ff879d6fbdad..a8f117062d15483da4be7abdd79af5ea116f7aba 100644 (file)
--- 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 c39ea09ba2ba691f3edd3792f7b00a316c636442..d2ffdbd7c2a003fbf80f61ef21fb935bb452a65f 100644 (file)
--- 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 fd3bd62eb09ff379d446cc0db66fedf616904cec..f57837d058f0156be9f03e96c9eb23dd3564f288 100644 (file)
--- 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 bc2f103d2ee7f0ce643aaaeddc2413fa5c0c95e2..55b4ac58146243244e55ce481a2f05d712106ad3 100644 (file)
--- 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 f7a720436319a822e75dbd521ba5255c36a7a015..76e27f5b006031a449006fc59d12da78205485a3 100644 (file)
--- 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 ae71a1edb6962add18946b15829ba6810e0c06bd..a5ee519f586fbebbd042044f670ef9bb11d76c7e 100644 (file)
--- 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 c2ff1da2389c4052d0f3a86fbdb41962da7be46a..9c2bc9be7fc661ac218eb4f74bfdf01dca3d920f 100644 (file)
--- 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 cf9cbe09282fb9ab62519e4de708ff1d16a67175..16b44d115545818a9798aab246116549c21c1a36 100644 (file)
--- 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 f05e085727cea8ae28c8830068d8dd6e8ce80694..d823e565dc471f5b27aa3f8c570186c4171a9def 100644 (file)
--- 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)