Make isClosedEnumerable a member of TypeNode (#2434)

2 files changed, 69 insertions, 0 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 6616f470f..b54290612 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -165,6 +165,62 @@ bool TypeNode::isInterpretedFinite()
   return getAttribute(IsInterpretedFiniteAttr());
 }
 
+/** Attribute true for types that are closed enumerable */
+struct IsClosedEnumerableTag
+{
+};
+struct IsClosedEnumerableComputedTag
+{
+};
+typedef expr::Attribute<IsClosedEnumerableTag, bool> IsClosedEnumerableAttr;
+typedef expr::Attribute<IsClosedEnumerableComputedTag, bool>
+    IsClosedEnumerableComputedAttr;
+
+bool TypeNode::isClosedEnumerable()
+{
+  // check it is already cached
+  if (!getAttribute(IsClosedEnumerableComputedAttr()))
+  {
+    bool ret = true;
+    if (isArray() || isSort() || isCodatatype() || isFunction())
+    {
+      ret = false;
+    }
+    else if (isSet())
+    {
+      ret = getSetElementType().isClosedEnumerable();
+    }
+    else if (isDatatype())
+    {
+      // avoid infinite loops: initially set to true
+      setAttribute(IsClosedEnumerableAttr(), ret);
+      setAttribute(IsClosedEnumerableComputedAttr(), true);
+      TypeNode tn = *this;
+      const Datatype& dt = getDatatype();
+      for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+      {
+        for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+        {
+          TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+          if (tn != ctn && !ctn.isClosedEnumerable())
+          {
+            ret = false;
+            break;
+          }
+        }
+        if (!ret)
+        {
+          break;
+        }
+      }
+    }
+    setAttribute(IsClosedEnumerableAttr(), ret);
+    setAttribute(IsClosedEnumerableComputedAttr(), true);
+    return ret;
+  }
+  return getAttribute(IsClosedEnumerableAttr());
+}
+
 bool TypeNode::isFirstClass() const {
   return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) && 
          getKind() != kind::CONSTRUCTOR_TYPE &&
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 9cb6efc29..5b0caf659 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -429,6 +429,19 @@ public:
    */
   bool isInterpretedFinite();
 
+  /** is closed enumerable type
+   *
+   * This returns true if this type has an enumerator that produces constants
+   * that are fully handled by CVC4's quantifier-free theory solvers. Examples
+   * of types that are not closed enumerable are:
+   * (1) uninterpreted sorts,
+   * (2) arrays,
+   * (3) codatatypes,
+   * (4) functions,
+   * (5) parametric sorts involving any of the above.
+   */
+  bool isClosedEnumerable();
+
   /**
    * Is this a first-class type?
    * First-class types are types for which: