Add documentation to Node and TNode (closes bug #201).

Also, only build doxygen documentation on stuff in src/,
not test/ or contrib/ or anywhere else.  Hopefully this
turns our 3000+ page user manual into something a little
more useful!

4 files changed, 46 insertions, 1 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;
 
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 1256ec64f..1722bae30 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -72,7 +72,7 @@ namespace expr {
 #endif /* sum != 64 */
 
 /**
- * This is an NodeValue.
+ * This is a NodeValue.
  */
 class NodeValue {
 
diff --git a/src/main/main.h b/src/main/main.h
index 7e0bf6b65..b2e6e401b 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -47,6 +47,7 @@ extern CVC4::StatisticsRegistry* pStatistics;
  */
 extern bool segvNoSpin;
 
+/** The options currently in play */
 extern Options options;
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 7d7da35c5..b25bf503d 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -99,6 +99,18 @@ public:
     throw(Interrupted, AssertionException) = 0;
 
   /**
+   * Request a split on a new theory atom.  This is equivalent to
+   * calling lemma({OR n (NOT n)}).
+   *
+   * @param n - a theory atom; must be of Boolean type
+   * @param safe - whether it is safe to be interrupted
+   */
+  void split(TNode n, bool safe = false)
+    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) {
+    lemma(n.orNode(n.notNode()));
+  }
+
+  /**
    * Provide an explanation in response to an explanation request.
    *
    * @param n - an explanation