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.)

1 files changed, 53 insertions, 0 deletions

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 */
+