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!

diff --git a/config/doxygen.cfg b/config/doxygen.cfg
index f891b0b714c95291d7215953b5e75bbf66732945..f0598e0c43162f9b3620e4e9179dd75c8a46f845 100644 (file)
--- 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 bd4864fed62e1091e5b5bf3fa66086b0696592d7..03840e670f75595dc35652467f3cc992fd4a0ddb 100644 (file)
--- 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 1256ec64f92e0d327f16f5e970d355602d84cd83..1722bae3091e577f935a3dbc1d72a27d59ad0a7e 100644 (file)
--- 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 7e0bf6b65e9e5dcc4ba90030d66c972ce0de24eb..b2e6e401bf430da0c7727b8dfd306da471d1c160 100644 (file)
--- 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 7d7da35c570e278e3ef6a334820a4e98e6cd7966..b25bf503d4fc7ed383af7df5941d76da3fc03007 100644 (file)
--- 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 a362a597c1795532aa3724350bbf3f83625d0f39..1897bbd1c402085ea1b0b5bd543ed5a5e5bdcc60 100644 (file)
--- 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();
+  }
 };