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, 8 insertions, 0 deletions

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