Universe set cardinality for finite types with finite cardinality (#3392)

* rewrote set cardinality for finite-types

* small changes and format

23 files changed, 1087 insertions, 326 deletions

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 48f5b7b35..a1c91c517 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -19,6 +19,7 @@
 #include "expr/node_algorithm.h"
 #include "options/sets_options.h"
 #include "theory/sets/normal_form.h"
+#include "theory/theory_model.h"
 #include "theory/valuation.h"
 
 using namespace std;
@@ -33,8 +34,13 @@ CardinalityExtension::CardinalityExtension(SolverState& s,
                                            eq::EqualityEngine& e,
                                            context::Context* c,
                                            context::UserContext* u)
-    : d_state(s), d_im(im), d_ee(e), d_card_processed(u)
+    : d_state(s),
+      d_im(im),
+      d_ee(e),
+      d_card_processed(u),
+      d_finite_type_constants_processed(false)
 {
+  d_true = NodeManager::currentNM()->mkConst(true);
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
   // we do congruence over cardinality
   d_ee.addFunctionKind(CARD);
@@ -44,6 +50,9 @@ void CardinalityExtension::reset()
 {
   d_eqc_to_card_term.clear();
   d_t_card_enabled.clear();
+  d_finite_type_elements.clear();
+  d_finite_type_slack_elements.clear();
+  d_univProxy.clear();
 }
 void CardinalityExtension::registerTerm(Node n)
 {
@@ -57,20 +66,112 @@ void CardinalityExtension::registerTerm(Node n)
     d_eqc_to_card_term[r] = n;
     registerCardinalityTerm(n[0]);
   }
-  if (tnc.isInterpretedFinite())
+  Trace("sets-card-debug") << "...finished register term" << std::endl;
+}
+
+void CardinalityExtension::checkFiniteTypes()
+{
+  for (std::pair<const TypeNode, bool>& pair : d_t_card_enabled)
   {
-    std::stringstream ss;
-    ss << "ERROR: cannot use cardinality on sets with finite element "
-          "type (term is "
-       << n << ")." << std::endl;
-    throw LogicException(ss.str());
-    // TODO (#1123): extend approach for this case
+    TypeNode type = pair.first;
+    if (pair.second && type.isInterpretedFinite())
+    {
+      checkFiniteType(type);
+    }
+  }
+}
+
+void CardinalityExtension::checkFiniteType(TypeNode& t)
+{
+  Assert(t.isInterpretedFinite());
+  NodeManager* nm = NodeManager::currentNM();
+  // get the universe set (as univset (Set t))
+  Node univ = d_state.getUnivSet(nm->mkSetType(t));
+  std::map<Node, Node>::iterator it = d_univProxy.find(univ);
+  Node proxy;
+  if (it == d_univProxy.end())
+  {
+    // Force cvc4 to build the cardinality graph for the universe set
+    proxy = d_state.getProxy(univ);
+    d_univProxy[univ] = proxy;
+  }
+  else
+  {
+    proxy = it->second;
+  }
+
+  // get all equivalent classes of type t
+  vector<Node> representatives = d_state.getSetsEqClasses(t);
+  // get the cardinality of the finite type t
+  Cardinality card = t.getCardinality();
+  if (!card.isFinite())
+  {
+    // TODO (#1123): support uninterpreted sorts with --finite-model-find
+    std::stringstream message;
+    message << "The cardinality " << card << " of the finite type " << t
+            << " is not supported yet." << endl;
+    Assert(false) << message.str().c_str();
+  }
+
+  Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality()));
+
+  Node cardUniv = nm->mkNode(kind::CARD, proxy);
+  Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality);
+
+  // (=> true (<= (card (as univset t)) cardUniv)
+  if (!d_state.isEntailed(leq, true))
+  {
+    d_im.assertInference(leq, d_true, "finite type cardinality", 1);
+  }
+
+  // add subset lemmas for sets, and membership lemmas for negative members
+  for (Node& representative : representatives)
+  {
+    // the universe set is a subset of itself
+    if (representative != d_ee.getRepresentative(univ))
+    {
+      // here we only add representatives with variables to avoid adding
+      // infinite equivalent generated terms to the cardinality graph
+      Node variable = d_state.getVariableSet(representative);
+      if (variable.isNull())
+      {
+        continue;
+      }
+
+      // (=> true (subset representative (as univset t))
+      Node subset = nm->mkNode(kind::SUBSET, variable, proxy);
+      // subset terms are rewritten as union terms: (subset A B) implies (=
+      // (union A B) B)
+      subset = Rewriter::rewrite(subset);
+      if (!d_state.isEntailed(subset, true))
+      {
+        d_im.assertInference(subset, d_true, "univset is a super set", 1);
+      }
+
+      // negative members are members in the universe set
+      const std::map<Node, Node>& negativeMembers =
+          d_state.getNegativeMembers(representative);
+
+      for (const std::pair<Node, Node>& negativeMember : negativeMembers)
+      {
+        Node member = nm->mkNode(MEMBER, negativeMember.first, univ);
+        // negativeMember.second is the reason for the negative membership and
+        // has kind MEMBER. So we specify the negation as the reason for the
+        // negative membership lemma
+        Node notMember = nm->mkNode(NOT, negativeMember.second);
+        // (=>
+        //    (not (member negativeMember representative)))
+        //    (member negativeMember (as univset t)))
+        d_im.assertInference(
+            member, notMember, "negative members are in the universe", 1);
+      }
+    }
   }
-  Trace("sets-card-debug") << "...finished register term" << std::endl;
 }
 
 void CardinalityExtension::check()
 {
+  checkFiniteTypes();
   checkRegister();
   if (d_im.hasProcessed())
   {
@@ -858,7 +959,8 @@ void CardinalityExtension::mkModelValueElementsFor(
     Valuation& val,
     Node eqc,
     std::vector<Node>& els,
-    const std::map<Node, Node>& mvals)
+    const std::map<Node, Node>& mvals,
+    TheoryModel* model)
 {
   TypeNode elementType = eqc.getType().getSetElementType();
   if (isModelValueBasic(eqc))
@@ -875,9 +977,37 @@ void CardinalityExtension::mkModelValueElementsFor(
       unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
       Assert(els.size() <= vu);
       NodeManager* nm = NodeManager::currentNM();
+      if (elementType.isInterpretedFinite())
+      {
+        // get all members of this finite type
+        collectFiniteTypeSetElements(model);
+      }
       while (els.size() < vu)
       {
-        els.push_back(nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType)));
+        if (elementType.isInterpretedFinite())
+        {
+          // At this point we are sure the formula is satisfiable and all
+          // cardinality constraints are satisfied. Since this type is finite,
+          // there is only one single cardinality graph for all sets of this
+          // type because the universe cardinality constraint has been added by
+          // CardinalityExtension::checkFiniteType. This means we have enough
+          // slack elements of this finite type for all disjoint leaves in the
+          // cardinality graph. Therefore we can safely add new distinct slack
+          // elements for the leaves without worrying about conflicts with the
+          // current members of this finite type.
+
+          Node slack = nm->mkSkolem("slack", elementType);
+          Node singleton = nm->mkNode(SINGLETON, slack);
+          els.push_back(singleton);
+          d_finite_type_slack_elements[elementType].push_back(slack);
+          Trace("sets-model") << "Added slack element " << slack << " to set "
+                              << eqc << std::endl;
+        }
+        else
+        {
+          els.push_back(
+              nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType)));
+        }
       }
     }
     else
@@ -906,6 +1036,44 @@ void CardinalityExtension::mkModelValueElementsFor(
   }
 }
 
+void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
+{
+  if (d_finite_type_constants_processed)
+  {
+    return;
+  }
+  for (const Node& set : getOrderedSetsEqClasses())
+  {
+    if (!set.getType().isInterpretedFinite())
+    {
+      continue;
+    }
+    if (!isModelValueBasic(set))
+    {
+      // only consider leaves in the cardinality graph
+      continue;
+    }
+    for (const std::pair<const Node, Node>& pair : d_state.getMembers(set))
+    {
+      Node member = pair.first;
+      Node modelRepresentative = model->getRepresentative(member);
+      std::vector<Node>& elements = d_finite_type_elements[member.getType()];
+      if (std::find(elements.begin(), elements.end(), modelRepresentative)
+          == elements.end())
+      {
+        elements.push_back(modelRepresentative);
+      }
+    }
+  }
+  d_finite_type_constants_processed = true;
+}
+
+const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers(
+    TypeNode typeNode)
+{
+  return d_finite_type_elements[typeNode];
+}
+
 }  // namespace sets
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index d9c5dd64a..bf9c5eeaa 100644
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -21,6 +21,7 @@
 #include "context/context.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/solver_state.h"
+#include "theory/type_set.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
@@ -124,7 +125,8 @@ class CardinalityExtension
   void mkModelValueElementsFor(Valuation& v,
                                Node eqc,
                                std::vector<Node>& els,
-                               const std::map<Node, Node>& mvals);
+                               const std::map<Node, Node>& mvals,
+                               TheoryModel* model);
   /** get ordered sets equivalence classes
    *
    * Get the ordered set of equivalence classes computed by this class. This
@@ -135,8 +137,26 @@ class CardinalityExtension
    */
   const std::vector<Node>& getOrderedSetsEqClasses() { return d_oSetEqc; }
 
