Optimizations and fixes for computing whether a type is finite (#2179)

1 files changed, 62 insertions, 27 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index d6cf12d41..6616f470f 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -83,46 +83,81 @@ bool TypeNode::isInterpretedFinite()
   if (!getAttribute(IsInterpretedFiniteComputedAttr()))
   {
     bool isInterpretedFinite = false;
-    if (getCardinality().isFinite())
+    if (isSort())
+    {
+      // If the finite model finding flag is set, we treat uninterpreted sorts
+      // as finite. If it is not set, we treat them implicitly as infinite
+      // sorts (that is, their cardinality is not constrained to be finite).
+      isInterpretedFinite = options::finiteModelFind();
+    }
+    else if (isBitVector() || isFloatingPoint())
     {
       isInterpretedFinite = true;
     }
-    else if (options::finiteModelFind())
+    else if (isDatatype())
     {
-      if( isSort() ){
-        isInterpretedFinite = true;
-      }else if( isDatatype() ){
-        TypeNode tn = *this;
-        const Datatype& dt = getDatatype();
-        isInterpretedFinite = dt.isInterpretedFinite(tn.toType());
-      }else if( isArray() ){
-        isInterpretedFinite =
-            getArrayIndexType().isInterpretedFinite()
-            && getArrayConstituentType().isInterpretedFinite();
-      }else if( isSet() ) {
-        isInterpretedFinite = getSetElementType().isInterpretedFinite();
+      TypeNode tn = *this;
+      const Datatype& dt = getDatatype();
+      isInterpretedFinite = dt.isInterpretedFinite(tn.toType());
+    }
+    else if (isArray())
+    {
+      TypeNode tnc = getArrayConstituentType();
+      if (!tnc.isInterpretedFinite())
+      {
+        // arrays with consistuent type that is infinite are infinite
+        isInterpretedFinite = false;
       }
-      else if (isFunction())
+      else if (getArrayIndexType().isInterpretedFinite())
       {
+        // arrays with both finite consistuent and index types are finite
         isInterpretedFinite = true;
-        if (!getRangeType().isInterpretedFinite())
-        {
-          isInterpretedFinite = false;
-        }
-        else
+      }
+      else
+      {
+        // If the consistuent type of the array has cardinality one, then the
+        // array type has cardinality one, independent of the index type.
+        isInterpretedFinite = tnc.getCardinality().isOne();
+      }
+    }
+    else if (isSet())
+    {
+      isInterpretedFinite = getSetElementType().isInterpretedFinite();
+    }
+    else if (isFunction())
+    {
+      isInterpretedFinite = true;
+      TypeNode tnr = getRangeType();
+      if (!tnr.isInterpretedFinite())
+      {
+        isInterpretedFinite = false;
+      }
+      else
+      {
+        std::vector<TypeNode> argTypes = getArgTypes();
+        for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
         {
-          std::vector<TypeNode> argTypes = getArgTypes();
-          for (unsigned i = 0, nargs = argTypes.size(); i < nargs; i++)
+          if (!argTypes[i].isInterpretedFinite())
           {
-            if (!argTypes[i].isInterpretedFinite())
-            {
-              isInterpretedFinite = false;
-              break;
-            }
+            isInterpretedFinite = false;
+            break;
           }
         }
+        if (!isInterpretedFinite)
+        {
+          // similar to arrays, functions are finite if their range type
+          // has cardinality one, regardless of the arguments.
+          isInterpretedFinite = tnr.getCardinality().isOne();
+        }
       }
     }
+    else
+    {
+      // 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.
+      isInterpretedFinite = getCardinality().isFinite();
+    }
     setAttribute(IsInterpretedFiniteAttr(), isInterpretedFinite);
     setAttribute(IsInterpretedFiniteComputedAttr(), true);
     return isInterpretedFinite;