diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-20 11:19:50 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-20 11:19:50 +0000 |
| commit | 2499bd64a5ac688573ebbcd6114983f64a8094eb (patch) | |
| tree | 0d49608cf7c21298fbeb8606fa1943c96beb8652 /src/printer | |
| parent | 5a98094e8eee680d4f489e901107dfc484a1679f (diff) | |
numerous bugfixes
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 27 |
1 files changed, 23 insertions, 4 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e23d7c88b..b83fd42dc 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -198,12 +198,23 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, case kind::FUNCTION_TYPE: case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: - case kind::TESTER_TYPE: - if(n.getNumChildren() > 0) { - copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " -> ")); - out << n[n.getNumChildren() - 1]; + if(n.getNumChildren() > 2) { + out << '('; + for(unsigned i = 0; i < n.getNumChildren() - 2; ++i) { + out << n[i] << ", "; + } + out << n[n.getNumChildren() - 2] + << ") -> " << n[n.getNumChildren() - 1]; + } else if(n.getNumChildren() == 2) { + out << n[0] << " -> " << n[1]; + } else { + Assert(n.getNumChildren() == 1); + out << n[0]; } break; + case kind::TESTER_TYPE: + out << n[0] << " -> BOOLEAN"; + break; case kind::ARRAY_TYPE: out << "ARRAY " << n[0] << " OF " << n[1]; @@ -265,6 +276,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << n.getOperator() << '(' << n[0] << ',' << n[1] << ')'; break; + // N-ary infix + case kind::BITVECTOR_CONCAT: + out << '('; + for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) { + cout << n[i] << ' ' << n.getOperator(); + } + out << n[n.getNumChildren() - 1] << ')'; + default: if(k == kind::NOT && n[0].getKind() == kind::EQUAL) { // collapse NOT-over-EQUAL |