summaryrefslogtreecommitdiff
path: root/src/theory/output_channel.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/output_channel.h')
-rw-r--r--src/theory/output_channel.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 34a5a7dbd..60d0e1d48 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -116,11 +116,12 @@ public:
* @param n - a theory lemma valid at decision level 0
* @param removable - whether the lemma can be removed at any point
* @param preprocess - whether to apply more aggressive preprocessing
+ * @param sendAtoms - whether to ensure atoms are sent to the theory
* @return the "status" of the lemma, including user level at which
* the lemma resides; the lemma will be removed when this user level pops
*/
virtual LemmaStatus lemma(TNode n, bool removable = false,
- bool preprocess = false)
+ bool preprocess = false, bool sendAtoms = false)
throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException, LogicException) = 0;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback