Minor cleanup stuff.

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 77d8f14decafb5b18b462e2a54c5733325c6b7d8..16f5f5c51c362daf8ab6eae67971e7e6fa2d5036 100644 (file)
--- 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 a68c3ca7fe547cb4334f39d3b6836513f0d2fa78..4fb2ff12ca91f15c8aa9c9e4b0a050f053f5f167 100644 (file)
--- 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 36494e1dee2ac77c226f7f35977d7d4c70ac9b53..a903b257648595d3556517f7ce4c6fa603edb5b4 100644 (file)
--- 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 c5c9828dfa8f1e04c6704edb62d4f8a5d18025ca..8a1ab26af07042cf988b554b33b5828935bf77b3 100644 (file)
--- 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 */