diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 11 |
3 files changed, 15 insertions, 2 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 77d8f14de..16f5f5c51 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -661,6 +661,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << n.getOperator().getConst<BitVectorExtract>(); opType = POSTFIX; break; + case kind::BITVECTOR_BITOF: + op << n.getOperator().getConst<BitVectorBitOf>(); + opType = POSTFIX; + break; case kind::BITVECTOR_REPEAT: out << "BVREPEAT("; toStream(out, n[0], depth, types, false); diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index a68c3ca7f..4fb2ff12c 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -37,7 +37,7 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { using namespace CVC4::language::output; switch(lang) { - case LANG_SMTLIB_V1: + case LANG_SMTLIB_V1: // TODO the printer return new printer::smt1::Smt1Printer(); case LANG_SMTLIB_V2: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 36494e1de..a903b2576 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -250,6 +250,15 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::DISTINCT: out << smtKindString(k) << " "; break; case kind::CHAIN: break; case kind::TUPLE: break; + case kind::FUNCTION_TYPE: + for(size_t i = 0; i < n.getNumChildren() - 1; ++i) { + if(i > 0) { + out << ' '; + } + out << n[i]; + } + out << ") " << n[n.getNumChildren() - 1]; + return; case kind::SEXPR: break; // bool theory @@ -455,7 +464,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ) { out << '('; - toStream(out, (*i), toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0); out << ' '; out << (*i).getType(); // The following code do stange things |