Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer

implemented.  This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0.  Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder.  (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)

12 files changed, 704 insertions, 0 deletions

diff --git a/src/printer/Makefile b/src/printer/Makefile
new file mode 100644
index 000000000..72baefbd9
--- /dev/null
+++ b/src/printer/Makefile
@@ -0,0 +1,4 @@
+topdir = ../..
+srcdir = src/printer
+
+include $(topdir)/Makefile.subdir
diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am
new file mode 100644
index 000000000..8fd50d823
--- /dev/null
+++ b/src/printer/Makefile.am
@@ -0,0 +1,21 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libprinter.la
+
+libprinter_la_SOURCES = \
+	printer.h \
+	printer.cpp \
+	ast/ast_printer.h \
+	ast/ast_printer.cpp \
+	smt/smt_printer.h \
+	smt/smt_printer.cpp \
+	smt2/smt2_printer.h \
+	smt2/smt2_printer.cpp \
+	cvc/cvc_printer.h \
+	cvc/cvc_printer.cpp
+
+libprinter_la_LIBADD = \
+	@builddir@/../lib/libreplacements.la
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
new file mode 100644
index 000000000..cd9b0cad5
--- /dev/null
+++ b/src/printer/ast/ast_printer.cpp
@@ -0,0 +1,100 @@
+/*********************                                                        */
+/*! \file ast_printer.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the AST output language
+ **
+ ** The pretty-printer interface for the AST output language.
+ **/
+
+#include "printer/ast/ast_printer.h"
+#include "util/language.h" // for LANG_AST
+#include "expr/node_manager.h" // for VarNameAttr
+
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+namespace printer {
+namespace ast {
+
+std::ostream& AstPrinter::toStream(std::ostream& out, TNode n,
+                                   int toDepth, bool types) const {
+  // null
+  if(n.getKind() == kind::NULL_EXPR) {
+    out << "null";
+    return out;
+  }
+
+  // variable
+  if(n.getMetaKind() == kind::metakind::VARIABLE) {
+    if(n.getKind() != kind::VARIABLE &&
+       n.getKind() != kind::SORT_TYPE) {
+      out << n.getKind() << ':';
+    }
+
+    string s;
+    if(n.getAttribute(expr::VarNameAttr(), s)) {
+      out << s;
+    } else {
+      out << "var_" << n.getId();
+    }
+    if(types) {
+      // print the whole type, but not *its* type
+      out << ":";
+      n.getType().toStream(out, -1, false, language::output::LANG_AST);
+    }
+
+    return out;
+  }
+
+  out << '(' << n.getKind();
+  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+    // constant
+    out << ' ';
+    kind::metakind::NodeValueConstPrinter::toStream(out, n);
+  } else {
+    // operator
+    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+      out << ' ';
+      if(toDepth != 0) {
+        n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+                                 types, language::output::LANG_AST);
+      } else {
+        out << "(...)";
+      }
+    }
+    for(TNode::iterator i = n.begin(),
+          iend = n.end();
+        i != iend;
+        ++i) {
+      if(i != iend) {
+        out << ' ';
+      }
+      if(toDepth != 0) {
+        (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+                      types, language::output::LANG_AST);
+      } else {
+        out << "(...)";
+      }
+    }
+  }
+  out << ')';
+
+  return out;
+}/* AstPrinter::toStream() */
+
+}/* CVC4::printer::ast namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
new file mode 100644
index 000000000..0851aef6c
--- /dev/null
+++ b/src/printer/ast/ast_printer.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file ast_printer.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the AST output language
+ **
+ ** The pretty-printer interface for the AST output language.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__AST_PRINTER_H
+#define __CVC4__PRINTER__AST_PRINTER_H
+
+#include <iostream>
+
+#include "printer/printer.h"
+
+namespace CVC4 {
+namespace printer {
+namespace ast {
+
+class AstPrinter : public CVC4::Printer {
+public:
+  std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+};/* class AstPrinter */
+
+}/* CVC4::printer::ast namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__AST_PRINTER_H */
+
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
new file mode 100644
index 000000000..aebaf7ae5
--- /dev/null
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file cvc_printer.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the CVC output language
+ **
+ ** The pretty-printer interface for the CVC output language.
+ **/
+
+#include "printer/cvc/cvc_printer.h"
+
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+namespace printer {
+namespace cvc {
+
+std::ostream& CvcPrinter::toStream(std::ostream& out, TNode n,
+                                   int toDepth, bool types) const {
+  return out;
+}/* CvcPrinter::toStream() */
+
+}/* CVC4::printer::cvc namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
new file mode 100644
index 000000000..53889a989
--- /dev/null
+++ b/src/printer/cvc/cvc_printer.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file cvc_printer.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the CVC output language
+ **
+ ** The pretty-printer interface for the CVC output language.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__CVC_PRINTER_H
+#define __CVC4__PRINTER__CVC_PRINTER_H
+
+#include <iostream>
+
+#include "printer/printer.h"
+
+namespace CVC4 {
+namespace printer {
+namespace cvc {
+
+class CvcPrinter : public CVC4::Printer {
+public:
+  std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+};/* class CvcPrinter */
+
+}/* CVC4::printer::cvc namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__CVC_PRINTER_H */
+
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
new file mode 100644
index 000000000..a2a9b3378
--- /dev/null
+++ b/src/printer/printer.cpp
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file printer.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Base of the pretty-printer interface
+ **
+ ** Base of the pretty-printer interface.
+ **/
+
+#include "printer/printer.h"
+
+#include "util/language.h"
+
+#include "printer/smt/smt_printer.h"
+#include "printer/smt2/smt2_printer.h"
+#include "printer/cvc/cvc_printer.h"
+#include "printer/ast/ast_printer.h"
+
+namespace CVC4 {
+
+Printer* Printer::d_printers[language::output::LANG_MAX];
+
+Printer* Printer::makePrinter(OutputLanguage lang) {
+  using namespace CVC4::language::output;
+
+  switch(lang) {
+  case LANG_SMTLIB:
+    //return new printer::smt::SmtPrinter;
+  case LANG_SMTLIB_V2:
+    return new printer::smt2::Smt2Printer;
+  case LANG_CVC4:
+    //return new printer::cvc::CvcPrinter;
+  case LANG_AST:
+    return new printer::ast::AstPrinter;
+  default:
+    Unhandled(lang);
+  }
+}/* Printer::makePrinter() */
+
+}/* CVC4 namespace */
+
diff --git a/src/printer/printer.h b/src/printer/printer.h
new file mode 100644
index 000000000..2532725ae
--- /dev/null
+++ b/src/printer/printer.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file printer.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Base of the pretty-printer interface
+ **
+ ** Base of the pretty-printer interface.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__PRINTER_H
+#define __CVC4__PRINTER__PRINTER_H
+
+#include "util/language.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+class Printer {
+  /** Printers for each OutputLanguage */
+  static Printer* d_printers[language::output::LANG_MAX];
+
+  /** Make a Printer for a given OutputLanguage */
+  static Printer* makePrinter(OutputLanguage lang);
+
+public:
+  /** Get the Printer for a given OutputLanguage */
+  static Printer* getPrinter(OutputLanguage lang) {
+    if(d_printers[lang] == NULL) {
+      d_printers[lang] = makePrinter(lang);
+    }
+    return d_printers[lang];
+  }
+
+  /** Write a Node out to a stream with this Printer. */
+  virtual std::ostream& toStream(std::ostream& out, TNode n,
+                                 int toDepth, bool types) const = 0;
+};/* class Printer */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__PRINTER_H */
+
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
new file mode 100644
index 000000000..6040c133b
--- /dev/null
+++ b/src/printer/smt/smt_printer.cpp
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file smt_printer.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the SMT output language
+ **
+ ** The pretty-printer interface for the SMT output language.
+ **/
+
+#include "printer/smt/smt_printer.h"
+
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+namespace printer {
+namespace smt {
+
+std::ostream& SmtPrinter::toStream(std::ostream& out, TNode n,
+                                   int toDepth, bool types) const {
+  return out;
+}/* SmtPrinter::toStream() */
+
+}/* CVC4::printer::smt namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
new file mode 100644
index 000000000..e503ca8f0
--- /dev/null
+++ b/src/printer/smt/smt_printer.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file smt_printer.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the SMT output language
+ **
+ ** The pretty-printer interface for the SMT output language.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__SMT_PRINTER_H
+#define __CVC4__PRINTER__SMT_PRINTER_H
+
+#include <iostream>
+
+#include "printer/printer.h"
+
+namespace CVC4 {
+namespace printer {
+namespace smt {
+
+class SmtPrinter : public CVC4::Printer {
+public:
+  std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+};/* class SmtPrinter */
+
+}/* CVC4::printer::smt namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__SMT_PRINTER_H */
+
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
new file mode 100644
index 000000000..c8c4bfc20
--- /dev/null
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -0,0 +1,234 @@
+/*********************                                                        */
+/*! \file smt2_printer.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the SMT2 output language
+ **
+ ** The pretty-printer interface for the SMT2 output language.
+ **/
+
+#include "printer/smt2/smt2_printer.h"
+
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+namespace printer {
+namespace smt2 {
+
+void printBvParameterizedOp(std::ostream& out, TNode n);
+
+std::ostream& Smt2Printer::toStream(std::ostream& out, TNode n,
+                                    int toDepth, bool types) const {
+  // null
+  if(n.getKind() == kind::NULL_EXPR) {
+    out << "null";
+    return out;
+  }
+
+  // variable
+  if(n.getMetaKind() == kind::metakind::VARIABLE) {
+    string s;
+    if(n.getAttribute(expr::VarNameAttr(), s)) {
+      out << s;
+    } else {
+      if(n.getKind() == kind::VARIABLE) {
+        out << "var_";
+      } else {
+        out << n.getKind() << '_';
+      }
+      out << n.getId();
+    }
+    if(types) {
+      // print the whole type, but not *its* type
+      out << ":";
+      n.getType().toStream(out, -1, false, language::output::LANG_SMTLIB_V2);
+    }
+
+    return out;
+  }
+
+  // constant
+  if(n.getMetaKind() == kind::metakind::CONSTANT) {
+    switch(n.getKind()) {
+    case kind::BITVECTOR_TYPE:
+      out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")";
+      break;
+    case kind::CONST_BITVECTOR: {
+      const BitVector& bv = n.getConst<BitVector>();
+      const Integer& x = bv.getValue();
+      out << "#b";
+      unsigned n = bv.getSize();
+      while(n-- > 0) {
+        out << (x.testBit(n) ? '1' : '0');
+      }
+      break;
+    }
+    default:
+      // fall back on whatever operator<< does on underlying type; we
+      // might luck out and be SMT-LIB v2 compliant
+      kind::metakind::NodeValueConstPrinter::toStream(out, n);
+    }
+
+    return out;
+  }
+
+  bool stillNeedToPrintParams = true;
+  // operator
+  out << '(';
+  switch(n.getKind()) {
+    // builtin theory
+  case kind::EQUAL: out << "= "; break;
+  case kind::DISTINCT: out << "distinct "; break;
+  case kind::TUPLE: break;
+
+    // bool theory
+  case kind::NOT: out << "not "; break;
+  case kind::AND: out << "and "; break;
+  case kind::IFF: out << "iff "; break;
+  case kind::IMPLIES: out << "implies "; break;
+  case kind::OR: out << "or "; break;
+  case kind::XOR: out << "xor "; break;
+  case kind::ITE: out << "ite "; break;
+
+    // uf theory
+  case kind::APPLY_UF: break;
+  case kind::SORT_TYPE: break;
+
+    // arith theory
+  case kind::PLUS: out << "+ "; break;
+  case kind::MULT: out << "* "; break;
+  case kind::MINUS: out << "- "; break;
+  case kind::UMINUS: out << "- "; break;
+  case kind::DIVISION: out << "/ "; break;
+  case kind::LT: out << "< "; break;
+  case kind::LEQ: out << "<= "; break;
+  case kind::GT: out << "> "; break;
+  case kind::GEQ: out << ">= "; break;
+
+    // arrays theory
+  case kind::SELECT: out << "select "; break;
+  case kind::STORE: out << "store "; break;
+
+    // bv theory
+  case kind::BITVECTOR_CONCAT: out << "concat "; break;
+  case kind::BITVECTOR_AND: out << "bvand "; break;
+  case kind::BITVECTOR_OR: out << "bvor "; break;
+  case kind::BITVECTOR_XOR: out << "bvxor "; break;
+  case kind::BITVECTOR_NOT: out << "bvnot "; break;
+  case kind::BITVECTOR_NAND: out << "bvnand "; break;
+  case kind::BITVECTOR_NOR: out << "bvnor "; break;
+  case kind::BITVECTOR_XNOR: out << "bvxnor "; break;
+  case kind::BITVECTOR_COMP: out << "bvcomp "; break;
+  case kind::BITVECTOR_MULT: out << "bvmul "; break;
+  case kind::BITVECTOR_PLUS: out << "bvadd "; break;
+  case kind::BITVECTOR_SUB: out << "bvsub "; break;
+  case kind::BITVECTOR_NEG: out << "bvneg "; break;
+  case kind::BITVECTOR_UDIV: out << "bvudiv "; break;
+  case kind::BITVECTOR_UREM: out << "bvurem "; break;
+  case kind::BITVECTOR_SDIV: out << "bvsdiv "; break;
+  case kind::BITVECTOR_SREM: out << "bvsrem "; break;
+  case kind::BITVECTOR_SMOD: out << "bvsmod "; break;
+  case kind::BITVECTOR_SHL: out << "bvshl "; break;
+  case kind::BITVECTOR_LSHR: out << "bvlshr "; break;
+  case kind::BITVECTOR_ASHR: out << "bvashr "; break;
+  case kind::BITVECTOR_ULT: out << "bvult "; break;
+  case kind::BITVECTOR_ULE: out << "bvule "; break;
+  case kind::BITVECTOR_UGT: out << "bvugt "; break;
+  case kind::BITVECTOR_UGE: out << "bvuge "; break;
+  case kind::BITVECTOR_SLT: out << "bvslt "; break;
+  case kind::BITVECTOR_SLE: out << "bvsle "; break;
+  case kind::BITVECTOR_SGT: out << "bvsgt "; break;
+  case kind::BITVECTOR_SGE: out << "bvsge "; break;
+
+  case kind::BITVECTOR_EXTRACT:
+  case kind::BITVECTOR_REPEAT:
+  case kind::BITVECTOR_ZERO_EXTEND:
+  case kind::BITVECTOR_SIGN_EXTEND:
+  case kind::BITVECTOR_ROTATE_LEFT:
+  case kind::BITVECTOR_ROTATE_RIGHT:
+    printBvParameterizedOp(out, n);
+    out << ' ';
+    stillNeedToPrintParams = false;
+    break;
+
+  default:
+    // fall back on however the kind prints itself; this probably
+    // won't be SMT-LIB v2 compliant, but it will be clear from the
+    // output that support for the kind needs to be added here.
+    out << n.getKind() << ' ';
+  }
+  if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
+     stillNeedToPrintParams) {
+    if(toDepth != 0) {
+      n.getOperator().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+                               types, language::output::LANG_SMTLIB_V2);
+    } else {
+      out << "(...)";
+    }
+  }
+  for(TNode::iterator i = n.begin(),
+        iend = n.end();
+      i != iend; ) {
+    if(toDepth != 0) {
+      (*i).toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+                    types, language::output::LANG_SMTLIB_V2);
+    } else {
+      out << "(...)";
+    }
+    if(++i != iend) {
+      out << ' ';
+    }
+  }
+  out << ')';
+
+  return out;
+}/* Smt2Printer::toStream() */
+
+void printBvParameterizedOp(std::ostream& out, TNode n) {
+  out << "(_ ";
+  switch(n.getKind()) {
+  case kind::BITVECTOR_EXTRACT: {
+    BitVectorExtract p = n.getOperator().getConst<BitVectorExtract>();
+    out << "extract " << p.high << " " << p.low;
+    break;
+  }
+  case kind::BITVECTOR_REPEAT:
+    out << "repeat "
+        << n.getOperator().getConst<BitVectorRepeat>().repeatAmount;
+    break;
+  case kind::BITVECTOR_ZERO_EXTEND:
+    out << "zero_extend "
+        << n.getOperator().getConst<BitVectorZeroExtend>().zeroExtendAmount;
+    break;
+  case kind::BITVECTOR_SIGN_EXTEND:
+    out << "sign_extend "
+        << n.getOperator().getConst<BitVectorSignExtend>().signExtendAmount;
+    break;
+  case kind::BITVECTOR_ROTATE_LEFT:
+    out << "rotate_left "
+        << n.getOperator().getConst<BitVectorRotateLeft>().rotateLeftAmount;
+    break;
+  case kind::BITVECTOR_ROTATE_RIGHT:
+    out << "rotate_right "
+        << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
+    break;
+  default:
+    Unhandled(n.getKind());
+  }
+  out << ")";
+}
+
+}/* CVC4::printer::smt2 namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
new file mode 100644
index 000000000..7cd88f0ff
--- /dev/null
+++ b/src/printer/smt2/smt2_printer.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file smt2_printer.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the SMT2 output language
+ **
+ ** The pretty-printer interface for the SMT2 output language.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__SMT2_PRINTER_H
+#define __CVC4__PRINTER__SMT2_PRINTER_H
+
+#include <iostream>
+
+#include "printer/printer.h"
+
+namespace CVC4 {
+namespace printer {
+namespace smt2 {
+
+class Smt2Printer : public CVC4::Printer {
+public:
+  std::ostream& toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
+};/* class Smt2Printer */
+
+}/* CVC4::printer::smt2 namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__SMT2_PRINTER_H */
+