From 5ab5104c4328bcaca155eff5869c601f589c086d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 10 Nov 2017 07:53:32 -0600 Subject: [PATCH] Printing for higher-order (#1347) --- src/printer/smt2/smt2_printer.cpp | 18 +++++++++++------- 1 file 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 "+"; -- 2.30.2