Fix computation of whether a type is finite (#6312)

This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.

Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).

31 files changed, 268 insertions, 297 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 47b376151..b29647311 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -3462,7 +3462,9 @@ bool Datatype::isFinite() const
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
   //////// all checks before this line
-  return d_dtype->isFinite();
+  // we assume that finite model finding is disabled by passing false as the
+  // second argument
+  return isCardinalityClassFinite(d_dtype->getCardinalityClass(), false);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 73f760170..66331f5c7 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -488,64 +488,44 @@ bool DType::computeCardinalityRecSingleton(
   return true;
 }
 
-bool DType::isFinite(TypeNode t) const
+CardinalityClass DType::getCardinalityClass(TypeNode t) const
 {
   Trace("datatypes-init") << "DType::isFinite " << std::endl;
   Assert(isResolved());
   Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self);
 
   // is this already in the cache ?
-  if (d_self.getAttribute(DTypeFiniteComputedAttr()))
+  std::map<TypeNode, CardinalityClass>::const_iterator it = d_cardClass.find(t);
+  if (it != d_cardClass.end())
   {
-    return d_self.getAttribute(DTypeFiniteAttr());
+    return it->second;
   }
+  // it is the max cardinality class of a constructor, with base case ONE
+  // if we have one constructor and FINITE otherwise.
+  CardinalityClass c = d_constructors.size() == 1 ? CardinalityClass::ONE
+                                                  : CardinalityClass::FINITE;
   for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
   {
-    if (!ctor->isFinite(t))
-    {
-      d_self.setAttribute(DTypeFiniteComputedAttr(), true);
-      d_self.setAttribute(DTypeFiniteAttr(), false);
-      return false;
-    }
+    CardinalityClass cc = ctor->getCardinalityClass(t);
+    c = maxCardinalityClass(c, cc);
   }
-  d_self.setAttribute(DTypeFiniteComputedAttr(), true);
-  d_self.setAttribute(DTypeFiniteAttr(), true);
-  return true;
+  d_cardClass[t] = c;
+  return c;
 }
-bool DType::isFinite() const
+CardinalityClass DType::getCardinalityClass() const
 {
   Assert(isResolved() && !isParametric());
-  return isFinite(d_self);
+  return getCardinalityClass(d_self);
 }
 
-bool DType::isInterpretedFinite(TypeNode t) const
+bool DType::isFinite(TypeNode t, bool fmfEnabled) const
 {
-  Trace("datatypes-init") << "DType::isInterpretedFinite " << std::endl;
-  Assert(isResolved());
-  Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self);
-  // is this already in the cache ?
-  if (d_self.getAttribute(DTypeUFiniteComputedAttr()))
-  {
-    return d_self.getAttribute(DTypeUFiniteAttr());
-  }
-  // start by assuming it is not
-  d_self.setAttribute(DTypeUFiniteComputedAttr(), true);
-  d_self.setAttribute(DTypeUFiniteAttr(), false);
-  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
-  {
-    if (!ctor->isInterpretedFinite(t))
-    {
-      return false;
-    }
-  }
-  d_self.setAttribute(DTypeUFiniteComputedAttr(), true);
-  d_self.setAttribute(DTypeUFiniteAttr(), true);
-  return true;
+  return isCardinalityClassFinite(getCardinalityClass(t), fmfEnabled);
 }
-bool DType::isInterpretedFinite() const
+
+bool DType::isFinite(bool fmfEnabled) const
 {
-  Assert(isResolved() && !isParametric());
-  return isInterpretedFinite(d_self);
+  return isFinite(d_self, fmfEnabled);
 }
 
 bool DType::isWellFounded() const
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index cee95cdc6..2837e37af 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -47,32 +47,6 @@ struct DTypeConsIndexTag
 {
 };
 typedef expr::Attribute<DTypeConsIndexTag, size_t> DTypeConsIndexAttr;
-/** Attribute true for datatype types that are finite. */
-struct DTypeFiniteTag
-{
-};
-typedef expr::Attribute<DTypeFiniteTag, bool> DTypeFiniteAttr;
-/** Attribute true when we have computed whether a datatype type is finite */
-struct DTypeFiniteComputedTag
-{
-};
-typedef expr::Attribute<DTypeFiniteComputedTag, bool> DTypeFiniteComputedAttr;
-/**
- * Attribute true for datatype types that are interpreted as finite (see
- * TypeNode::isInterpretedFinite).
- */
-struct DTypeUFiniteTag
-{
-};
-typedef expr::Attribute<DTypeUFiniteTag, bool> DTypeUFiniteAttr;
-/**
- * Attribute true when we have computed whether a datatype type is interpreted
- * as finite.
- */
-struct DTypeUFiniteComputedTag
-{
-};
-typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
 // ----------------------- end datatype attributes
 
 class DTypeConstructor;
@@ -282,30 +256,31 @@ class DType
   Cardinality getCardinality() const;
 
   /**
-   * Return true iff this DType has finite cardinality. If the
-   * datatype is not well-founded, this method returns false. The
+   * Return the cardinality class of the datatype. The
    * DType must be resolved or an assertion is violated.
    *
    * The version of this method that takes type t is required
    * for parametric datatypes, where t is an instantiated
    * parametric datatype type whose datatype is this class.
    */
