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, 18 insertions, 0 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 97f434e9b..409518fcf 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -85,6 +85,24 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
       out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
       break;
     }
+    case kind::TYPE_CONSTANT:
+      switch(TypeConstant tc = n.getConst<TypeConstant>()) {
+      case REAL_TYPE:
+        out << "REAL";
+        break;
+      case INTEGER_TYPE:
+        out << "INT";
+        break;
+      case BOOLEAN_TYPE:
+        out << "BOOLEAN";
+        break;
+      case KIND_TYPE:
+        out << "TYPE";
+        break;
+      default:
+        Unhandled(tc);
+      }
+      break;
     case kind::BUILTIN:
       switch(Kind k = n.getConst<Kind>()) {
       case kind::EQUAL: out << '='; break;