+  /**
+   * get the slack elements generated for each finite type. This function is
+   * called by TheorySetsPrivate::collectModelInfo to ask the TheoryModel to
+   * exclude these slack elements from the members in all sets of that type.
+   */
+  const std::map<TypeNode, std::vector<TNode> >& getFiniteTypeSlackElements()
+      const
+  {
+    return d_finite_type_slack_elements;
+  }
+  /**
+   * get non-slack members in all sets of the given finite type. This function
+   * is called by TheorySetsPrivate::collectModelInfo to specify the exclusion
+   * sets for TheoryModel
+   */
+  const std::vector<Node>& getFiniteTypeMembers(TypeNode typeNode);
+
  private:
   /** constants */
+  Node d_true;
   Node d_zero;
   /** the empty vector */
   std::vector<Node> d_emp_exp;
@@ -302,6 +322,21 @@ class CardinalityExtension
    * function.
    */
   void checkNormalForm(Node eqc, std::vector<Node>& intro_sets);
+
+  /**
+   * add cardinality lemmas for each finite type
+   */
+  void checkFiniteTypes();
+  /**
+   * This function adds the following lemmas for the finite type t for each S
+   * where S is a (a representative) set term of type t, and for each negative
+   * member x not in S 1- (=> true (<= (card (as univset t)) n) where n is the
+   * cardinality of t 2- (=> true (subset S (as univset t)) where S is a set
+   * term of type t 3- (=> (not (member negativeMember S))) (member
+   * negativeMember (as univset t)))
+   */
+  void checkFiniteType(TypeNode& t);
+
   /** element types of sets for which cardinality is enabled */
   std::map<TypeNode, bool> d_t_card_enabled;
   /**
@@ -338,6 +373,32 @@ class CardinalityExtension
    * ( A ^ B ), and (B \ A).
    */
   std::map<Node, Node> d_localBase;
+
+  /**
+   * a map to store proxy nodes for the universe sets of finite types
+   */
+  std::map<Node, Node> d_univProxy;
+
+  /**
+   * collect the elements in all sets of finite types in model, and
+   * store them in the field d_finite_type_elements
+   */
+  void collectFiniteTypeSetElements(TheoryModel* model);
+  /**
+   * a map to store the non-slack elements encountered so far in all finite
+   * types
+   */
+  std::map<TypeNode, std::vector<Node> > d_finite_type_elements;
+  /**
+   * a map to store slack elements in all finite types
+   */
+  std::map<TypeNode, std::vector<TNode> > d_finite_type_slack_elements;
+  /** This boolean determines whether we already collected finite type constants
+   *  present in the current model.
+   *  Default value is false
+   */
+  bool d_finite_type_constants_processed;
+
 }; /* class CardinalityExtension */
 
 }  // namespace sets
diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index ca7c0bf2b..9e695bf56 100644
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -404,7 +404,7 @@ Node SolverState::getProxy(Node n)
 {
   Kind nk = n.getKind();
   if (nk != EMPTYSET && nk != SINGLETON && nk != INTERSECTION && nk != SETMINUS
-      && nk != UNION)
+      && nk != UNION && nk != UNIVERSE_SET)
   {
     return n;
   }
@@ -605,6 +605,19 @@ void SolverState::debugPrintSet(Node s, const char* c) const
   }
 }
 
+const vector<Node> SolverState::getSetsEqClasses(const TypeNode& t) const
+{
+  vector<Node> representatives;
+  for (const Node& eqc : getSetsEqClasses())
+  {
+    if (eqc.getType().getSetElementType() == t)
+    {
+      representatives.push_back(eqc);
+    }
+  }
+  return representatives;
+}
+
 }  // namespace sets
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h
index 7426a701b..5bf20daca 100644
--- a/src/theory/sets/solver_state.h
+++ b/src/theory/sets/solver_state.h
@@ -121,8 +121,13 @@ class SolverState
    * class.
    */
   bool isCongruent(Node n) const;
-  /** Get the list of all equivalence classes of set type */
+
+  /** Get the list of all equivalence classes of set terms */
   const std::vector<Node>& getSetsEqClasses() const { return d_set_eqc; }
+  /** Get the list of all equivalence classes of set terms that have element
+   * type t */
+  const std::vector<Node> getSetsEqClasses(const TypeNode& t) const;
+
   /**
    * Get the list of non-variable sets that exists in the equivalence class
    * whose representative is r.
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 6a381d471..ad9a8cbdb 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -14,9 +14,10 @@
  ** Sets theory implementation.
  **/
 
-#include <algorithm>
 #include "theory/sets/theory_sets_private.h"
 
+#include <algorithm>
+
 #include "expr/emptyset.h"
 #include "expr/node_algorithm.h"
 #include "options/sets_options.h"
@@ -52,9 +53,9 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
       d_rels_enabled(false),
       d_card_enabled(false)
 {
-  d_true = NodeManager::currentNM()->mkConst( true );
-  d_false = NodeManager::currentNM()->mkConst( false );
-  d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
 
   d_equalityEngine.addFunctionKind(kind::SINGLETON);
   d_equalityEngine.addFunctionKind(kind::UNION);
@@ -65,74 +66,92 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_equalityEngine.addFunctionKind(kind::SUBSET);
 }
 
-TheorySetsPrivate::~TheorySetsPrivate(){
-  for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info) {
+TheorySetsPrivate::~TheorySetsPrivate()
+{
+  for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info)
+  {
     delete current_pair.second;
   }
 }
 
-void TheorySetsPrivate::eqNotifyNewClass(TNode t) {
-  if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){
-    EqcInfo * e = getOrMakeEqcInfo( t, true );
+void TheorySetsPrivate::eqNotifyNewClass(TNode t)
+{
+  if (t.getKind() == kind::SINGLETON || t.getKind() == kind::EMPTYSET)
+  {
+    EqcInfo* e = getOrMakeEqcInfo(t, true);
     e->d_singleton = t;
   }
 }
 
-void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){
+void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2) {}
 