-  bool isFinite(TypeNode t) const;
-  bool isFinite() const;
+  CardinalityClass getCardinalityClass(TypeNode t) const;
+  CardinalityClass getCardinalityClass() const;
 
   /**
-   * Return true iff this  DType is finite (all constructors are
-   * finite, i.e., there  are finitely  many ground terms) under the
-   * assumption that unintepreted sorts are finite. If the
-   * datatype is  not well-founded, this method returns false.  The
+   * Return true iff this DType has finite cardinality. If the
+   * datatype is not well-founded, this method returns false. The
    * DType must be resolved or an assertion is violated.
    *
-   * The versions of these methods that takes type t is required
+   * The version of this method that takes type t is required
    * for parametric datatypes, where t is an instantiated
    * parametric datatype type whose datatype is this class.
+   *
+   * @param t The (instantiated) datatype type we are computing finiteness for
+   * @param fmfEnabled Whether finite model finding is enabled
+   * @return true if finite model finding is enabled
    */
-  bool isInterpretedFinite(TypeNode t) const;
-  bool isInterpretedFinite() const;
+  bool isFinite(TypeNode t, bool fmfEnabled=false) const;
+  bool isFinite(bool fmfEnabled=false) const;
 
   /** is well-founded
    *
@@ -640,6 +615,8 @@ class DType
   /** cache of shared selectors for this datatype */
   mutable std::map<TypeNode, std::map<TypeNode, std::map<unsigned, Node> > >
       d_sharedSel;
+  /**  A cache for getCardinalityClass. */
+  mutable std::map<TypeNode, CardinalityClass> d_cardClass;
 }; /* class DType */
 
 /**
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index debb66ef4..8d6194b06 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -158,34 +158,28 @@ Cardinality DTypeConstructor::getCardinality(TypeNode t) const
   return c;
 }
 
-bool DTypeConstructor::isFinite(TypeNode t) const
+CardinalityClass DTypeConstructor::getCardinalityClass(TypeNode t) const
 {
-  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
-  return cinfo.first == CardinalityType::FINITE;
-}
-
-bool DTypeConstructor::isInterpretedFinite(TypeNode t) const
-{
-  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
-  return cinfo.first != CardinalityType::INFINITE;
+  std::pair<CardinalityClass, bool> cinfo = computeCardinalityInfo(t);
+  return cinfo.first;
 }
 
 bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const
 {
-  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
+  std::pair<CardinalityClass, bool> cinfo = computeCardinalityInfo(t);
   return cinfo.second;
 }
 
-std::pair<DTypeConstructor::CardinalityType, bool>
-DTypeConstructor::computeCardinalityInfo(TypeNode t) const
+std::pair<CardinalityClass, bool> DTypeConstructor::computeCardinalityInfo(
+    TypeNode t) const
 {
-  std::map<TypeNode, std::pair<CardinalityType, bool> >::iterator it =
+  std::map<TypeNode, std::pair<CardinalityClass, bool> >::iterator it =
       d_cardInfo.find(t);
   if (it != d_cardInfo.end())
   {
     return it->second;
   }
-  std::pair<CardinalityType, bool> ret(CardinalityType::FINITE, false);
+  std::pair<CardinalityClass, bool> ret(CardinalityClass::ONE, false);
   std::vector<TypeNode> instTypes;
   std::vector<TypeNode> paramTypes;
   bool isParam = t.isParametricDatatype();
@@ -204,27 +198,16 @@ DTypeConstructor::computeCardinalityInfo(TypeNode t) const
                          instTypes.begin(),
                          instTypes.end());
     }
-    if (tc.isFinite())
-    {
-      // do nothing
-    }
-    else if (tc.isInterpretedFinite())
-    {
-      if (ret.first == CardinalityType::FINITE)
-      {
-        // not simply finite, it depends on uninterpreted sorts being finite
-        ret.first = CardinalityType::INTERPRETED_FINITE;
-      }
-    }
-    else
+    // get the current cardinality class
+    CardinalityClass cctc = tc.getCardinalityClass();
+    // update ret.first to the max cardinality class
+    ret.first = maxCardinalityClass(ret.first, cctc);
+    if (cctc != CardinalityClass::INFINITE)
     {
-      // infinite implies the constructor is infinite cardinality
-      ret.first = CardinalityType::INFINITE;
-      continue;
+      // if the argument is (interpreted) finite and external, set the flag
+      // for indicating it has a finite external argument
+      ret.second = ret.second || !tc.isDatatype();
     }
-    // if the argument is (interpreted) finite and external, set the flag
-    // for indicating it has a finite external argument
-    ret.second = ret.second || !tc.isDatatype();
   }
   d_cardInfo[t] = ret;
   return ret;
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index 368d4cbde..55d940d91 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -24,6 +24,7 @@
 #include "expr/dtype_selector.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "util/cardinality_class.h"
 
 namespace cvc5 {
 
@@ -147,18 +148,15 @@ class DTypeConstructor
   Cardinality getCardinality(TypeNode t) const;
 
   /**
-   * Return true iff this constructor is finite (it is nullary or
-   * each of its argument types are finite).  This function can
-   * only be called for resolved constructors.
-   */
-  bool isFinite(TypeNode t) const;
-  /**
-   * Return true iff this constructor is finite (it is nullary or
-   * each of its argument types are finite) under assumption
-   * uninterpreted sorts are finite.  This function can
-   * only be called for resolved constructors.
+   * Return the cardinality class, which indicates if the type has cardinality
+   * one, is finite or infinite, possibly dependent on uninterpreted sorts being
+   * finite.
+   *
+   * Note that the cardinality of a constructor is equivalent to asking how
+   * many applications of this constructor exist.
    */
