2 files changed, 69 insertions, 49 deletions

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 7eec52b19..8e86ba49d 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -153,60 +153,39 @@ Cardinality DTypeConstructor::getCardinality(TypeNode t) const
 
 bool DTypeConstructor::isFinite(TypeNode t) const
 {
-  Assert(isResolved());
-
-  TNode self = d_constructor;
-  // is this already in the cache ?
-  if (self.getAttribute(DTypeFiniteComputedAttr()))
-  {
-    return self.getAttribute(DTypeFiniteAttr());
-  }
-  std::vector<TypeNode> instTypes;
-  std::vector<TypeNode> paramTypes;
-  bool isParam = t.isParametricDatatype();
-  if (isParam)
-  {
-    paramTypes = t.getDType().getParameters();
-    instTypes = TypeNode(t).getParamTypes();
-  }
-  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
-  {
-    TypeNode tc = getArgType(i);
-    if (isParam)
-    {
-      tc = tc.substitute(paramTypes.begin(),
-                         paramTypes.end(),
-                         instTypes.begin(),
-                         instTypes.end());
-    }
-    if (!tc.isFinite())
-    {
-      self.setAttribute(DTypeFiniteComputedAttr(), true);
-      self.setAttribute(DTypeFiniteAttr(), false);
-      return false;
-    }
-  }
-  self.setAttribute(DTypeFiniteComputedAttr(), true);
-  self.setAttribute(DTypeFiniteAttr(), true);
-  return true;
+  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
+  return cinfo.first == CardinalityType::FINITE;
 }
 
 bool DTypeConstructor::isInterpretedFinite(TypeNode t) const
 {
-  Assert(isResolved());
-  TNode self = d_constructor;
-  // is this already in the cache ?
-  if (self.getAttribute(DTypeUFiniteComputedAttr()))
+  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
+  return cinfo.first != CardinalityType::INFINITE;
+}
+
+bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const
+{
+  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
+  return cinfo.second;
+}
+
+std::pair<DTypeConstructor::CardinalityType, bool>
+DTypeConstructor::computeCardinalityInfo(TypeNode t) const
+{
+  std::map<TypeNode, std::pair<CardinalityType, bool> >::iterator it =
+      d_cardInfo.find(t);
+  if (it != d_cardInfo.end())
   {
-    return self.getAttribute(DTypeUFiniteAttr());
+    return it->second;
   }
+  std::pair<CardinalityType, bool> ret(CardinalityType::FINITE, false);
   std::vector<TypeNode> instTypes;
   std::vector<TypeNode> paramTypes;
   bool isParam = t.isParametricDatatype();
   if (isParam)
   {
     paramTypes = t.getDType().getParameters();
-    instTypes = TypeNode(t).getParamTypes();
+    instTypes = t.getParamTypes();
   }
   for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++)
   {
@@ -218,16 +197,30 @@ bool DTypeConstructor::isInterpretedFinite(TypeNode t) const
                          instTypes.begin(),
                          instTypes.end());
     }
-    if (!tc.isInterpretedFinite())
+    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
     {
-      self.setAttribute(DTypeUFiniteComputedAttr(), true);
-      self.setAttribute(DTypeUFiniteAttr(), false);
-      return false;
+      // 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();
   }
-  self.setAttribute(DTypeUFiniteComputedAttr(), true);
-  self.setAttribute(DTypeUFiniteAttr(), true);
-  return true;
+  d_cardInfo[t] = ret;
+  return ret;
 }
 
 bool DTypeConstructor::isResolved() const { return !d_tester.isNull(); }
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index fc414c756..2dba895e9 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -158,6 +158,13 @@ class DTypeConstructor
    * only be called for resolved constructors.
    */
   bool isInterpretedFinite(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
+   * finite type. This function can only be called for resolved constructors.
+   *
+   */
+  bool hasFiniteExternalArgType(TypeNode t) const;
 
   /**
    * Returns true iff this constructor has already been
@@ -229,6 +236,17 @@ 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
@@ -286,6 +304,13 @@ class DTypeConstructor
                          std::vector<TypeNode>& processing,
                          std::map<TypeNode, Node>& gt,
                          bool isValue) const;
+  /**
+   * Compute cardinality info, returns a pair where its first component is
+   * an identifier indicating the cardinality type of this constructor for
+   * 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;
   /** compute shared selectors
    * This computes the maps d_sharedSelectors and d_sharedSelectorIndex.
    */
@@ -324,6 +349,8 @@ class DTypeConstructor
    * its argument index for this constructor.
    */
   mutable std::map<TypeNode, std::map<Node, unsigned> > d_sharedSelectorIndex;
+  /**  A cache for computeCardinalityInfo. */
+  mutable std::map<TypeNode, std::pair<CardinalityType, bool> > d_cardInfo;
 }; /* class DTypeConstructor */
 
 /**