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

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d5d296579d7eea448223baaedae94cd157543a34..0b17731141c92fc181c878fb7ef672e0339e6dfb 100644 (file)
--- 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 dfab42dadcc6e8abbe3e5fd4b332b9e108fdb172..f52658a03380b1b4d59f9b3c67dea4f084b6c01d 100644 (file)
--- 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 c06691d08e5148c0609e306263588178c45b4fbd..8001ca3df5475d0f5f49fbcea3d95dd34dd6c12c 100644 (file)
--- 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 65b422a5382010e0b5cd2147088ffd7ffa7ae463..72d00a5a250fa71edc3fbc07c983407f3a324681 100644 (file)
--- 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.
    *

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 370e5d3488d66aef0def0ef62b9933929779a619..777f6e57fc7c4eaf75da73d713da5a1d0723273e 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -77,10 +77,7 @@ class EqualityTypeRule {
     if( check ) {
       TypeNode lhsType = n[0].getType(check);
       TypeNode rhsType = n[1].getType(check);
-
-      // TODO : we may want to limit cases where we have equalities between terms of different types 
-      //   equalities between (Set Int) and (Set Real) already cause strange issues in theory solver for sets
-      //   one possibility is to only allow this for Int/Real
+      
       if ( TypeNode::leastCommonTypeNode(lhsType, rhsType).isNull() ) {
         std::stringstream ss;
         ss << "Subexpressions must have a common base type:" << std::endl;
@@ -90,6 +87,7 @@ class EqualityTypeRule {
 
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }
+      // TODO : check isFirstClass for these types? (github issue #1202)
     }
     return booleanType;
   }