diff options
Diffstat (limited to 'src/theory/theory_inference_manager.h')
| -rw-r--r-- | src/theory/theory_inference_manager.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 914c87d19..e52afe124 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -105,6 +105,11 @@ class TheoryInferenceManager * been provided in a custom way. */ void trustedConflict(TrustNode tconf); + /** Send lemma lem with property p on the output channel. */ + LemmaStatus lemma(TNode lem, LemmaProperty p = LemmaProperty::NONE); + /** Send (trusted) lemma lem with property p on the output channel. */ + LemmaStatus trustedLemma(const TrustNode& tlem, + LemmaProperty p = LemmaProperty::NONE); /** * Assert internal fact. This is recommended method for asserting "internal" * facts into the equality engine of the theory. In particular, this method |