diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-04 18:59:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-04 18:59:33 +0000 |
commit | 97f2f155ad238f48b35050088c3cf60cc326b1f3 (patch) | |
tree | ec531843fb8a5ff2fd354ebaf87dfaa87db70c8b /src | |
parent | a2cc0337aa53cfb686e26d68f98f2ae176ff1337 (diff) |
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!
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/node.h | 32 | ||||
-rw-r--r-- | src/expr/node_value.h | 2 | ||||
-rw-r--r-- | src/main/main.h | 1 | ||||
-rw-r--r-- | src/theory/output_channel.h | 12 |
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 |