Tuesday end-of-day commit.

Expected performance impact outside of datatypes/CVC parser is
negligible.

* CVC language LAMBDA, functional LET, type LET, precedence fixes,
  bitvectors, and arrays, with partial parsing support also for
  quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
    tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
  these are complicated because they have to be left unresolved
  at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
  (not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items

1 files changed, 11 insertions, 3 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 9449594e3..716e2a3b3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -519,18 +519,26 @@ TypeNode NodeManager::getType(TNode n, bool check)
   return typeNode;
 }
 
-TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor, TypeNode range) {
+TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor,
+                                        TypeNode range) {
   std::vector<TypeNode> sorts;
   Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
   for(Datatype::Constructor::const_iterator i = constructor.begin();
       i != constructor.end();
       ++i) {
-    Debug("datatypes") << *(*i).getSelector().getType().d_typeNode << std::endl;
-    TypeNode sort = (*(*i).getSelector().getType().d_typeNode)[1];
+    TypeNode selectorType = *(*i).getSelector().getType().d_typeNode;
+    Debug("datatypes") << selectorType << std::endl;
+    TypeNode sort = selectorType[1];
+
+    // should be guaranteed here already, but just in case
+    Assert(!sort.isFunctionLike());
+
     Debug("datatypes") << "ctor sort: " << sort << std::endl;
     sorts.push_back(sort);
   }
   Debug("datatypes") << "ctor range: " << range << std::endl;
+  CheckArgument(!range.isFunctionLike(), range,
+                "cannot create higher-order function types");
   sorts.push_back(range);
   return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
 }