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, 10 insertions, 5 deletions

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