-}
-
-void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
+void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2)
+{
   if (!d_state.isInConflict())
   {
-    Trace("sets-prop-debug") << "Merge " << t1 << " and " << t2 << "..." << std::endl;
+    Trace("sets-prop-debug")
+        << "Merge " << t1 << " and " << t2 << "..." << std::endl;
     Node s1, s2;
-    EqcInfo * e2 = getOrMakeEqcInfo( t2 );
-    if( e2 ){
+    EqcInfo* e2 = getOrMakeEqcInfo(t2);
+    if (e2)
+    {
       s2 = e2->d_singleton;
-      EqcInfo * e1 = getOrMakeEqcInfo( t1 );
+      EqcInfo* e1 = getOrMakeEqcInfo(t1);
       Node s1;
       Trace("sets-prop-debug") << "Merging singletons..." << std::endl;
-      if( e1 ){
+      if (e1)
+      {
         s1 = e1->d_singleton;
-        if( !s1.isNull() && !s2.isNull() ){
-          if( s1.getKind()==s2.getKind() ){
-            Trace("sets-prop") << "Propagate eq inference : " << s1 << " == " << s2 << std::endl;
-            //infer equality between elements of singleton
-            Node exp = s1.eqNode( s2 );
-            Node eq = s1[0].eqNode( s2[0] );
-            d_keep.insert( exp );
-            d_keep.insert( eq );
-            assertFact( eq, exp );
-          }else{
-            //singleton equal to emptyset, conflict
-            Trace("sets-prop") << "Propagate conflict : " << s1 << " == " << s2 << std::endl;
-            conflict( s1, s2 );
+        if (!s1.isNull() && !s2.isNull())
+        {
+          if (s1.getKind() == s2.getKind())
+          {
+            Trace("sets-prop") << "Propagate eq inference : " << s1
+                               << " == " << s2 << std::endl;
+            // infer equality between elements of singleton
+            Node exp = s1.eqNode(s2);
+            Node eq = s1[0].eqNode(s2[0]);
+            d_keep.insert(exp);
+            d_keep.insert(eq);
+            assertFact(eq, exp);
+          }
+          else
+          {
+            // singleton equal to emptyset, conflict
+            Trace("sets-prop")
+                << "Propagate conflict : " << s1 << " == " << s2 << std::endl;
+            conflict(s1, s2);
             return;
           }
         }
-      }else{
-        //copy information
-        e1 = getOrMakeEqcInfo( t1, true );
-        e1->d_singleton.set( e2->d_singleton );
+      }
+      else
+      {
+        // copy information
+        e1 = getOrMakeEqcInfo(t1, true);
+        e1->d_singleton.set(e2->d_singleton);
       }
     }
-    //merge membership list
+    // merge membership list
     Trace("sets-prop-debug") << "Copying membership list..." << std::endl;
-    NodeIntMap::iterator mem_i2 = d_members.find( t2 );
-    if( mem_i2 != d_members.end() ) {
-      NodeIntMap::iterator mem_i1 = d_members.find( t1 );
+    NodeIntMap::iterator mem_i2 = d_members.find(t2);
+    if (mem_i2 != d_members.end())
+    {
+      NodeIntMap::iterator mem_i1 = d_members.find(t1);
       int n_members = 0;
-      if( mem_i1 != d_members.end() ) {
+      if (mem_i1 != d_members.end())
+      {
         n_members = (*mem_i1).second;
       }
-      for( int i=0; i<(*mem_i2).second; i++ ){
+      for (int i = 0; i < (*mem_i2).second; i++)
+      {
         Assert(i < (int)d_members_data[t2].size()
                && d_members_data[t2][i].getKind() == kind::MEMBER);
         Node m2 = d_members_data[t2][i];
-        //check if redundant
+        // check if redundant
         bool add = true;
-        for( int j=0; j<n_members; j++ ){
+        for (int j = 0; j < n_members; j++)
+        {
           Assert(j < (int)d_members_data[t1].size()
                  && d_members_data[t1][j].getKind() == kind::MEMBER);
           if (d_state.areEqual(m2[0], d_members_data[t1][j][0]))
@@ -141,30 +160,42 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
             break;
           }
         }
-        if( add ){
-          if( !s1.isNull() && s2.isNull() ){
+        if (add)
+        {
+          if (!s1.isNull() && s2.isNull())
+          {
             Assert(m2[1].getType().isComparableTo(s1.getType()));
             Assert(d_state.areEqual(m2[1], s1));
-            Node exp = NodeManager::currentNM()->mkNode( kind::AND, m2[1].eqNode( s1 ), m2 );
-            if( s1.getKind()==kind::SINGLETON ){
-              if( s1[0]!=m2[0] ){
-                Node eq = s1[0].eqNode( m2[0] );
-                d_keep.insert( exp );
-                d_keep.insert( eq );
-                Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp << " => " << eq << std::endl;
-                assertFact( eq, exp );
+            Node exp = NodeManager::currentNM()->mkNode(
+                kind::AND, m2[1].eqNode(s1), m2);
+            if (s1.getKind() == kind::SINGLETON)
+            {
+              if (s1[0] != m2[0])
+              {
+                Node eq = s1[0].eqNode(m2[0]);
+                d_keep.insert(exp);
+                d_keep.insert(eq);
+                Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
+                                   << " => " << eq << std::endl;
+                assertFact(eq, exp);
               }
-            }else{
-              //conflict
-              Trace("sets-prop") << "Propagate eq-mem conflict : " << exp << std::endl;
+            }
+            else
+            {
+              // conflict
+              Trace("sets-prop")
+                  << "Propagate eq-mem conflict : " << exp << std::endl;
               d_state.setConflict(exp);
               return;
             }
           }
-          if( n_members<(int)d_members_data[t1].size() ){
+          if (n_members < (int)d_members_data[t1].size())
+          {
             d_members_data[t1][n_members] = m2;
-          }else{
-            d_members_data[t1].push_back( m2 );
+          }
+          else
+          {
+            d_members_data[t1].push_back(m2);
           }
           n_members++;
         }
@@ -174,52 +205,69 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
   }
 }
 
-void TheorySetsPrivate::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
-  if( t1.getType().isSet() ){
-    Node eq = t1.eqNode( t2 );
-    if( d_deq.find( eq )==d_deq.end() ){
+void TheorySetsPrivate::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+{
+  if (t1.getType().isSet())
+  {
+    Node eq = t1.eqNode(t2);
+    if (d_deq.find(eq) == d_deq.end())
+    {
       d_deq[eq] = true;
     }
   }
 }
 
-TheorySetsPrivate::EqcInfo::EqcInfo( context::Context* c ) : d_singleton( c ){
-  
-}
+TheorySetsPrivate::EqcInfo::EqcInfo(context::Context* c) : d_singleton(c) {}
 
-TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo( TNode n, bool doMake ){
-  std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
-  if( eqc_i==d_eqc_info.end() ){
+TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo(TNode n,
+                                                                bool doMake)
+{
+  std::map<Node, EqcInfo*>::iterator eqc_i = d_eqc_info.find(n);
+  if (eqc_i == d_eqc_info.end())
+  {
     EqcInfo* ei = NULL;
-    if( doMake ){
-      ei = new EqcInfo( d_external.getSatContext() );
+    if (doMake)
+    {
+      ei = new EqcInfo(d_external.getSatContext());
       d_eqc_info[n] = ei;
     }
     return ei;
-  }else{
+  }
+  else
+  {
     return eqc_i->second;
   }
 }
 
 bool TheorySetsPrivate::areCareDisequal(Node a, Node b)
 {
-  if( d_equalityEngine.isTriggerTerm(a, THEORY_SETS) && d_equalityEngine.isTriggerTerm(b, THEORY_SETS) ){
-    TNode a_shared = d_equalityEngine.getTriggerTermRepresentative(a, THEORY_SETS);
-    TNode b_shared = d_equalityEngine.getTriggerTermRepresentative(b, THEORY_SETS);
-    EqualityStatus eqStatus = d_external.d_valuation.getEqualityStatus(a_shared, b_shared);
-    if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
+  if (d_equalityEngine.isTriggerTerm(a, THEORY_SETS)
+      && d_equalityEngine.isTriggerTerm(b, THEORY_SETS))
+  {
+    TNode a_shared =
+        d_equalityEngine.getTriggerTermRepresentative(a, THEORY_SETS);
+    TNode b_shared =
+        d_equalityEngine.getTriggerTermRepresentative(b, THEORY_SETS);
+    EqualityStatus eqStatus =
+        d_external.d_valuation.getEqualityStatus(a_shared, b_shared);
+    if (eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE
+        || eqStatus == EQUALITY_FALSE_IN_MODEL)
+    {
       return true;
     }
   }
   return false;
 }
 
-bool TheorySetsPrivate::isMember( Node x, Node s ) {
+bool TheorySetsPrivate::isMember(Node x, Node s)
+{
   Assert(d_equalityEngine.hasTerm(s)
          && d_equalityEngine.getRepresentative(s) == s);
-  NodeIntMap::iterator mem_i = d_members.find( s );
-  if( mem_i != d_members.end() ) {
-    for( int i=0; i<(*mem_i).second; i++ ){
+  NodeIntMap::iterator mem_i = d_members.find(s);
+  if (mem_i != d_members.end())
+  {
+    for (int i = 0; i < (*mem_i).second; i++)
+    {
       if (d_state.areEqual(d_members_data[s][i][0], x))
       {
         return true;
@@ -228,53 +276,71 @@ bool TheorySetsPrivate::isMember( Node x, Node s ) {
   }
   return false;
 }
-        
-bool TheorySetsPrivate::assertFact( Node fact, Node exp ){
-  Trace("sets-assert") << "TheorySets::assertFact : " << fact << ", exp = " << exp << std::endl;
+
+bool TheorySetsPrivate::assertFact(Node fact, Node exp)
+{
+  Trace("sets-assert") << "TheorySets::assertFact : " << fact
+                       << ", exp = " << exp << std::endl;
   bool polarity = fact.getKind() != kind::NOT;
   TNode atom = polarity ? fact : fact[0];
   if (!d_state.isEntailed(atom, polarity))
   {
-    if( atom.getKind()==kind::EQUAL ){
-      d_equalityEngine.assertEquality( atom, polarity, exp );
-    }else{
-      d_equalityEngine.assertPredicate( atom, polarity, exp );
+    if (atom.getKind() == kind::EQUAL)
+    {
+      d_equalityEngine.assertEquality(atom, polarity, exp);
+    }
+    else
+    {
+      d_equalityEngine.assertPredicate(atom, polarity, exp);
     }
     if (!d_state.isInConflict())
     {
-      if( atom.getKind()==kind::MEMBER && polarity ){
-        //check if set has a value, if so, we can propagate
-        Node r = d_equalityEngine.getRepresentative( atom[1] );
-        EqcInfo * e = getOrMakeEqcInfo( r, true );
-        if( e ){
+      if (atom.getKind() == kind::MEMBER && polarity)
+      {
+        // check if set has a value, if so, we can propagate
+        Node r = d_equalityEngine.getRepresentative(atom[1]);
+        EqcInfo* e = getOrMakeEqcInfo(r, true);
+        if (e)
+        {
           Node s = e->d_singleton;
-          if( !s.isNull() ){
-            Node exp = NodeManager::currentNM()->mkNode( kind::AND, atom, atom[1].eqNode( s ) );
-            d_keep.insert( exp );
-            if( s.getKind()==kind::SINGLETON ){
-              if( s[0]!=atom[0] ){
+          if (!s.isNull())
+          {
+            Node exp = NodeManager::currentNM()->mkNode(
+                kind::AND, atom, atom[1].eqNode(s));
+            d_keep.insert(exp);
+            if (s.getKind() == kind::SINGLETON)
+            {
+              if (s[0] != atom[0])
+              {
                 Trace("sets-prop") << "Propagate mem-eq : " << exp << std::endl;
-                Node eq = s[0].eqNode( atom[0] );
-                d_keep.insert( eq );
-                assertFact( eq, exp ); 
+                Node eq = s[0].eqNode(atom[0]);
+                d_keep.insert(eq);
+                assertFact(eq, exp);
               }
-            }else{
-              Trace("sets-prop") << "Propagate mem-eq conflict : " << exp << std::endl;
+            }
+            else
+            {
+              Trace("sets-prop")
+                  << "Propagate mem-eq conflict : " << exp << std::endl;
               d_state.setConflict(exp);
             }
           }
         }
-        //add to membership list
-        NodeIntMap::iterator mem_i = d_members.find( r );
+        // add to membership list
+        NodeIntMap::iterator mem_i = d_members.find(r);
         int n_members = 0;
-        if( mem_i != d_members.end() ) {
+        if (mem_i != d_members.end())
+        {
           n_members = (*mem_i).second;
         }
         d_members[r] = n_members + 1;
-        if( n_members<(int)d_members_data[r].size() ){
+        if (n_members < (int)d_members_data[r].size())
+        {
           d_members_data[r][n_members] = atom;
-        }else{
-          d_members_data[r].push_back( atom );
+        }
+        else
+        {
+          d_members_data[r].push_back(atom);
         }
       }
     }
@@ -302,44 +368,52 @@ void TheorySetsPrivate::fullEffortReset()
   d_cardSolver->reset();
 }
 
-void TheorySetsPrivate::fullEffortCheck(){
+void TheorySetsPrivate::fullEffortCheck()
+{
   Trace("sets") << "----- Full effort check ------" << std::endl;
-  do{
+  do
+  {
     Trace("sets") << "...iterate full effort check..." << std::endl;
     fullEffortReset();
 
     Trace("sets-eqc") << "Equality Engine:" << std::endl;
     std::map<TypeNode, unsigned> eqcTypeCount;
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-    while( !eqcs_i.isFinished() ){
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(&d_equalityEngine);
+    while (!eqcs_i.isFinished())
+    {
       Node eqc = (*eqcs_i);
       bool isSet = false;
       TypeNode tn = eqc.getType();
       d_state.registerEqc(tn, eqc);
       eqcTypeCount[tn]++;
-      //common type node and term
+      // common type node and term
       TypeNode tnc;
       Node tnct;
-      if( tn.isSet() ){
+      if (tn.isSet())
+      {
         isSet = true;
         tnc = tn.getSetElementType();
         tnct = eqc;
       }
       Trace("sets-eqc") << "[" << eqc << "] : ";
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
-      while( !eqc_i.isFinished() ) {
+      eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, &d_equalityEngine);
+      while (!eqc_i.isFinished())
+      {
         Node n = (*eqc_i);
-        if( n!=eqc ){
+        if (n != eqc)
+        {
           Trace("sets-eqc") << n << " ";
         }
         TypeNode tnn = n.getType();
-        if( isSet ){
+        if (isSet)
+        {
           Assert(tnn.isSet());
           TypeNode tnnel = tnn.getSetElementType();
-          tnc = TypeNode::mostCommonTypeNode( tnc, tnnel );
+          tnc = TypeNode::mostCommonTypeNode(tnc, tnnel);
           Assert(!tnc.isNull());
-          //update the common type term
-          if( tnc==tnnel ){
+          // update the common type term
+          if (tnc == tnnel)
+          {
             tnct = n;
           }
         }
@@ -353,23 +427,34 @@ void TheorySetsPrivate::fullEffortCheck(){
           // if we do not handle the kind, set incomplete
           Kind nk = n[0].getKind();
           // some kinds of cardinality we cannot handle
-          if (nk == kind::UNIVERSE_SET || d_rels->isRelationKind(nk))
+          if ((nk == kind::UNIVERSE_SET
+               && !n[0].getType().isInterpretedFinite())
+              || d_rels->isRelationKind(nk))
           {
             d_full_check_incomplete = true;
             Trace("sets-incomplete")
                 << "Sets : incomplete because of " << n << "." << std::endl;
-            // TODO (#1124) handle this case
+            // TODO (#1124):  The issue can be divided into 4 parts
+            // 1- Supporting the universe cardinality for finite types with
+            // finite cardinality (done) 2- Supporting the universe cardinality
+            // for for uninterpreted sorts with finite-model-find (pending)
+            //    See the implementation of
+            //    CardinalityExtension::checkFiniteType
+            // 3- Supporting the universe cardinality for non-finite types
+            // (pending, easy) 4- Supporting cardinality for relations (hard)
           }
         }
         else
         {
-          if( d_rels->isRelationKind( n.getKind() ) ){
+          if (d_rels->isRelationKind(n.getKind()))
+          {
             d_rels_enabled = true;
           }
         }
         ++eqc_i;
       }
-      if( isSet ){
+      if (isSet)
+      {
         Assert(tnct.getType().getSetElementType() == tnc);
         d_most_common_type[eqc] = tnc;
         d_most_common_type_term[eqc] = tnct;
@@ -394,7 +479,8 @@ void TheorySetsPrivate::fullEffortCheck(){
     // e.g. the cardinality solver.
     if (!d_im.hasProcessed())
     {
-      if( Trace.isOn("sets-mem") ){
+      if (Trace.isOn("sets-mem"))
+      {
         const std::vector<Node>& sec = d_state.getSetsEqClasses();
         for (const Node& s : sec)
         {
@@ -421,7 +507,8 @@ void TheorySetsPrivate::fullEffortCheck(){
       if (!d_im.hasProcessed())
       {
         checkDownwardsClosure();
-        if( options::setsInferAsLemmas() ){
+        if (options::setsInferAsLemmas())
+        {
           d_im.flushPendingLemmas();
         }
         if (!d_im.hasProcessed())
@@ -482,7 +569,7 @@ void TheorySetsPrivate::checkSubtypes()
           Node mctt = d_most_common_type_term[s];
           Assert(!mctt.isNull());
           Trace("sets") << "    most common type term is " << mctt << std::endl;
-          std::vector< Node > exp;
+          std::vector<Node> exp;
           exp.push_back(it2.second);
           Assert(d_state.areEqual(mctt, it2.second[1]));
           exp.push_back(mctt.eqNode(it2.second[1]));
@@ -506,7 +593,7 @@ void TheorySetsPrivate::checkSubtypes()
 void TheorySetsPrivate::checkDownwardsClosure()
 {
   Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl;
-  //downwards closure
+  // downwards closure
   const std::vector<Node>& sec = d_state.getSetsEqClasses();
   for (const Node& s : sec)
   {
@@ -523,33 +610,42 @@ void TheorySetsPrivate::checkDownwardsClosure()
             Node mem = it2.second;
             Node eq_set = nv;
             Assert(d_equalityEngine.areEqual(mem[1], eq_set));
-            if( mem[1]!=eq_set ){
-              Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl;
-              if( !options::setsProxyLemmas() ){
-                Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
-                nmem = Rewriter::rewrite( nmem );
-                std::vector< Node > exp;
-                exp.push_back( mem );
-                exp.push_back( mem[1].eqNode( eq_set ) );
+            if (mem[1] != eq_set)
+            {
+              Trace("sets-debug") << "Downwards closure based on " << mem
+                                  << ", eq_set = " << eq_set << std::endl;
+              if (!options::setsProxyLemmas())
+              {
+                Node nmem = NodeManager::currentNM()->mkNode(
+                    kind::MEMBER, mem[0], eq_set);
+                nmem = Rewriter::rewrite(nmem);
+                std::vector<Node> exp;
+                exp.push_back(mem);
+                exp.push_back(mem[1].eqNode(eq_set));
                 d_im.assertInference(nmem, exp, "downc");
                 if (d_state.isInConflict())
                 {
                   return;
                 }
-              }else{
-                //use proxy set
+              }
+              else
+              {
+                // use proxy set
                 Node k = d_state.getProxy(eq_set);
-                Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k );
-                Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
-                nmem = Rewriter::rewrite( nmem );
-                std::vector< Node > exp;
+                Node pmem =
+                    NodeManager::currentNM()->mkNode(kind::MEMBER, mem[0], k);
+                Node nmem = NodeManager::currentNM()->mkNode(
+                    kind::MEMBER, mem[0], eq_set);
+                nmem = Rewriter::rewrite(nmem);
+                std::vector<Node> exp;
                 if (d_state.areEqual(mem, pmem))
                 {
-                  exp.push_back( pmem );
+                  exp.push_back(pmem);
                 }
                 else
                 {
-                  nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem );
+                  nmem = NodeManager::currentNM()->mkNode(
+                      kind::OR, pmem.negate(), nmem);
                 }
                 d_im.assertInference(nmem, exp, "downc");
               }
@@ -563,7 +659,7 @@ void TheorySetsPrivate::checkDownwardsClosure()
 
 void TheorySetsPrivate::checkUpwardsClosure()
 {
-  //upwards closure
+  // upwards closure
   NodeManager* nm = NodeManager::currentNM();
   const std::map<Kind, std::map<Node, std::map<Node, Node> > >& boi =
       d_state.getBinaryOpIndex();
@@ -576,7 +672,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
     for (const std::pair<const Node, std::map<Node, Node> >& it : itb.second)
     {
       Node r1 = it.first;
-      //see if there are members in first argument r1
+      // see if there are members in first argument r1
       const std::map<Node, Node>& r1mem = d_state.getMembers(r1);
       if (!r1mem.empty() || k == kind::UNION)
       {
@@ -584,7 +680,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
         {
           Node r2 = it2.first;
           Node term = it2.second;
-          //see if there are members in second argument
+          // 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::INTERSECTION)
@@ -592,7 +688,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
             Trace("sets-debug")
                 << "Checking " << term << ", members = " << (!r1mem.empty())
                 << ", " << (!r2mem.empty()) << std::endl;
-            //for all members of r1
+            // for all members of r1
             if (!r1mem.empty())
             {
               for (const std::pair<const Node, Node>& itm1m : r1mem)
@@ -601,14 +697,17 @@ void TheorySetsPrivate::checkUpwardsClosure()
                 Node x = itm1m.second[0];
                 Trace("sets-debug") << "checking membership " << xr << " "
                                     << itm1m.second << std::endl;
-                std::vector< Node > exp;
+                std::vector<Node> exp;
                 exp.push_back(itm1m.second);
                 d_state.addEqualityToExp(term[0], itm1m.second[1], exp);
                 bool valid = false;
                 int inferType = 0;
-                if( k==kind::UNION ){
+                if (k == kind::UNION)
+                {
                   valid = true;
-                }else if( k==kind::INTERSECTION ){
+                }
+                else if (k == kind::INTERSECTION)
+                {
                   // conclude x is in term
                   // if also existing in members of r2
                   std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
@@ -621,7 +720,8 @@ void TheorySetsPrivate::checkUpwardsClosure()
                   }
                   else
                   {
-                    // if not, check whether it is definitely not a member, if unknown, split
+                    // if not, check whether it is definitely not a member, if
+                    // unknown, split
                     if (r2nmem.find(xr) == r2nmem.end())
                     {
                       exp.push_back(nm->mkNode(kind::MEMBER, x, term[1]));
@@ -629,7 +729,9 @@ void TheorySetsPrivate::checkUpwardsClosure()
                       inferType = 1;
                     }
                   }
-                }else{
+                }
+                else
+                {
                   Assert(k == kind::SETMINUS);
                   std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
                   if (itm == r2mem.end())
@@ -642,9 +744,11 @@ void TheorySetsPrivate::checkUpwardsClosure()
                     inferType = 1;
                   }
                 }
-                if( valid ){
+                if (valid)
+                {
                   Node rr = d_equalityEngine.getRepresentative(term);
-                  if( !isMember( x, rr ) ){
+                  if (!isMember(x, rr))
+                  {
                     Node kk = d_state.getProxy(term);
                     Node fact = nm->mkNode(kind::MEMBER, x, kk);
                     d_im.assertInference(fact, exp, "upc", inferType);
@@ -658,16 +762,18 @@ void TheorySetsPrivate::checkUpwardsClosure()
                                     << itm1m.second << std::endl;
               }
             }
-            if( k==kind::UNION ){
+            if (k == kind::UNION)
+            {
               if (!r2mem.empty())
               {
-                //for all members of r2
+                // for all members of r2
                 for (const std::pair<const Node, Node>& itm2m : r2mem)
                 {
                   Node x = itm2m.second[0];
                   Node rr = d_equalityEngine.getRepresentative(term);
-                  if( !isMember( x, rr ) ){
-                    std::vector< Node > exp;
+                  if (!isMember(x, rr))
+                  {
+                    std::vector<Node> exp;
                     exp.push_back(itm2m.second);
                     d_state.addEqualityToExp(term[1], itm2m.second[1], exp);
                     Node k = d_state.getProxy(term);
@@ -688,40 +794,46 @@ void TheorySetsPrivate::checkUpwardsClosure()
   }
   if (!d_im.hasProcessed())
   {
-    if( options::setsExt() ){
-      //universal sets
+    if (options::setsExt())
+    {
+      // universal sets
       Trace("sets-debug") << "Check universe sets..." << std::endl;
-      //all elements must be in universal set
+      // all elements must be in universal set
       const std::vector<Node>& sec = d_state.getSetsEqClasses();
       for (const Node& s : sec)
       {
-        //if equivalence class contains a variable
+        // if equivalence class contains a variable
         Node v = d_state.getVariableSet(s);
         if (!v.isNull())
         {
-          //the variable in the equivalence class
-          std::map< TypeNode, Node > univ_set;
+          // the variable in the equivalence class
+          std::map<TypeNode, Node> univ_set;
           const std::map<Node, Node>& smems = d_state.getMembers(s);
           for (const std::pair<const Node, Node>& it2 : smems)
           {
             Node e = it2.second[0];
-            TypeNode tn = NodeManager::currentNM()->mkSetType( e.getType() );
+            TypeNode tn = NodeManager::currentNM()->mkSetType(e.getType());
             Node u;
-            std::map< TypeNode, Node >::iterator itu = univ_set.find( tn );
-            if( itu==univ_set.end() ){
+            std::map<TypeNode, Node>::iterator itu = univ_set.find(tn);
+            if (itu == univ_set.end())
+            {
               Node ueqc = d_state.getUnivSetEqClass(tn);
-              // if the universe does not yet exist, or is not in this equivalence class
+              // if the universe does not yet exist, or is not in this
+              // equivalence class
               if (s != ueqc)
               {
                 u = d_state.getUnivSet(tn);
               }
               univ_set[tn] = u;
-            }else{
+            }
+            else
+            {
               u = itu->second;
             }
-            if( !u.isNull() ){
+            if (!u.isNull())
+            {
               Assert(it2.second.getKind() == kind::MEMBER);
-              std::vector< Node > exp;
+              std::vector<Node> exp;
               exp.push_back(it2.second);
               if (v != it2.second[1])
               {
@@ -743,10 +855,11 @@ void TheorySetsPrivate::checkUpwardsClosure()
 
 void TheorySetsPrivate::checkDisequalities()
 {
-  //disequalities
+  // disequalities
   Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl;
   NodeManager* nm = NodeManager::currentNM();
-  for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) {
+  for (NodeBoolMap::const_iterator it = d_deq.begin(); it != d_deq.end(); ++it)
+  {
     if (!(*it).second)
     {
       // not active
@@ -832,9 +945,11 @@ void TheorySetsPrivate::checkReduceComprehensions()
 /**************************** TheorySetsPrivate *****************************/
 /**************************** TheorySetsPrivate *****************************/
 
-void TheorySetsPrivate::check(Theory::Effort level) {
+void TheorySetsPrivate::check(Theory::Effort level)
+{
   Trace("sets-check") << "Sets check effort " << level << std::endl;
-  if( level == Theory::EFFORT_LAST_CALL ){
+  if (level == Theory::EFFORT_LAST_CALL)
+  {
     return;
   }
   while (!d_external.done() && !d_state.isInConflict())
@@ -843,15 +958,18 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     Assertion assertion = d_external.get();
     TNode fact = assertion.assertion;
     Trace("sets-assert") << "Assert from input " << fact << std::endl;
-    //assert the fact
-    assertFact( fact, fact );
+    // assert the fact
+    assertFact(fact, fact);
   }
-  Trace("sets-check") << "Sets finished assertions effort " << level << std::endl;
-  //invoke full effort check, relations check
+  Trace("sets-check") << "Sets finished assertions effort " << level
+                      << std::endl;
+  // invoke full effort check, relations check
   if (!d_state.isInConflict())
   {
-    if( level == Theory::EFFORT_FULL ){
-      if( !d_external.d_valuation.needCheck() ){
+    if (level == Theory::EFFORT_FULL)
+    {
+      if (!d_external.d_valuation.needCheck())
+      {
         fullEffortCheck();
         if (!d_state.isInConflict() && !d_im.hasSentLemma()
             && d_full_check_incomplete)
@@ -862,13 +980,14 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     }
   }
   Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
-}/* TheorySetsPrivate::check() */
+} /* TheorySetsPrivate::check() */
 
 /************************ Sharing ************************/
 /************************ Sharing ************************/
 /************************ Sharing ************************/
 
-void TheorySetsPrivate::addSharedTerm(TNode n) {
+void TheorySetsPrivate::addSharedTerm(TNode n)
+{
   Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n << ")"
                 << std::endl;
   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
@@ -880,74 +999,98 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
                                      unsigned depth,
                                      unsigned& n_pairs)
 {
-  if( depth==arity ){
-    if( t2!=NULL ){
+  if (depth == arity)
+  {
+    if (t2 != NULL)
+    {
       Node f1 = t1->getData();
       Node f2 = t2->getData();
       if (!d_state.areEqual(f1, f2))
       {
         Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
-        vector< pair<TNode, TNode> > currentPairs;
-        for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
+        vector<pair<TNode, TNode> > currentPairs;
+        for (unsigned k = 0; k < f1.getNumChildren(); ++k)
+        {
           TNode x = f1[k];
           TNode y = f2[k];
           Assert(d_equalityEngine.hasTerm(x));
           Assert(d_equalityEngine.hasTerm(y));
           Assert(!d_state.areDisequal(x, y));
           Assert(!areCareDisequal(x, y));
-          if( !d_equalityEngine.areEqual( x, y ) ){
-            Trace("sets-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
-            if( d_equalityEngine.isTriggerTerm(x, THEORY_SETS) && d_equalityEngine.isTriggerTerm(y, THEORY_SETS) ){
-              TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_SETS);
-              TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_SETS);
+          if (!d_equalityEngine.areEqual(x, y))
+          {
+            Trace("sets-cg")
+                << "Arg #" << k << " is " << x << " " << y << std::endl;
+            if (d_equalityEngine.isTriggerTerm(x, THEORY_SETS)
+                && d_equalityEngine.isTriggerTerm(y, THEORY_SETS))
+            {
+              TNode x_shared =
+                  d_equalityEngine.getTriggerTermRepresentative(x, THEORY_SETS);
+              TNode y_shared =
+                  d_equalityEngine.getTriggerTermRepresentative(y, THEORY_SETS);
               currentPairs.push_back(make_pair(x_shared, y_shared));
-            }else if( isCareArg( f1, k ) && isCareArg( f2, k ) ){
-              //splitting on sets (necessary for handling set of sets properly)
-              if( x.getType().isSet() ){
+            }
+            else if (isCareArg(f1, k) && isCareArg(f2, k))
+            {
+              // splitting on sets (necessary for handling set of sets properly)
+              if (x.getType().isSet())
+              {
                 Assert(y.getType().isSet());
                 if (!d_state.areDisequal(x, y))
                 {
-                  Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl;
+                  Trace("sets-cg-lemma")
+                      << "Should split on : " << x << "==" << y << std::endl;
                   d_im.split(x.eqNode(y));
                 }
               }
             }
           }
         }
-        for (unsigned c = 0; c < currentPairs.size(); ++ c) {
-          Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
+        for (unsigned c = 0; c < currentPairs.size(); ++c)
+        {
+          Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " "
+                                << currentPairs[c].second << std::endl;
           d_external.addCarePair(currentPairs[c].first, currentPairs[c].second);
           n_pairs++;
         }
       }
     }
-  }else{
-    if( t2==NULL ){
-      if( depth<(arity-1) ){
-        //add care pairs internal to each child
+  }
+  else
+  {
+    if (t2 == NULL)
+    {
+      if (depth < (arity - 1))
+      {
+        // add care pairs internal to each child
         for (std::pair<const TNode, TNodeTrie>& t : t1->d_data)
         {
           addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs);
         }
       }
-      //add care pairs based on each pair of non-disequal arguments
+      // add care pairs based on each pair of non-disequal arguments
       for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
            it != t1->d_data.end();
            ++it)
       {
         std::map<TNode, TNodeTrie>::iterator it2 = it;
         ++it2;
-        for( ; it2 != t1->d_data.end(); ++it2 ){
-          if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+        for (; it2 != t1->d_data.end(); ++it2)
+        {
+          if (!d_equalityEngine.areDisequal(it->first, it2->first, false))
+          {
             if (!areCareDisequal(it->first, it2->first))
             {
-              addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+              addCarePairs(
+                  &it->second, &it2->second, arity, depth + 1, n_pairs);
             }
           }
         }
       }
-    }else{
-      //add care pairs based on product of indices, non-disequal arguments
+    }
+    else
+    {
+      // add care pairs based on product of indices, non-disequal arguments
       for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
       {
         for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
@@ -965,7 +1108,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
   }
 }
 
-void TheorySetsPrivate::computeCareGraph() {
+void TheorySetsPrivate::computeCareGraph()
+{
   const std::map<Kind, std::vector<Node> >& ol = d_state.getOperatorList();
   for (const std::pair<const Kind, std::vector<Node> >& it : ol)
   {
@@ -978,32 +1122,39 @@ void TheorySetsPrivate::computeCareGraph() {
       Trace("sets-cg") << "Build index for " << k << "..." << std::endl;
       std::map<TypeNode, TNodeTrie> index;
       unsigned arity = 0;
-      //populate indices
+      // populate indices
       for (TNode f1 : it.second)
       {
         Assert(d_equalityEngine.hasTerm(f1));
         Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
         Assert(d_equalityEngine.hasTerm(f1));
-        //break into index based on operator, and type of first argument (since some operators are parametric)
+        // break into index based on operator, and type of first argument (since
+        // some operators are parametric)
         TypeNode tn = f1[0].getType();
-        std::vector< TNode > reps;
+        std::vector<TNode> reps;
         bool hasCareArg = false;
-        for( unsigned j=0; j<f1.getNumChildren(); j++ ){
-          reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
-          if( isCareArg( f1, j ) ){
+        for (unsigned j = 0; j < f1.getNumChildren(); j++)
+        {
+          reps.push_back(d_equalityEngine.getRepresentative(f1[j]));
+          if (isCareArg(f1, j))
+          {
             hasCareArg = true;
           }
         }
-        if( hasCareArg ){
+        if (hasCareArg)
+        {
           Trace("sets-cg-debug") << "......adding." << std::endl;
-          index[tn].addTerm( f1, reps );
+          index[tn].addTerm(f1, reps);
           arity = reps.size();
-        }else{
+        }
+        else
+        {
           Trace("sets-cg-debug") << "......skip." << std::endl;
         }
       }
-      if( arity>0 ){
-        //for each index
+      if (arity > 0)
+      {
+        // for each index
         for (std::pair<const TypeNode, TNodeTrie>& tt : index)
         {
           Trace("sets-cg") << "Process index " << tt.first << "..."
@@ -1016,23 +1167,33 @@ void TheorySetsPrivate::computeCareGraph() {
   }
 }
 
-bool TheorySetsPrivate::isCareArg( Node n, unsigned a ) {
-  if( d_equalityEngine.isTriggerTerm( n[a], THEORY_SETS ) ){
+bool TheorySetsPrivate::isCareArg(Node n, unsigned a)
+{
+  if (d_equalityEngine.isTriggerTerm(n[a], THEORY_SETS))
+  {
     return true;
-  }else if( ( n.getKind()==kind::MEMBER || n.getKind()==kind::SINGLETON ) && a==0 && n[0].getType().isSet() ){
+  }
+  else if ((n.getKind() == kind::MEMBER || n.getKind() == kind::SINGLETON)
+           && a == 0 && n[0].getType().isSet())
+  {
     return true;
-  }else{
+  }
+  else
+  {
     return false;
   }
 }
 
-EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
+EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b)
+{
   Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
-  if (d_equalityEngine.areEqual(a, b)) {
+  if (d_equalityEngine.areEqual(a, b))
+  {
     // The terms are implied to be equal
     return EQUALITY_TRUE;
   }
-  if (d_equalityEngine.areDisequal(a, b, false)) {
+  if (d_equalityEngine.areDisequal(a, b, false))
+  {
     // The terms are implied to be dis-equal
     return EQUALITY_FALSE;
   }
@@ -1058,13 +1219,43 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
 /******************** Model generation ********************/
 /******************** Model generation ********************/
 
+namespace {
+/**
+ * This function is a helper function to print sets as
+ * Set A = { a0, a1, a2, }
+ * instead of
+ * (union (singleton a0) (union (singleton a1) (singleton a2)))
+ */
+void traceSetElementsRecursively(stringstream& stream, const Node& set)
+{
+  Assert(set.getType().isSet());
+  if (set.getKind() == SINGLETON)
+  {
+    stream << set[0] << ", ";
+  }
+  if (set.getKind() == UNION)
+  {
+    traceSetElementsRecursively(stream, set[0]);
+    traceSetElementsRecursively(stream, set[1]);
+  }
+}
+
+std::string traceElements(const Node& set)
+{
+  std::stringstream stream;
+  traceSetElementsRecursively(stream, set);
+  return stream.str();
+}
+
+}  // namespace
+
 bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
 {
   Trace("sets-model") << "Set collect model info" << std::endl;
   set<Node> termSet;
   // Compute terms appearing in assertions and shared terms
   d_external.computeRelevantTerms(termSet);
-  
+
   // Assert equalities and disequalities to the model
   if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
   {
@@ -1072,7 +1263,7 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
   }
 
   NodeManager* nm = NodeManager::currentNM();
-  std::map< Node, Node > mvals;
+  std::map<Node, Node> mvals;
   // If cardinality is enabled, we need to use the ordered equivalence class
   // list computed by the cardinality solver, where sets equivalence classes
   // are assigned model values based on their position in the cardinality
@@ -1084,13 +1275,19 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
   for (int i = (int)(sec.size() - 1); i >= 0; i--)
   {
     Node eqc = sec[i];
-    if( termSet.find( eqc )==termSet.end() ){
-      Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl;
-    }else{
-      std::vector< Node > els;
+    if (termSet.find(eqc) == termSet.end())
+    {
+      Trace("sets-model") << "* Do not assign value for " << eqc
+                          << " since is not relevant." << std::endl;
+    }
+    else
+    {
+      std::vector<Node> els;
       bool is_base = !d_card_enabled || d_cardSolver->isModelValueBasic(eqc);
-      if( is_base ){
-        Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl;
+      if (is_base)
+      {
+        Trace("sets-model")
+            << "Collect elements of base eqc " << eqc << std::endl;
         // members that must be in eqc
         const std::map<Node, Node>& emems = d_state.getMembers(eqc);
         if (!emems.empty())
@@ -1098,24 +1295,44 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
           for (const std::pair<const Node, Node>& itmm : emems)
           {
             Node t = nm->mkNode(kind::SINGLETON, itmm.first);
-            els.push_back( t );
+            els.push_back(t);
           }
         }
       }
-      if( d_card_enabled ){
+      if (d_card_enabled)
+      {
         // make the slack elements for the equivalence class based on set
         // cardinality
-        d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals);
+        d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals, m);
       }
-      Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() );
-      rep = Rewriter::rewrite( rep );
-      Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl;
+      Node rep = NormalForm::mkBop(kind::UNION, els, eqc.getType());
+      rep = Rewriter::rewrite(rep);
+      Trace("sets-model") << "* Assign representative of " << eqc << " to "
+                          << rep << std::endl;
       mvals[eqc] = rep;
       if (!m->assertEquality(eqc, rep, true))
       {
         return false;
       }
       m->assertSkeleton(rep);
+
+      Trace("sets-model") << "Set " << eqc << " = { " << traceElements(rep)
+                          << " }" << std::endl;
+    }
+  }
+
+  // handle slack elements constraints for finite types
+  if (d_card_enabled)
+  {
+    const std::map<TypeNode, std::vector<TNode> >& slackElements =
+        d_cardSolver->getFiniteTypeSlackElements();
+    for (const std::pair<TypeNode, std::vector<TNode> >& pair : slackElements)
+    {
+      const std::vector<Node>& members =
+          d_cardSolver->getFiniteTypeMembers(pair.first);
+      m->setAssignmentExclusionSetGroup(pair.second, members);
+      Trace("sets-model") << "ExclusionSet: Group " << pair.second
+                          << " is excluded from set" << members << std::endl;
     }
   }
   return true;
@@ -1125,26 +1342,32 @@ bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
 /********************** Helper functions ***************************/
 /********************** Helper functions ***************************/
 
-Node mkAnd(const std::vector<TNode>& conjunctions) {
+Node mkAnd(const std::vector<TNode>& conjunctions)
+{
   Assert(conjunctions.size() > 0);
 
   std::set<TNode> all;
-  for (unsigned i = 0; i < conjunctions.size(); ++i) {
+  for (unsigned i = 0; i < conjunctions.size(); ++i)
+  {
     TNode t = conjunctions[i];
-    if (t.getKind() == kind::AND) {
-      for(TNode::iterator child_it = t.begin();
-          child_it != t.end(); ++child_it) {
+    if (t.getKind() == kind::AND)
+    {
+      for (TNode::iterator child_it = t.begin(); child_it != t.end();
+           ++child_it)
+      {
         Assert((*child_it).getKind() != kind::AND);
         all.insert(*child_it);
       }
     }
-    else {
+    else
+    {
       all.insert(t);
     }
   }
 
   Assert(all.size() > 0);
-  if (all.size() == 1) {
+  if (all.size() == 1)
+  {
     // All the same, or just one
     return conjunctions[0];
   }
@@ -1152,35 +1375,37 @@ Node mkAnd(const std::vector<TNode>& conjunctions) {
   NodeBuilder<> conjunction(kind::AND);
   std::set<TNode>::const_iterator it = all.begin();
   std::set<TNode>::const_iterator it_end = all.end();
-  while (it != it_end) {
+  while (it != it_end)
+  {
     conjunction << *it;
-    ++ it;
+    ++it;
   }
   return conjunction;
-}/* mkAnd() */
+} /* mkAnd() */
 
-void TheorySetsPrivate::propagate(Theory::Effort effort) {
+void TheorySetsPrivate::propagate(Theory::Effort effort) {}
 
-}
-
-bool TheorySetsPrivate::propagate(TNode literal) {
-  Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
+bool TheorySetsPrivate::propagate(TNode literal)
+{
+  Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
 
   // If already in conflict, no more propagation
   if (d_state.isInConflict())
   {
-    Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+    Debug("sets-prop") << "TheoryUF::propagate(" << literal
+                       << "): already in conflict" << std::endl;
     return false;
   }
 
   // Propagate out
   bool ok = d_external.d_out->propagate(literal);
-  if (!ok) {
+  if (!ok)
+  {
     d_state.setConflict();
   }
 
   return ok;
-}/* TheorySetsPrivate::propagate(TNode) */
+} /* TheorySetsPrivate::propagate(TNode) */
 
 OutputChannel* TheorySetsPrivate::getOutputChannel()
 {
@@ -1189,11 +1414,11 @@ OutputChannel* TheorySetsPrivate::getOutputChannel()
 
 Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
 
-void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq)
+{
   d_equalityEngine.setMasterEqualityEngine(eq);
 }
 
-
 void TheorySetsPrivate::conflict(TNode a, TNode b)
 {
   Node conf = explain(a.eqNode(b));
@@ -1205,18 +1430,22 @@ void TheorySetsPrivate::conflict(TNode a, TNode b)
 
 Node TheorySetsPrivate::explain(TNode literal)
 {
-  Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
-                << std::endl;
+  Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl;
 
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
   std::vector<TNode> assumptions;
 
-  if(atom.getKind() == kind::EQUAL) {
+  if (atom.getKind() == kind::EQUAL)
+  {
     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
-  } else if(atom.getKind() == kind::MEMBER) {
+  }
+  else if (atom.getKind() == kind::MEMBER)
+  {
     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
-  } else {
+  }
+  else
+  {
     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
                   << polarity << "); kind" << atom.getKind() << std::endl;
     Unhandled();
@@ -1229,34 +1458,30 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
 {
   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
                 << std::endl;
-  switch(node.getKind()) {
-  case kind::EQUAL:
-    d_equalityEngine.addTriggerEquality(node);
-    break;
-  case kind::MEMBER:
-    d_equalityEngine.addTriggerPredicate(node);
-    break;
-  case kind::CARD:
-    d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
-    break;
-  default:
-    d_equalityEngine.addTerm(node);
-    break;
+  switch (node.getKind())
+  {
+    case kind::EQUAL: d_equalityEngine.addTriggerEquality(node); break;
+    case kind::MEMBER: d_equalityEngine.addTriggerPredicate(node); break;
+    case kind::CARD: d_equalityEngine.addTriggerTerm(node, THEORY_SETS); break;
+    default: d_equalityEngine.addTerm(node); break;
   }
 }
 
-Node TheorySetsPrivate::expandDefinition(LogicRequest &logicRequest, Node n) {
+Node TheorySetsPrivate::expandDefinition(LogicRequest& logicRequest, Node n)
+{
   Debug("sets-proc") << "expandDefinition : " << n << std::endl;
   return n;
 }
 
-Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+Theory::PPAssertStatus TheorySetsPrivate::ppAssert(
+    TNode in, SubstitutionMap& outSubstitutions)
+{
   Debug("sets-proc") << "ppAssert : " << in << std::endl;
   Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
-  
-  //TODO: allow variable elimination for sets when setsExt = true
-  
-  //this is based off of Theory::ppAssert
+
+  // TODO: allow variable elimination for sets when setsExt = true
+
+  // this is based off of Theory::ppAssert
   if (in.getKind() == kind::EQUAL)
   {
     if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
@@ -1294,68 +1519,88 @@ void TheorySetsPrivate::presolve() { d_state.reset(); }
 /**************************** eq::NotifyClass *****************************/
 /**************************** eq::NotifyClass *****************************/
 
-
-bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality,
+                                                             bool value)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
-                   << " value = " << value << std::endl;
-  if (value) {
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = "
+                   << equality << " value = " << value << std::endl;
+  if (value)
+  {
     return d_theory.propagate(equality);
-  } else {
+  }
+  else
+  {
     // We use only literal triggers so taking not is safe
     return d_theory.propagate(equality.notNode());
   }
 }
 
-bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate,
+                                                              bool value)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
-                   << " value = " << value << std::endl;
-  if (value) {
+  Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = "
+                   << predicate << " value = " << value << std::endl;
+  if (value)
+  {
     return d_theory.propagate(predicate);
-  } else {
+  }
+  else
+  {
     return d_theory.propagate(predicate.notNode());
   }
 }
 
-bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag,
+                                                                 TNode t1,
+                                                                 TNode t2,
+                                                                 bool value)
 {
   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
-                   << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
-  d_theory.propagate( value ? t1.eqNode( t2 ) : t1.eqNode( t2 ).negate() );
+                   << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value
+                   << std::endl;
+  d_theory.propagate(value ? t1.eqNode(t2) : t1.eqNode(t2).negate());
   return true;
 }
 
-void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
+void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1,
+                                                               TNode t2)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+  Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge "
+                   << " t1 = " << t1 << " t2 = " << t2 << std::endl;
   d_theory.conflict(t1, t2);
 }
 
 void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
+  Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:"
+                   << " t = " << t << std::endl;
   d_theory.eqNotifyNewClass(t);
 }
 
 void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+  Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:"
+                   << " t1 = " << t1 << " t2 = " << t2 << std::endl;
   d_theory.eqNotifyPreMerge(t1, t2);
 }
 
 void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+  Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:"
+                   << " t1 = " << t1 << " t2 = " << t2 << std::endl;
   d_theory.eqNotifyPostMerge(t1, t2);
 }
 
-void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1,
+                                                      TNode t2,
+                                                      TNode reason)
 {
-  Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
+  Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:"
+                   << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason
+                   << std::endl;
   d_theory.eqNotifyDisequal(t1, t2, reason);
 }
 
-}/* CVC4::theory::sets namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace sets
+}  // namespace theory
+}  // namespace CVC4
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a53201e3e..22848ff97 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1583,6 +1583,22 @@ set(regress_1_tests
   regress1/sets/comp-pos-member.smt2
   regress1/sets/copy_check_heap_access_33_4.smt2
   regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
+  regress1/sets/finite-type/sets-card-arrcolor.smt2
+  regress1/sets/finite-type/sets-card-arrunit.smt2
+  regress1/sets/finite-type/sets-card-bool-1.smt2
+  regress1/sets/finite-type/sets-card-bool-2.smt2
+  regress1/sets/finite-type/sets-card-bool-3.smt2
+  regress1/sets/finite-type/sets-card-bool-4.smt2
+  regress1/sets/finite-type/sets-card-bool-rec.smt2
+  regress1/sets/finite-type/sets-card-bv-1.smt2
+  regress1/sets/finite-type/sets-card-bv-2.smt2
+  regress1/sets/finite-type/sets-card-bv-3.smt2
+  regress1/sets/finite-type/sets-card-bv-4.smt2
+  regress1/sets/finite-type/sets-card-color.smt2
+  regress1/sets/finite-type/sets-card-color-sat.smt2
+  regress1/sets/finite-type/sets-card-datatype-1.smt2
+  regress1/sets/finite-type/sets-card-datatype-2.smt2
+  regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2
   regress1/sets/fuzz14418.smt2
   regress1/sets/fuzz15201.smt2
   regress1/sets/fuzz31811.smt2
@@ -2277,6 +2293,7 @@ set(regression_disabled_tests
   regress1/rewriterules/test_guards.smt2
   regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2
   regress1/sets/setofsets-disequal.smt2
+  regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
   regress1/simple-rdl-definefun.smt2
   # does not solve after minor modification to search
   regress1/sygus/car_3.lus.sy
diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2
new file mode 100644
index 000000000..2c7acf282
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_ALL)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Color ((Red) (Green) (Blue)))
+(declare-fun A () (Set (Array Color Color)))
+(declare-fun B () (Set (Array Color Color)))
+(assert (> (card A) 25))
+(assert (> (card B) 25))
+(assert (distinct A B))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2 b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2
new file mode 100644
index 000000000..95d363397
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_ALL)
+(set-info :status unsat)
+(set-option :sets-ext true)
+(declare-datatype Unit ((mkUnit)))
+
+(declare-fun S () (Set (Array Int Unit)))
+
+(assert (> (card S) 1))
+
+(check-sat)
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
new file mode 100644
index 000000000..c455caa28
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set Bool))
+(declare-fun B () (Set Bool))
+(declare-fun universe () (Set Bool))
+(assert (= (card A) 2))
+(assert (= (card B) 2))
+(assert (= (intersection A B) (as emptyset (Set Bool))))
+(assert (= universe (as univset (Set Bool))))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2
new file mode 100644
index 000000000..977bf3795
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set Bool))
+(declare-fun universe () (Set Bool))
+(assert (= (card A) 2))
+(assert (= universe (as univset (Set Bool))))
+(check-sat)
+
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2
new file mode 100644
index 000000000..623376e37
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set Bool))
+(declare-fun B () (Set Bool))
+(declare-fun universe () (Set Bool))
+(assert (= (card A) 2))
+(assert (= (card B) 2))
+(assert (= universe (as univset (Set Bool))))
+(check-sat)
+
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2
new file mode 100644
index 000000000..1e18597dc
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_ALL)
+(set-info :status sat)
+(set-option :sets-ext true)
+(set-option :produce-models true)
+(declare-fun A () (Set Bool))
+(declare-fun x () Bool)
+(assert (member (member x A) A))
+(assert (> (card A) 1))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2
new file mode 100644
index 000000000..150dd5cff
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_ALL)
+(set-info :status sat)
+(set-option :sets-ext true)
+(declare-fun A () (Set Bool))
+(declare-fun x () Bool)
+(assert (member (member x A) A))
+(assert (> (card A) 1))
+(declare-fun U () (Set Bool))
+(assert (= U (as univset (Set Bool))))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2
new file mode 100644
index 000000000..1388b9bfa
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun universe () (Set (_ BitVec 3)))
+(assert (= (card A) 3))
+(assert (= universe (as univset (Set (_ BitVec 3)))))
+(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
new file mode 100644
index 000000000..26ee05f3c
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2
@@ -0,0 +1,16 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun B () (Set (_ BitVec 3)))
+(declare-fun universe () (Set (_ BitVec 3)))
+(assert (= (card A) 5))
+(assert (= (card B) 5))
+(assert (not (= A B)))
+(assert (= (card (intersection A B)) 2))
+(assert (= (card (setminus A B)) 3))
+(assert (= (card (setminus B A)) 3))
+(assert (= universe (as univset (Set (_ BitVec 3)))))
+(check-sat)
+
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
new file mode 100644
index 000000000..8c92d1c6b
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2
@@ -0,0 +1,19 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun B () (Set (_ BitVec 3)))
+(declare-fun universe () (Set (_ BitVec 3)))
+(declare-fun x () (_ BitVec 3))
+(assert (= (card A) 3))
+(assert (= (card B) 3))
+(assert (not (= A B)))
+(assert (= (card (intersection A B)) 1))
+(assert (= (card (setminus A B)) 2))
+(assert (= (card (setminus B A)) 2))
+(assert (not (member x A)))
+(assert (not (member x B)))
+(assert (= universe (as univset (Set (_ BitVec 3)))))
+(check-sat)
+
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
new file mode 100644
index 000000000..d2c8a744d
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2
@@ -0,0 +1,18 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun B () (Set (_ BitVec 3)))
+(declare-fun universe () (Set (_ BitVec 3)))
+(declare-fun x () (_ BitVec 3))
+(assert (= (card A) 5))
+(assert (= (card B) 5))
+(assert (not (= A B)))
+(assert (= (card (intersection A B)) 2))
+(assert (= (card (setminus A B)) 3))
+(assert (= (card (setminus B A)) 3))
+(assert (= universe (as univset (Set (_ BitVec 3)))))
+(assert (not (member x A)))
+(assert (not (member x B)))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2
new file mode 100644
index 000000000..ca8015622
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_BVDTLIAFS)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Color ((Red) (Green) (Blue) (Purple)))
+(declare-fun A () (Set Color))
+(declare-fun B () (Set Color))
+(assert (> (card A) (card B) ))
+(assert (member Red B))
+(declare-fun d () Color)
+(assert (not (= d Red)))
+(assert (member d B))
+(assert (not (member Green A)))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-color.smt2 b/test/regress/regress1/sets/finite-type/sets-card-color.smt2
new file mode 100644
index 000000000..4fe3f0428
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-color.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_BVDTLIAFS)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Color ((Red) (Green) (Blue)))
+(declare-fun A () (Set Color))
+(declare-fun B () (Set Color))
+(assert (> (card A) (card B) ))
+(assert (member Red B))
+(declare-fun d () Color)
+(assert (not (= d Red)))
+(assert (member d B))
+(assert (not (member Green A)))
+(check-sat)
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
new file mode 100644
index 000000000..0121479e9
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Rec ((mkRec (r1 (_ BitVec 2)) (r2 (_ BitVec 2)))))
+(declare-fun A () (Set Rec))
+(declare-fun B () (Set Rec))
+(declare-fun universe () (Set Rec))
+(declare-fun x () Rec)
+(assert (= (card A) 5))
+(assert (= (card B) 5))
+(assert (= (card (intersection A B)) 1))
+(assert (= universe (as univset (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
new file mode 100644
index 000000000..708ebb2ca
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-datatype Rec ((mkRec (r1 (_ BitVec 2)) (r2 (_ BitVec 2)))))
+(declare-fun A () (Set Rec))
+(declare-fun B () (Set Rec))
+(declare-fun universe () (Set Rec))
+(assert (= (card A) 9))
+(assert (= (card B) 9))
+(assert (= (card (intersection A B)) 1))
+(assert (= universe (as univset (Set Rec))))
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2
new file mode 100644
index 000000000..b4bd97f1d
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2
@@ -0,0 +1,30 @@
+(set-logic QF_ALL)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 2)))
+(declare-fun B () (Set (_ BitVec 2)))
+(declare-fun C () (Set (_ BitVec 2)))
+(declare-fun D () (Set (_ BitVec 2)))
+
+(declare-fun x () (_ BitVec 2))
+(assert (not (member x A)))
+(assert (not (member x B)))
+(assert (not (member x C)))
+(assert (not (member x D)))
+(declare-fun y () (_ BitVec 2))
+(assert (not (member y A)))
+(assert (not (member y B)))
+(assert (not (member y C)))
+(assert (not (member y D)))
+(declare-fun z () (_ BitVec 2))
+(assert (not (member z A)))
+(assert (not (member z B)))
+(assert (not (member z C)))
+(assert (not (member z D)))
+
+(assert (distinct x y z))
+
+(assert (= (card (union A (union B (union C D)))) 2))
+
+(check-sat)
diff --git a/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2 b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
new file mode 100644
index 000000000..88825a600
--- /dev/null
+++ b/test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
@@ -0,0 +1,30 @@
+(set-logic QF_ALL)
+(set-info :status unsat)
+(set-option :produce-models true)
+(set-option :sets-ext true)
+(declare-fun A () (Set (_ BitVec 3)))
+(declare-fun B () (Set (_ BitVec 3)))
+(declare-fun C () (Set (_ BitVec 3)))
+(declare-fun D () (Set (_ BitVec 3)))
+
+(declare-fun x () (_ BitVec 3))
+(assert (not (member x A)))
+(assert (not (member x B)))
+(assert (not (member x C)))
+(assert (not (member x D)))
+(declare-fun y () (_ BitVec 3))
+(assert (not (member y A)))
+(assert (not (member y B)))
+(assert (not (member y C)))
+(assert (not (member y D)))
+(declare-fun z () (_ BitVec 3))
+(assert (not (member z A)))
+(assert (not (member z B)))
+(assert (not (member z C)))
+(assert (not (member z D)))
+
+(assert (distinct x y z))
+
+(assert (= (card (union A (union B (union C D)))) 6))
+
+(check-sat)