-  bool isInterpretedFinite(TypeNode t) const;
+  CardinalityClass getCardinalityClass(TypeNode t) const;
+
   /**
    * Has finite external argument type. This returns true if this constructor
    * has an argument type that is not a datatype and is interpreted as a
@@ -237,17 +235,6 @@ class DTypeConstructor
   void toStream(std::ostream& out) const;
 
  private:
-  /** Constructor cardinality type */
-  enum class CardinalityType
-  {
-    // the constructor is finite
-    FINITE,
-    // the constructor is interpreted-finite (finite under the assumption that
-    // uninterpreted sorts are finite)
-    INTERPRETED_FINITE,
-    // the constructor is infinte
-    INFINITE
-  };
   /** resolve
    *
    * This resolves (initializes) the constructor. For details
@@ -311,7 +298,7 @@ class DTypeConstructor
    * type t, and a Boolean indicating whether the constructor has any arguments
    * that have finite external type.
    */
-  std::pair<CardinalityType, bool> computeCardinalityInfo(TypeNode t) const;
+  std::pair<CardinalityClass, bool> computeCardinalityInfo(TypeNode t) const;
   /** compute shared selectors
    * This computes the maps d_sharedSelectors and d_sharedSelectorIndex.
    */
@@ -351,7 +338,7 @@ class DTypeConstructor
    */
   mutable std::map<TypeNode, std::map<Node, unsigned> > d_sharedSelectorIndex;
   /**  A cache for computeCardinalityInfo. */
-  mutable std::map<TypeNode, std::pair<CardinalityType, bool> > d_cardInfo;
+  mutable std::map<TypeNode, std::pair<CardinalityClass, bool> > d_cardInfo;
 }; /* class DTypeConstructor */
 
 /**
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 2da1b7ad2..3c0316405 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -65,160 +65,123 @@ Cardinality TypeNode::getCardinality() const {
   return kind::getCardinality(*this);
 }
 
-/** Attribute true for types that are finite */
-struct IsFiniteTag
+/** Attribute true for types that have cardinality one */
+struct TypeCardinalityClassTag
 {
 };
-typedef expr::Attribute<IsFiniteTag, bool> IsFiniteAttr;
-/** Attribute true for types which we have computed the above attribute */
-struct IsFiniteComputedTag
-{
-};
-typedef expr::Attribute<IsFiniteComputedTag, bool> IsFiniteComputedAttr;
+typedef expr::Attribute<TypeCardinalityClassTag, uint64_t>
+    TypeCardinalityClassAttr;
 
-/** Attribute true for types that are interpreted as finite */
-struct IsInterpretedFiniteTag
-{
-};
-typedef expr::Attribute<IsInterpretedFiniteTag, bool> IsInterpretedFiniteAttr;
-/** Attribute true for types which we have computed the above attribute */
-struct IsInterpretedFiniteComputedTag
-{
-};
-typedef expr::Attribute<IsInterpretedFiniteComputedTag, bool>
-    IsInterpretedFiniteComputedAttr;
-
-bool TypeNode::isFinite() { return isFiniteInternal(false); }
-
-bool TypeNode::isInterpretedFinite()
-{
-  return isFiniteInternal(options::finiteModelFind());
-}
-
-bool TypeNode::isFiniteInternal(bool usortFinite)
+CardinalityClass TypeNode::getCardinalityClass()
 {
   // check it is already cached
-  if (usortFinite)
-  {
-    if (getAttribute(IsInterpretedFiniteComputedAttr()))
-    {
-      return getAttribute(IsInterpretedFiniteAttr());
-    }
-  }
-  else if (getAttribute(IsFiniteComputedAttr()))
+  if (hasAttribute(TypeCardinalityClassAttr()))
   {
-    return getAttribute(IsFiniteAttr());
+    return static_cast<CardinalityClass>(
+        getAttribute(TypeCardinalityClassAttr()));
   }
-  bool ret = false;
+  CardinalityClass ret = CardinalityClass::INFINITE;
   if (isSort())
   {
-    ret = usortFinite;
+    ret = CardinalityClass::INTERPRETED_ONE;
   }
   else if (isBoolean() || isBitVector() || isFloatingPoint()
            || isRoundingMode())
   {
-    ret = true;
+    ret = CardinalityClass::FINITE;
   }
-  else if (isString() || isRegExp() || isSequence() || isReal())
+  else if (isString() || isRegExp() || isSequence() || isReal() || isBag())
   {
-    ret = false;
+    ret = CardinalityClass::INFINITE;
   }
   else
   {
     // recursive case (this may be a parametric sort), we assume infinite for
-    // the moment here to prevent infinite loops
-    if (usortFinite)
-    {
-      setAttribute(IsInterpretedFiniteAttr(), false);
-      setAttribute(IsInterpretedFiniteComputedAttr(), true);
-    }
-    else
-    {
-      setAttribute(IsFiniteAttr(), false);
-      setAttribute(IsFiniteComputedAttr(), true);
-    }
+    // the moment here to prevent infinite loops, which may occur when
+    // computing the cardinality of datatype types with foreign types
+    setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret));
+
     if (isDatatype())
     {
       TypeNode tn = *this;
       const DType& dt = getDType();
-      ret = usortFinite ? dt.isInterpretedFinite(tn) : dt.isFinite(tn);
+      ret = dt.getCardinalityClass(tn);
     }
     else if (isArray())
     {
-      TypeNode tnc = getArrayConstituentType();
-      if (!tnc.isFiniteInternal(usortFinite))
+      ret = getArrayConstituentType().getCardinalityClass();
+      if (ret == CardinalityClass::FINITE
+          || ret == CardinalityClass::INTERPRETED_FINITE)
+      {
+        CardinalityClass cci = getArrayIndexType().getCardinalityClass();
+        // arrays with both finite element types, we take the max with its
+        // index type.
+        ret = maxCardinalityClass(ret, cci);
+      }
+      // else, array types whose element type is INFINITE, ONE, or
+      // INTERPRETED_ONE have the same cardinality class as their range.
+    }
+    else if (isSet())
+    {
+      CardinalityClass cc = getSetElementType().getCardinalityClass();
+      if (cc == CardinalityClass::ONE)
       {
-        // arrays with constituent type that is infinite are infinite
-        ret = false;
+        // 1 -> 2
+        ret = CardinalityClass::FINITE;
       }
-      else if (getArrayIndexType().isFiniteInternal(usortFinite))
+      else if (ret == CardinalityClass::INTERPRETED_ONE)
       {
-        // arrays with both finite constituent and index types are finite
-        ret = true;
+        // maybe 1 -> maybe finite
+        ret = CardinalityClass::INTERPRETED_FINITE;
       }
       else
       {
-        // If the consistuent type of the array has cardinality one, then the
-        // array type has cardinality one, independent of the index type.
-        ret = tnc.getCardinality().isOne();
+        // finite or infinite is unchanged
+        ret = cc;
       }
     }
