Ho node manager types (#1203)

* Remove restrictions about function types

* Introduce notion of first-class type, improve assertions, add comment on equality type rule.

* Update comment

4 files changed, 41 insertions, 20 deletions

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d5d296579..0b1773114 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1075,10 +1075,12 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
   Assert(sorts.size() >= 2);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(!sorts[i].isFunctionLike(), sorts,
-                  "cannot create higher-order function types");
+    CheckArgument(sorts[i].isFirstClass(), sorts,
+                  "cannot create function types for argument types that are not first-class");
     sortNodes.push_back(sorts[i]);
   }
+  CheckArgument(!sorts[sorts.size()-1].isFunction(), sorts[sorts.size()-1],
+                "must flatten function types");
   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 }
 
@@ -1087,8 +1089,8 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   Assert(sorts.size() >= 1);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(!sorts[i].isFunctionLike(), sorts,
-                  "cannot create higher-order function types");
+    CheckArgument(sorts[i].isFirstClass(), sorts,
+                  "cannot create predicate types for argument types that are not first-class");
     sortNodes.push_back(sorts[i]);
   }
   sortNodes.push_back(booleanType());
@@ -1121,10 +1123,10 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                 "unexpected NULL index type");
   CheckArgument(!constituentType.isNull(), constituentType,
                 "unexpected NULL constituent type");
-  CheckArgument(!indexType.isFunctionLike(), indexType,
-                "cannot index arrays by a function-like type");
-  CheckArgument(!constituentType.isFunctionLike(), constituentType,
-                "cannot store function-like types in arrays");
+  CheckArgument(indexType.isFirstClass(), indexType,
+                "cannot index arrays by types that are not first-class");
+  CheckArgument(constituentType.isFirstClass(), constituentType,
+                "cannot store types that are not first-class in arrays");
   Debug("arrays") << "making array type " << indexType << " "
                   << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
@@ -1133,24 +1135,23 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
 inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
   CheckArgument(!elementType.isNull(), elementType,
                 "unexpected NULL element type");
-  // TODO: Confirm meaning of isFunctionLike(). --K
-  CheckArgument(!elementType.isFunctionLike(), elementType,
-                "cannot store function-like types in sets");
+  CheckArgument(elementType.isFirstClass(), elementType,
+                "cannot store types that are not first-class in sets");
   Debug("sets") << "making sets type " << elementType << std::endl;
   return mkTypeNode(kind::SET_TYPE, elementType);
 }
 
 inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
-  CheckArgument(!domain.isFunctionLike(), domain,
-                "cannot create higher-order function types");
-  CheckArgument(!range.isFunctionLike(), range,
-                "cannot create higher-order function types");
+  CheckArgument(domain.isDatatype(), domain,
+                "cannot create non-datatype selector type");
+  CheckArgument(range.isFirstClass(), range,
+                "cannot have selector fields that are not first-class types");
   return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
 }
 
 inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
-  CheckArgument(!domain.isFunctionLike(), domain,
-                "cannot create higher-order function types");
+  CheckArgument(domain.isDatatype(), domain,
+                "cannot create non-datatype tester");
   return mkTypeNode(kind::TESTER_TYPE, domain );
 }
 
diff --git a/src/expr/type.h b/src/expr/type.h
index dfab42dad..f52658a03 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -59,9 +59,6 @@ class FunctionType;
 class SExprType;
 class SortType;
 class SortConstructorType;
-// not in release 1.0
-//class PredicateSubtype;
-class SubrangeType;
 class Type;
 
 /** Hash function for Types */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index c06691d08..8001ca3df 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -22,6 +22,7 @@
 #include "options/base_options.h"
 #include "options/expr_options.h"
 #include "options/quantifiers_options.h"
+#include "options/uf_options.h"
 
 using namespace std;
 
@@ -86,6 +87,16 @@ bool TypeNode::isInterpretedFinite() const {
   }
 }
 
+bool TypeNode::isFirstClass() const {
+  return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) && 
+         getKind() != kind::CONSTRUCTOR_TYPE &&
+         getKind() != kind::SELECTOR_TYPE &&
+         getKind() != kind::TESTER_TYPE &&
+         getKind() != kind::SEXPR_TYPE &&
+         ( getKind() != kind::TYPE_CONSTANT ||
+           getConst<TypeConstant>() != REGEXP_TYPE );
+}
+
 bool TypeNode::isWellFounded() const {
   return kind::isWellFounded(*this);
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 65b422a53..72d00a5a2 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -429,6 +429,18 @@ public:
    */
   bool isInterpretedFinite() const;
 
+
+  /**
+   * Is this a first-class type?
+   * First-class types are types for which:
+   * (1) we handle equalities between terms of that type, and 
+   * (2) they are allowed to be parameters of parametric types (e.g. index or element types of arrays).
+   *
+   * Examples of types that are not first-class include constructor types,
+   * selector types, tester types, regular expressions and SExprs.
+   */
+  bool isFirstClass() const;
+
   /**
    * Returns whether this type is well-founded.
    *