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

5 files changed, 32 insertions, 89 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index be089bca8..2e27b4f66 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -648,15 +648,23 @@ public:
   ExprSetLanguage(OutputLanguage l) : d_language(l) {}
 
   inline void applyLanguage(std::ostream& out) {
-    out.iword(s_iosIndex) = int(d_language);
+    // (offset by one to detect whether default has been set yet)
+    out.iword(s_iosIndex) = int(d_language) + 1;
   }
 
   static inline OutputLanguage getLanguage(std::ostream& out) {
-    return OutputLanguage(out.iword(s_iosIndex));
+    long& l = out.iword(s_iosIndex);
+    if(l == 0) {
+      // set the default language on this ostream
+      // (offset by one to detect whether default has been set yet)
+      l = s_defaultLanguage + 1;
+    }
+    return OutputLanguage(l - 1);
   }
 
   static inline void setLanguage(std::ostream& out, OutputLanguage l) {
-    out.iword(s_iosIndex) = int(l);
+    // (offset by one to detect whether default has been set yet)
+    out.iword(s_iosIndex) = int(l) + 1;
   }
 };/* class ExprSetLanguage */
 
@@ -664,7 +672,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 659 "${template}"
+#line 676 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index cb9730d34..c4604d40e 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -88,11 +88,6 @@ struct NodeValueCompare {
   inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
 };/* struct NodeValueCompare */
 
-struct NodeValueConstPrinter {
-  inline static void toStream(std::ostream& out,
-                              const ::CVC4::expr::NodeValue* nv);
-};
-
 /**
  * "metakinds" represent the "kinds" of kinds at the meta-level.
  * "metakind" is an ugly name but it's not used by client code, just
@@ -264,6 +259,12 @@ ${metakind_constHashes}
   }
 }
 
+struct NodeValueConstPrinter {
+  inline static void toStream(std::ostream& out,
+                              const ::CVC4::expr::NodeValue* nv);
+  inline static void toStream(std::ostream& out, TNode n);
+};
+
 inline void NodeValueConstPrinter::toStream(std::ostream& out,
                                             const ::CVC4::expr::NodeValue* nv) {
   Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
@@ -275,6 +276,10 @@ ${metakind_constPrinters}
   }
 }
 
+inline void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) {
+  toStream(out, n.d_nv);
+}
+
 /**
  * Cleanup to be performed when a NodeValue zombie is collected, and
  * it has CONSTANT metakind.  This calls the destructor for the underlying
diff --git a/src/expr/node.h b/src/expr/node.h
index c30e2e856..bd4864fed 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -105,6 +105,12 @@ class NodeValue;
   class ExprSetDepth;
 }/* CVC4::expr namespace */
 
+namespace kind {
+  namespace metakind {
+    struct NodeValueConstPrinter;
+  }/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+
 /**
  * Encapsulation of an NodeValue pointer.  The reference count is
  * maintained in the NodeValue if ref_count is true.
@@ -149,6 +155,8 @@ class NodeTemplate {
 
   friend class ::CVC4::expr::attr::AttributeManager;
 
+  friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
+
   /**
    * Assigns the expression value and does reference counting. No assumptions
    * are made on the expression, and should only be used if we know what we 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index ce0928209..cc8c780a8 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -178,9 +178,6 @@ namespace CVC4 {
 
 namespace CVC4 {
 
-template <unsigned nchild_thresh>
-inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&);
-
 /* see expr/convenience_node_builders.h */
 class AndNodeBuilder;
 class OrNodeBuilder;
@@ -692,13 +689,6 @@ public:
   operator Node();
   operator Node() const;
 
-  inline void toStream(std::ostream& out, int depth = -1, bool types = false,
-                       OutputLanguage language = language::output::LANG_AST) const {
-    Assert(!isUsed(), "NodeBuilder is one-shot only; "
-           "attempt to access it after conversion");
-    d_nv->toStream(out, depth, types, language);
-  }
-
   NodeBuilder<nchild_thresh>& operator&=(TNode);
   NodeBuilder<nchild_thresh>& operator|=(TNode);
   NodeBuilder<nchild_thresh>& operator+=(TNode);
@@ -1250,15 +1240,6 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) {
   }
 }
 
-template <unsigned nchild_thresh>
-inline std::ostream& operator<<(std::ostream& out,
-                                const NodeBuilder<nchild_thresh>& b) {
-  b.toStream(out,
-             Node::setdepth::getDepth(out),
-             Node::printtypes::getPrintTypes(out));
-  return out;
-}
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_BUILDER_H */
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index a5fff2095..666462875 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -25,6 +25,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "util/language.h"
+#include "printer/printer.h"
 #include <sstream>
 
 using namespace std;
@@ -44,67 +45,7 @@ string NodeValue::toString() const {
 
 void NodeValue::toStream(std::ostream& out, int toDepth, bool types,
                          OutputLanguage language) const {
-  using namespace CVC4;
-  using namespace CVC4::kind;
-  using namespace CVC4::language::output;
-
-  switch(language) {
-  case LANG_CVC4:
-    // FIXME support cvc output language
-  case LANG_SMTLIB:
-    // FIXME support smt-lib output language
-  case LANG_SMTLIB_V2:
-    // FIXME support smt-lib v2 output language
-  case LANG_AST:
-    if(getKind() == kind::NULL_EXPR) {
-      out << "null";
-    } else if(getMetaKind() == kind::metakind::VARIABLE) {
-      if(getKind() != kind::VARIABLE &&
-         getKind() != kind::SORT_TYPE) {
-        out << getKind() << ':';
-      }
-
-      string s;
-      NodeManager* nm = NodeManager::currentNM();
-
-      // conceptually "this" is const, and hasAttribute() doesn't change
-      // its argument, but it requires a non-const key arg (for now)
-      if(nm->getAttribute(const_cast<NodeValue*>(this),
-                          VarNameAttr(), s)) {
-        out << s;
-      } else {
-        out << "var_" << d_id;
-      }
-      if(types) {
-        // print the whole type, but not *its* type
-        out << ":";
-        nm->getType(TNode(this)).toStream(out, -1, false, language);
-      }
-    } else {
-      out << '(' << Kind(d_kind);
-      if(getMetaKind() == kind::metakind::CONSTANT) {
-        out << ' ';
-        kind::metakind::NodeValueConstPrinter::toStream(out, this);
-      } else {
-        for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
-          if(i != nv_end()) {
-            out << ' ';
-          }
-          if(toDepth != 0) {
-            (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-                           types, language);
-          } else {
-            out << "(...)";
-          }
-        }
-      }
-      out << ')';
-    }
-    break;
-
-  default:
-    out << "[output language " << language << " unsupported]";
-  }// end switch(language)
+  Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types);
 }
 
 void NodeValue::printAst(std::ostream& out, int ind) const {