-    else if (isSet())
-    {
-      ret = getSetElementType().isFiniteInternal(usortFinite);
-    }
-    else if (isBag())
-    {
-      // there are infinite bags for all element types
-      ret = false;
-    }
     else if (isFunction())
     {
-      ret = true;
-      TypeNode tnr = getRangeType();
-      if (!tnr.isFiniteInternal(usortFinite))
-      {
-        ret = false;
-      }
-      else
+      ret = getRangeType().getCardinalityClass();
+      if (ret == CardinalityClass::FINITE
+          || ret == CardinalityClass::INTERPRETED_FINITE)
       {
+        // we may have a larger cardinality class based on the
+        // arguments of the function
         std::vector<TypeNode> argTypes = getArgTypes();
-        for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+        for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++)
         {
-          if (!argTypes[i].isFiniteInternal(usortFinite))
-          {
-            ret = false;
-            break;
-          }
-        }
-        if (!ret)
-        {
-          // similar to arrays, functions are finite if their range type
-          // has cardinality one, regardless of the arguments.
-          ret = tnr.getCardinality().isOne();
+          CardinalityClass cca = argTypes[i].getCardinalityClass();
+          ret = maxCardinalityClass(ret, cca);
         }
       }
+      // else, function types whose range type is INFINITE, ONE, or
+      // INTERPRETED_ONE have the same cardinality class as their range.
+    }
+    else if (isConstructor())
+    {
+      // notice that we require computing the cardinality class of the
+      // constructor type, which is equivalent to asking how many
+      // constructor applications of the given constructor exist. This
+      // is used in several places in the decision procedure for datatypes.
+      // The cardinality starts with one.
+      ret = CardinalityClass::ONE;
+      // we may have a larger cardinality class based on the
+      // arguments of the constructor
+      std::vector<TypeNode> argTypes = getArgTypes();
+      for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++)
+      {
+        CardinalityClass cca = argTypes[i].getCardinalityClass();
+        ret = maxCardinalityClass(ret, cca);
+      }
     }
     else
     {
-      // all types should be handled above
+      // all types we care about should be handled above
       Assert(false);
-      // by default, compute the exact cardinality for the type and check
-      // whether it is finite. This should be avoided in general, since
-      // computing cardinalities for types can be highly expensive.
-      ret = getCardinality().isFinite();
     }
   }
