diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-30 00:16:47 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-06-30 00:16:47 -0400 |
commit | 841c33c4b0b22c73951634fa6df5bf1b7065adbf (patch) | |
tree | e9295d98912bbf5133748a4d62d49fb6e2c59b2b /src | |
parent | a401cd2deb921c3499d8fdbe0d14cfee67c92737 (diff) |
fix smt2 parameterized sort printing
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 79cb18d92..5cc044272 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -288,10 +288,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(n.getKind() == kind::SORT_TYPE) { string name; + if(n.getNumChildren() != 0) { + out << '('; + } if(n.getAttribute(expr::VarNameAttr(), name)) { out << maybeQuoteSymbol(name); - return; } + if(n.getNumChildren() != 0) { + for(unsigned i = 0; i < n.getNumChildren(); ++i) { + out << ' '; + toStream(out, n[i], toDepth, types); + } + out << ')'; + } + return; } bool stillNeedToPrintParams = true; |