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.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 44b89e8cb..51187b7dd 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -113,10 +113,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
* @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)
+ virtual LemmaStatus lemma(TNode n, bool removable = false,
+ bool preprocess = false)
throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback