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.h11
1 files changed, 0 insertions, 11 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 1c48c0160..269f28732 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -100,17 +100,6 @@ public:
throw(Interrupted, AssertionException) = 0;
/**
- * Tell the core to add the following valid lemma as if it were a
- * user assertion. This should NOT be called during solving, only
- * preprocessing.
- *
- * @param n - a theory lemma valid to be asserted
- * @param safe - whether it is safe to be interrupted
- */
- virtual void augmentingLemma(TNode n, bool safe = false)
- throw(Interrupted, AssertionException) = 0;
-
- /**
* 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