summaryrefslogtreecommitdiff
path: root/src/theory/output_channel.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-04-04 18:59:33 +0000
committerMorgan Deters <mdeters@gmail.com>2011-04-04 18:59:33 +0000
commit97f2f155ad238f48b35050088c3cf60cc326b1f3 (patch)
treeec531843fb8a5ff2fd354ebaf87dfaa87db70c8b /src/theory/output_channel.h
parenta2cc0337aa53cfb686e26d68f98f2ae176ff1337 (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/theory/output_channel.h')
-rw-r--r--src/theory/output_channel.h12
1 files changed, 12 insertions, 0 deletions
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback