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

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