From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 22 Jun 2014 04:32:33 +0000 (-0400)
Subject: Minor cleanup stuff.
X-Git-Tag: cvc5-1.0.0~6738
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=542156e0f589dfe89ca7fb5736b44b05cb653ab6;p=cvc5.git

Minor cleanup stuff.
---

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
diff --git a/src/util/language.cpp b/src/util/language.cpp
index c5c9828df..8a1ab26af 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -110,7 +110,7 @@ InputLanguage toInputLanguage(std::string language) {
     return input::LANG_AUTO;
   }
 
-  throw OptionException(std::string("unknown input language " + language + "'"));
+  throw OptionException(std::string("unknown input language `" + language + "'"));
 }/* toInputLanguage() */
 
 }/* CVC4::language namespace */