* ability to output NodeBuilders without first converting them to Nodes---useful for debugging.

* language-dependent Node::toString()
* some minor proof-related cleanup

4 files changed, 51 insertions, 4 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 0f4b55d4a..2751c96a8 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -211,7 +211,7 @@ class NodeTemplate {
 
   /**
    * 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 
+   * are made on the expression, and should only be used if we know what we
    * are doing.
    *
    * @param ev the expression value to assign
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 2cb2527b2..1914bb736 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -157,6 +157,7 @@
 #ifndef __CVC4__NODE_BUILDER_H
 #define __CVC4__NODE_BUILDER_H
 
+#include <iostream>
 #include <vector>
 #include <cstdlib>
 #include <stdint.h>
@@ -184,6 +185,11 @@ class OrNodeBuilder;
 class PlusNodeBuilder;
 class MultNodeBuilder;
 
+// Sometimes it's useful for debugging to output a NodeBuilder that
+// isn't yet a Node..
+template <unsigned nchild_thresh>
+std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb);
+
 /**
  * The main template NodeBuilder.
  */
@@ -720,6 +726,10 @@ public:
   // private fields
   template <unsigned N>
   friend class NodeBuilder;
+
+  template <unsigned N>
+  friend std::ostream& operator<<(std::ostream& out, const NodeBuilder<N>& nb);
+
 };/* class NodeBuilder<> */
 
 }/* CVC4 namespace */
@@ -1151,7 +1161,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
      ** allocated "inline" in this NodeBuilder. **/
 
     // Lookup the expression value in the pool we already have
-    expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
+    expr::NodeValue* poolNv = d_nm->poolLookup(const_cast<expr::NodeValue*>(&d_inlineNv));
     // If something else is there, we reuse it
     if(poolNv != NULL) {
       /* Subcase (a): The Node under construction already exists in
@@ -1301,6 +1311,11 @@ inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const
 }
 #endif /* CVC4_DEBUG */
 
+template <unsigned nchild_thresh>
+std::ostream& operator<<(std::ostream& out, const NodeBuilder<nchild_thresh>& nb) {
+  return out << *nb.d_nv;
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_BUILDER_H */
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 5fe48b01d..f1fade69d 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -39,16 +39,23 @@ NodeValue NodeValue::s_null(0);
 
 string NodeValue::toString() const {
   stringstream ss;
-  toStream(ss);
+  toStream(ss, -1, false, Options::current()->outputLanguage);
   return ss.str();
 }
 
 void NodeValue::toStream(std::ostream& out, int toDepth, bool types,
                          OutputLanguage language) const {
+  // Ensure that this node value is live for the length of this call.
+  // It really breaks things badly if we don't have a nonzero ref
+  // count, even just for printing.
+  RefCountGuard guard(this);
+
   Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types);
 }
 
 void NodeValue::printAst(std::ostream& out, int ind) const {
+  RefCountGuard guard(this);
+
   indent(out, ind);
   out << '(';
   out << getKind();
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 71aa37926..95af57719 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -297,6 +297,30 @@ public:
 
 private:
 
+  class RefCountGuard {
+    NodeValue* d_nv;
+  public:
+    RefCountGuard(const NodeValue* nv) :
+      d_nv(const_cast<NodeValue*>(nv)) {
+      // inc()
+      if(EXPECT_TRUE( d_nv->d_rc < MAX_RC )) {
+        ++d_nv->d_rc;
+      }
+    }
+    ~RefCountGuard() {
+      // dec() without marking for deletion: we don't want to garbage
+      // collect this NodeValue if ours is the last reference to it.
+      // E.g., this can happen when debugging code calls the print
+      // routines below.  As RefCountGuards are scoped on the stack,
+      // this should be fine---but not in multithreaded contexts!
+      if(EXPECT_TRUE( d_nv->d_rc < MAX_RC )) {
+        --d_nv->d_rc;
+      }
+    }
+  };/* NodeValue::RefCountGuard */
+
+  friend class RefCountGuard;
+
   /**
    * Indents the given stream a given amount of spaces.
    * @param out the stream to indent
@@ -464,7 +488,8 @@ inline T NodeValue::iterator<T>::operator*() const {
 inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
   nv.toStream(out,
               Node::setdepth::getDepth(out),
-              Node::printtypes::getPrintTypes(out));
+              Node::printtypes::getPrintTypes(out),
+              Node::setlanguage::getLanguage(out));
   return out;
 }