diff options
-rw-r--r-- | config/doxygen.cfg | 2 | ||||
-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 | ||||
-rw-r--r-- | 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 @@ -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 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(); + } }; |