diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-10 07:53:32 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-10 07:53:32 -0600 |
commit | 5ab5104c4328bcaca155eff5869c601f589c086d (patch) | |
tree | b6e357f4e08b204e63f99903d2fa0ea006d1aeef /src/printer | |
parent | 8ada7b0ac4b3832d8fbf5e31080cb85df330049f (diff) |
Printing for higher-order (#1347)
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 18 |
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 "+"; |