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/theory | |
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/theory')
-rw-r--r-- | src/theory/output_channel.h | 12 |
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 |