-  if (usortFinite)
-  {
-    setAttribute(IsInterpretedFiniteAttr(), ret);
-    setAttribute(IsInterpretedFiniteComputedAttr(), true);
-  }
-  else
-  {
-    setAttribute(IsFiniteAttr(), ret);
-    setAttribute(IsFiniteComputedAttr(), true);
-  }
+  setAttribute(TypeCardinalityClassAttr(), static_cast<uint64_t>(ret));
   return ret;
 }
 
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 9b2f4b4d0..dab7fd394 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -30,6 +30,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "util/cardinality.h"
+#include "util/cardinality_class.h"
 
 namespace cvc5 {
 
@@ -407,19 +408,14 @@ public:
    * @return a finite or infinite cardinality
    */
   Cardinality getCardinality() const;
-
-  /**
-   * Is this type finite? This assumes uninterpreted sorts have infinite
-   * cardinality.
-   */
-  bool isFinite();
-
   /**
-   * Is this type interpreted as finite.
-   * If finite model finding is enabled, this assumes all uninterpreted sorts
-   *   are interpreted as finite.
+   * Get the cardinality class of this type node. The cardinality class
+   * is static for each type node and does not depend on the state of the
+   * solver. For details on cardinality classes, see util/cardinality_class.h
+   *
+   * @return the cardinality class
    */
-  bool isInterpretedFinite();
+  CardinalityClass getCardinalityClass();
 
   /** is closed enumerable type
    *
@@ -713,13 +709,6 @@ private:
   static TypeNode commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast);
 
   /**
-   * Is this type interpreted as finite.
-   * If the flag usortFinite is true, this assumes all uninterpreted sorts
-   *   are interpreted as finite.
-   */
-  bool isFiniteInternal(bool usortFinite);
-
-  /**
    * Indents the given stream a given amount of spaces.
    *
    * @param out the stream to indent
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 6e7a5c0a8..d4dbdf82d 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -786,7 +786,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
           TypeNode tnc = children[c1].getType();
           // we may only apply this symmetry breaking scheme (which introduces
           // disequalities) if the types are infinite.
-          if (tnc == children[c2].getType() && !tnc.isInterpretedFinite())
+          if (tnc == children[c2].getType() && !d_state.isFiniteType(tnc))
           {
             Node sym_lem_deq = children[c1].eqNode(children[c2]).negate();
             // notice that this symmetry breaking still allows for
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 7242407cc..60fd87731 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -218,7 +218,7 @@ void TheoryDatatypes::postCheck(Effort level)
             const DType& dt = tt.getDType();
             Trace("datatypes-debug")
                 << "Datatype " << dt.getName() << " is "
-                << dt.isInterpretedFinite(tt) << " "
+                << dt.getCardinalityClass(tt) << " "
                 << dt.isRecursiveSingleton(tt) << std::endl;
             bool continueProc = true;
             if( dt.isRecursiveSingleton( tt ) ){
@@ -273,14 +273,21 @@ void TheoryDatatypes::postCheck(Effort level)
               int consIndex = -1;
               int fconsIndex = -1;
               bool needSplit = true;
-              for( unsigned int j=0; j<pcons.size(); j++ ) {
+              for (size_t j = 0, psize = pcons.size(); j < psize; j++)
+              {
                 if( pcons[j] ) {
                   if( consIndex==-1 ){
                     consIndex = j;
                   }
                   Trace("datatypes-debug") << j << " compute finite..."
                                            << std::endl;
-                  bool ifin = dt[j].isInterpretedFinite(tt);
+                  // Notice that we split here on all datatypes except the
+                  // truly infinite ones. It is possible to also not split
+                  // on those that are interpreted-finite when finite model
+                  // finding is disabled, but as a heuristic we choose to split
+                  // on those too.
+                  bool ifin = dt[j].getCardinalityClass(tt)
+                              != CardinalityClass::INFINITE;
                   Trace("datatypes-debug") << "...returned " << ifin
                                            << std::endl;
                   if (!ifin)
@@ -1327,8 +1334,9 @@ bool TheoryDatatypes::collectModelValues(TheoryModel* m,
       for( unsigned r=0; r<2; r++ ){
         if( neqc.isNull() ){
           for( unsigned i=0; i<pcons.size(); i++ ){
-            //must try the infinite ones first
-            bool cfinite = dt[ i ].isInterpretedFinite( tt );
+            // must try the infinite ones first
+            bool cfinite =
+                d_state.isFiniteType(dt[i].getSpecializedConstructorType(tt));
             if( pcons[i] && (r==1)==cfinite ){
               neqc = utils::getInstCons(eqc, dt, i);
               break;
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index f7a6f26f3..6cb2fdce9 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -199,7 +199,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    Debug("dt-enum") << "datatype is " << d_type << std::endl;
    Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
                     << d_datatype.isRecursiveSingleton(d_type);
-   Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type)
+   Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type)
                     << std::endl;
    // Start with the ground term constructed via mkGroundValue, which does
    // a traversal over the structure of the datatype to find a finite term.
@@ -312,7 +312,8 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
        // or other cases
        if (prevSize == d_size_limit
            || (d_size_limit == 0 && d_datatype.isCodatatype())
-           || !d_datatype.isInterpretedFinite(d_type))
+           || d_datatype.getCardinalityClass(d_type)
+                  == CardinalityClass::INFINITE)
        {
          d_size_limit++;
          d_ctor = 0;
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 044183756..fbee35f3d 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -63,7 +63,8 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
 
   bool hasCyclesDt(const DType& dt)
   {
-    return dt.isRecursiveSingleton(d_type) || !dt.isFinite(d_type);
+    return dt.isRecursiveSingleton(d_type)
+           || dt.getCardinalityClass(d_type) == CardinalityClass::INFINITE;
   }
   bool hasCycles( TypeNode tn ){
     if( tn.isDatatype() ){
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index a4f4170fa..b0f6e63bf 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -357,7 +357,7 @@ void BoundedIntegers::checkOwnership(Node f)
           // supported for finite element types #1123). Regardless, this is
           // typically not a limitation since this variable can be bound in a
           // standard way below since its type is finite.
-          if (!v.getType().isInterpretedFinite())
+          if (!d_qstate.isFiniteType(v.getType()))
           {
             setBoundedVar(f, v, BOUND_SET_MEMBER);
             setBoundVar = true;
@@ -417,7 +417,7 @@ void BoundedIntegers::checkOwnership(Node f)
       for( unsigned i=0; i<f[0].getNumChildren(); i++) {
         if( d_bound_type[f].find( f[0][i] )==d_bound_type[f].end() ){
           TypeNode tn = f[0][i].getType();
-          if ((tn.isSort() && tn.isInterpretedFinite())
+          if ((tn.isSort() && d_qstate.isFiniteType(tn))
               || d_qreg.getQuantifiersBoundInference().mayComplete(tn))
           {
             success = true;
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index e935ee694..585032dc4 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -133,7 +133,7 @@ void ModelEngine::registerQuantifier( Node f ){
     for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
       TypeNode tn = f[0][i].getType();
       if( !tn.isSort() ){
-        if (!tn.isInterpretedFinite())
+        if (!d_qstate.isFiniteType(tn))
         {
           if( tn.isInteger() ){
             if( !options::fmfBound() ){
diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp
index 7b184bf0d..1fbf53761 100644
--- a/src/theory/quantifiers/quant_bound_inference.cpp
+++ b/src/theory/quantifiers/quant_bound_inference.cpp
@@ -48,8 +48,14 @@ bool QuantifiersBoundInference::mayComplete(TypeNode tn)
 
 bool QuantifiersBoundInference::mayComplete(TypeNode tn, unsigned maxCard)
 {
+  if (!tn.isClosedEnumerable())
+  {
+    return false;
+  }
   bool mc = false;
-  if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
+  // we cannot use FMF to complete interpreted types, thus we pass
+  // false for fmfEnabled here
+  if (isCardinalityClassFinite(tn.getCardinalityClass(), false))
   {
     Cardinality c = tn.getCardinality();
     if (!c.isLargeFinite())
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index be384d1aa..cc2525b78 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -52,6 +52,7 @@ void QuantDSplit::checkOwnership(Node q)
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
     if( tn.isDatatype() ){
+      bool isFinite = d_qstate.isFiniteType(tn);
       const DType& dt = tn.getDType();
       if (dt.isRecursiveSingleton(tn))
       {
@@ -62,14 +63,14 @@ void QuantDSplit::checkOwnership(Node q)
         if (options::quantDynamicSplit() == options::QuantDSplitMode::AGG)
         {
           // split if it is a finite datatype
-          doSplit = dt.isInterpretedFinite(tn);
+          doSplit = isFinite;
         }
         else if (options::quantDynamicSplit()
                  == options::QuantDSplitMode::DEFAULT)
         {
           if (!qbi.isFiniteBound(q, q[0][i]))
           {
-            if (dt.isInterpretedFinite(tn))
+            if (isFinite)
             {
               // split if goes from being unhandled -> handled by finite
               // instantiation. An example is datatypes with uninterpreted sort
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index c0fb17dab..83a4276ab 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -773,8 +773,10 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal()
   // have we run out of constructor classes for this size?
   if (d_ccCons.empty())
   {
-    // check whether we should terminate
-    if (d_tn.isInterpretedFinite())
+    // check whether we should terminate, which notice always treats
+    // uninterpreted sorts as infinite, since we do not put bounds on them
+    // in our enumeration.
+    if (isCardinalityClassFinite(d_tn.getCardinalityClass(), false))
     {
       if (ncc == tc.getNumConstructorClasses())
       {
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 05547aa8a..301299f11 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -202,7 +202,8 @@ void TheorySep::postProcessModel( TheoryModel* m ){
           Trace("sep-model") << "_";
           //m->d_comment_str << "_";
           TypeEnumerator te_range( data_type );
-          if( data_type.isInterpretedFinite() ){
+          if (d_state.isFiniteType(data_type))
+          {
             pto_children.push_back( *te_range );
           }else{
             //must enumerate until we find one that is not explicitly pointed to
@@ -820,7 +821,7 @@ void TheorySep::postCheck(Effort level)
   {
     TypeNode data_type = d_loc_to_data_type[it->first];
     // if the data type is finite
-    if (!data_type.isInterpretedFinite())
+    if (!d_state.isFiniteType(data_type))
     {
       continue;
     }
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 8ba3cd9ea..a9a7429b4 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -85,8 +85,9 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
 {
   NodeManager* nm = NodeManager::currentNM();
   TypeNode setType = nm->mkSetType(t);
+  bool finiteType = d_state.isFiniteType(t);
   // skip infinite types that do not have univset terms
-  if (!t.isInterpretedFinite() && d_state.getUnivSetEqClass(setType).isNull())
+  if (!finiteType && d_state.getUnivSetEqClass(setType).isNull())
   {
     return;
   }
@@ -96,7 +97,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
 
   // cardinality of an interpreted finite type t is infinite when t
   // is infinite without --fmf
-  if (t.isInterpretedFinite() && card.isInfinite())
+  if (finiteType && card.isInfinite())
   {
     // TODO (#1123): support uninterpreted sorts with --finite-model-find
     std::stringstream message;
@@ -126,7 +127,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
   // get all equivalent classes of type t
   vector<Node> representatives = d_state.getSetsEqClasses(t);
 
-  if (t.isInterpretedFinite())
+  if (finiteType)
   {
     Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality()));
     Node cardUniv = nm->mkNode(kind::CARD, proxy);
@@ -998,6 +999,7 @@ void CardinalityExtension::mkModelValueElementsFor(
     TheoryModel* model)
 {
   TypeNode elementType = eqc.getType().getSetElementType();
+  bool elementTypeFinite = d_state.isFiniteType(elementType);
   if (isModelValueBasic(eqc))
   {
     std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
@@ -1018,14 +1020,14 @@ void CardinalityExtension::mkModelValueElementsFor(
       Assert(els.size() <= vu);
       NodeManager* nm = NodeManager::currentNM();
       SkolemManager* sm = nm->getSkolemManager();
-      if (elementType.isInterpretedFinite())
+      if (elementTypeFinite)
       {
         // get all members of this finite type
         collectFiniteTypeSetElements(model);
       }
       while (els.size() < vu)
       {
-        if (elementType.isInterpretedFinite())
+        if (elementTypeFinite)
         {
           // At this point we are sure the formula is satisfiable and all
           // cardinality constraints are satisfied. Since this type is finite,
@@ -1085,7 +1087,7 @@ void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
   }
   for (const Node& set : getOrderedSetsEqClasses())
   {
-    if (!set.getType().isInterpretedFinite())
+    if (!d_state.isFiniteType(set.getType()))
     {
       continue;
     }
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 61d0818c6..6ee88b298 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -539,7 +539,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
   {
     Assert(tn.isSequence());
     TypeNode etn = tn.getSequenceElementType();
-    if (etn.isInterpretedFinite())
+    if (d_state.isFiniteType(etn))
     {
       // infinite cardinality, we are fine
       return;
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index e546e6937..7f669e36d 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -41,7 +41,10 @@ std::string PreRegisterVisitor::toString() const {
  * current. This method is used by PreRegisterVisitor and SharedTermsVisitor
  * below.
  */
-bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent)
+bool isAlreadyVisited(TheoryEngine* te,
+                      TheoryIdSet visitedTheories,
+                      TNode current,
+                      TNode parent)
 {
   TheoryId currentTheoryId = Theory::theoryOf(current);
   if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
@@ -67,7 +70,7 @@ bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent)
 
   // do we need to consider the type?
   TypeNode type = current.getType();
