Printing for higher-order (#1347)

1 files changed, 11 insertions, 7 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 3caeeaaaa..8a80ba59e 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -363,13 +363,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     break;
   case kind::CHAIN: break;
   case kind::FUNCTION_TYPE:
-    for(size_t i = 0; i < n.getNumChildren() - 1; ++i) {
-      if(i > 0) {
-        out << ' ';
-      }
-      out << n[i];
+    out << "->";
+    for(size_t i = 0; i < n.getNumChildren(); ++i) {
+      out << " ";
+      toStream(out, n[i], toDepth, types, TypeNode::null());
     }
-    out << ") " << n[n.getNumChildren() - 1];
+    out << ")";
     return;
   case kind::SEXPR: break;
 
@@ -383,7 +382,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
 
     // uf theory
   case kind::APPLY_UF: typeChildren = true; break;
-
+    // higher-order
+  case kind::HO_APPLY: break;
+  case kind::LAMBDA: out << smtKindString(k) << " "; break;
+  
     // arith theory
   case kind::PLUS:
   case kind::MULT:
@@ -817,6 +819,8 @@ static string smtKindString(Kind k) throw() {
 
     // uf theory
   case kind::APPLY_UF: break;
+  
+  case kind::LAMBDA: return "lambda";
 
     // arith theory
   case kind::PLUS: return "+";