From 97f2f155ad238f48b35050088c3cf60cc326b1f3 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 4 Apr 2011 18:59:33 +0000
Subject: [PATCH] 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!

---
 config/doxygen.cfg              |  2 +-
 src/expr/node.h                 | 32 ++++++++++++++++++++++++++++++++
 src/expr/node_value.h           |  2 +-
 src/main/main.h                 |  1 +
 src/theory/output_channel.h     | 12 ++++++++++++
 test/unit/theory/theory_black.h | 11 +++++++++++
 6 files changed, 58 insertions(+), 2 deletions(-)

diff --git a/config/doxygen.cfg b/config/doxygen.cfg
index f891b0b71..f0598e0c4 100644
--- a/config/doxygen.cfg
+++ b/config/doxygen.cfg
@@ -568,7 +568,7 @@ WARN_LOGFILE           =
 # directories like "/usr/src/myproject". Separate the files or directories
 # with spaces.
 
-INPUT                  = $(SRCDIR)
+INPUT                  = $(SRCDIR)/src
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is
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
@@ -98,6 +98,18 @@ public:
   virtual void lemma(TNode n, bool safe = false)
     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.
    *
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index a362a597c..1897bbd1c 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -289,4 +289,15 @@ public:
 
     TS_ASSERT_EQUALS(&oc, &theOtherChannel);
   }
+
+  void testOutputChannel() {
+    Node n = atom0.orNode(atom1);
+    d_outputChannel.lemma(n);
+    d_outputChannel.split(atom0);
+    Node s = atom0.orNode(atom0.notNode());
+    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);
+    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[0], make_pair(LEMMA, n));
+    TS_ASSERT_EQUALS(d_outputChannel.d_callHistory[1], make_pair(LEMMA, s));
+    d_outputChannel.d_callHistory.clear();
+  }
 };
-- 
2.30.2