-  if (currentTheoryId == parentTheoryId && !type.isInterpretedFinite())
+  if (currentTheoryId == parentTheoryId && !te->isFiniteType(type))
   {
     // current and parent are the same theory, and we are infinite, return true
     return true;
@@ -100,7 +103,7 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
   }
 
   TheoryIdSet visitedTheories = (*find).second;
-  return isAlreadyVisited(visitedTheories, current, parent);
+  return isAlreadyVisited(d_engine, visitedTheories, current, parent);
 }
 
 void PreRegisterVisitor::visit(TNode current, TNode parent) {
@@ -149,7 +152,7 @@ void PreRegisterVisitor::preRegister(TheoryEngine* te,
     // Note that if enclosed by different theories it's shared, for example,
     // in read(a, f(a)), f(a) should be shared with integers.
     TypeNode type = current.getType();
-    if (currentTheoryId != parentTheoryId || type.isInterpretedFinite())
+    if (currentTheoryId != parentTheoryId || te->isFiniteType(type))
     {
       // preregister with the type's theory, if necessary
       TheoryId typeTheoryId = Theory::theoryOf(type);
@@ -244,7 +247,7 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
   }
 
   TheoryIdSet visitedTheories = (*find).second;
-  return isAlreadyVisited(visitedTheories, current, parent);
+  return isAlreadyVisited(d_engine, visitedTheories, current, parent);
 }
 
 void SharedTermsVisitor::visit(TNode current, TNode parent) {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8c030351b..55c782f2f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1907,6 +1907,12 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
   }
 }
 
