1 files changed, 32 insertions, 0 deletions
diff --git a/src/expr/node.h b/src/expr/node.h
index bd4864fed..03840e670 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -85,12 +85,44 @@ public:
 };
 
 /**
+ * \typedef NodeTemplate<true> Node;
+ *
  * The Node class encapsulates the NodeValue with reference counting.
+ *
+ * One should use generally use Nodes to manipulate expressions, to be safe.
+ * Every outstanding Node that references a NodeValue is counted in that
+ * NodeValue's reference count.  Reference counts are maintained correctly
+ * on assignment of the Node object (to point to another NodeValue), and,
+ * upon destruction of the Node object, the NodeValue's reference count is
+ * decremented and, if zero, it becomes eligible for reclamation by the
+ * system.
  */
 typedef NodeTemplate<true> Node;
 
 /**
+ * \typedef NodeTemplate<false> TNode;
+ *
  * The TNode class encapsulates the NodeValue but doesn't count references.
+ *
+ * TNodes are just like Nodes, but they don't update the reference count.
+ * Therefore, there is less overhead (copying a TNode is just the cost of
+ * the underlying pointer copy).  Generally speaking, this is unsafe!
+ * However, there are certain situations where a TNode can be used safely.
+ *
+ * The largest class of uses for TNodes are when you need to use them in a
+ * "temporary," scoped fashion (hence the "T" in "TNode").  In general,
+ * it is safe to use TNode as a function parameter type, since the calling
+ * function (or some other function on the call stack) presumably has a Node
+ * reference to the expression data.  It is generally _not_ safe, however,
+ * to return a TNode _from_ a function.  (Functions that return Nodes often
+ * create the expression they return; such new expressions may not be
+ * referenced on the call stack, and have a reference count of 1 on
+ * creation.  If this is returned as a TNode rather than a Node, the
+ * count drops to zero, marking the expression as eligible for reclamation.)
+ *
+ * More guidelines on when to use TNodes is available in the CVC4
+ * Developer's Guide:
+ * http://goedel.cims.nyu.edu/wiki/Developer%27s_Guide#Dealing_with_expressions_.28Nodes_and_TNodes.29
  */
 typedef NodeTemplate<false> TNode;