+bool TheoryEngine::isFiniteType(TypeNode tn) const
+{
+  return isCardinalityClassFinite(tn.getCardinalityClass(),
+                                  options::finiteModelFind());
+}
+
 void TheoryEngine::spendResource(Resource r)
 {
   d_resourceManager->spendResource(r);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4da9a38dd..b43488fa8 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -631,6 +631,24 @@ class TheoryEngine {
    */
   std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
 
+  //---------------------- information about cardinality of types
+  /**
+   * Is the cardinality of type tn finite? This method depends on whether
+   * finite model finding is enabled. If finite model finding is enabled, then
+   * we assume that all uninterpreted sorts have finite cardinality.
+   *
+   * Notice that if finite model finding is enabled, this method returns true
+   * if tn is an uninterpreted sort. It also returns true for the sort
+   * (Array Int U) where U is an uninterpreted sort. This type
+   * is finite if and only if U has cardinality one; for cases like this,
+   * we conservatively return that tn has finite cardinality.
+   *
+   * This method does *not* depend on the state of the theory engine, e.g.
+   * if U in the above example currently is entailed to have cardinality >1
+   * based on the assertions.
+   */
+  bool isFiniteType(TypeNode tn) const;
+  //---------------------- end information about cardinality of types
  private:
 
   /** Dump the assertions to the dump */
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 8396361bf..2103c3997 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -273,7 +273,13 @@ bool TheoryEngineModelBuilder::isCdtValueMatch(Node v,
   return false;
 }
 
-bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn)
+bool TheoryEngineModelBuilder::isFiniteType(TypeNode tn) const
+{
+  return isCardinalityClassFinite(tn.getCardinalityClass(),
+                                  options::finiteModelFind());
+}
+
+bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn) const
 {
   if (tn.isSort())
   {
@@ -837,7 +843,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       {
         const DType& dt = t.getDType();
         isCorecursive = dt.isCodatatype()
-                        && (!dt.isFinite(t) || dt.isRecursiveSingleton(t));
+                        && (!isFiniteType(t) || dt.isRecursiveSingleton(t));
       }
 #ifdef CVC5_ASSERTIONS
       bool isUSortFiniteRestricted = false;
@@ -914,13 +920,13 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
             n = itAssigner->second.getNextAssignment();
             Assert(!n.isNull());
           }
-          else if (t.isSort() || !t.isInterpretedFinite())
+          else if (t.isSort() || !isFiniteType(t))
           {
             // If its interpreted as infinite, we get a fresh value that does
             // not occur in the model.
             // Note we also consider uninterpreted sorts to be infinite here
-            // regardless of whether isInterpretedFinite is true (which is true
-            // for uninterpreted sorts iff finite model finding is enabled).
+            // regardless of whether the cardinality class of t is
+            // CardinalityClass::INTERPRETED_FINITE.
             // This is required because the UF solver does not explicitly
             // assign uninterpreted constants to equivalence classes in its
             // collectModelValues method. Doing so would have the same effect
diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 5652dc7ab..2ed8e2be6 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -299,9 +299,14 @@ class TheoryEngineModelBuilder
   bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
   //------------------------------------end for codatatypes
 
+  /**
+   * Is the given type constrained to be finite? This depends on whether
+   * finite model finding is enabled.
+   */
+  bool isFiniteType(TypeNode tn) const;
   //---------------------------------for debugging finite model finding
   /** does type tn involve an uninterpreted sort? */
-  bool involvesUSort(TypeNode tn);
+  bool involvesUSort(TypeNode tn) const;
   /** is v an excluded value based on uninterpreted sorts?
    * This gives an assertion failure in the case that v contains
    * an uninterpreted constant whose index is out of the bounds
diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp
index e6d36033a..5ac5e6ae9 100644
--- a/src/theory/theory_state.cpp
+++ b/src/theory/theory_state.cpp
@@ -172,6 +172,11 @@ context::CDList<Assertion>::const_iterator TheoryState::factsEnd(TheoryId tid)
   return d_valuation.factsEnd(tid);
 }
 
+bool TheoryState::isFiniteType(TypeNode tn) const
+{
+  return d_valuation.isFiniteType(tn);
+}
+
 Valuation& TheoryState::getValuation() { return d_valuation; }
 
 }  // namespace theory
diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h
index 850f42da0..933f44d2b 100644
--- a/src/theory/theory_state.h
+++ b/src/theory/theory_state.h
@@ -101,6 +101,11 @@ class TheoryState
   context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
   /** The beginning iterator of facts for theory tid.*/
   context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
+  /**
+   * Is the cardinality of type tn finite? This method depends on whether
+   * finite model finding is enabled. For details, see theory_engine.h.
+   */
+  bool isFiniteType(TypeNode tn) const;
 
   /** Get the underlying valuation class */
   Valuation& getValuation();
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index edd61fd2a..13709c2ab 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -212,7 +212,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
       hasFunctions = true;
       // if during collect model, must have an infinite type
       // if not during collect model, must have a finite type
-      if (tn.isInterpretedFinite() != isCollectModel)
+      if (d_state.isFiniteType(tn) != isCollectModel)
       {
         func_eqcs[tn].push_back(eqc);
         Trace("uf-ho-debug")
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index c72c4e487..937fcd5fa 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -220,5 +220,10 @@ context::CDList<Assertion>::const_iterator Valuation::factsEnd(TheoryId tid)
   return theory->facts_end();
 }
 
+bool Valuation::isFiniteType(TypeNode tn) const
+{
+  return d_engine->isFiniteType(tn);
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index af7e4205e..9eaf24616 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -215,6 +215,11 @@ public:
   context::CDList<Assertion>::const_iterator factsBegin(TheoryId tid);
   /** The beginning iterator of facts for theory tid.*/
   context::CDList<Assertion>::const_iterator factsEnd(TheoryId tid);
+  /**
+   * Is the cardinality of type tn finite? This method depends on whether
+   * finite model finding is enabled. For details, see theory_engine.h.
+   */
+  bool isFiniteType(TypeNode tn) const;
 };/* class Valuation */
 
 }  // namespace theory
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index c7f7e780c..ea4ece8dd 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -29,6 +29,8 @@ libcvc4_add_sources(
   bool.h
   cardinality.cpp
   cardinality.h
+  cardinality_class.cpp
+  cardinality_class.h
   dense_map.h
   divisible.cpp
   divisible.h
diff --git a/test/regress/regress0/fmf/issue4260-arrays-card-one.smt2 b/test/regress/regress0/fmf/issue4260-arrays-card-one.smt2
new file mode 100644
index 000000000..bdd5e3347
--- /dev/null
+++ b/test/regress/regress0/fmf/issue4260-arrays-card-one.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic AUFNIA)
+(declare-sort S0 0)
+(declare-const a (Array Int S0))
+(declare-const b (Array Int S0))
+(assert (distinct b a))
+(check-sat)