diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-27 21:24:16 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-27 21:24:16 -0500 |
| commit | a0a969d7d65a778f2230ee920339541fdf380234 (patch) | |
| tree | 2e8a3436a36a487f97b3bc75e473a68259fb145b /src/theory/theory_inference_manager.h | |
| parent | 31f2135ad14b12e2ee9a24f5ca0da06cf5ed7b92 (diff) | |
Add the buffered inference manager (#4954)
This class implements a highly common pattern of buffering facts and lemmas to send on the output channel. It is planned that the inference managers of strings, sets, datatypes, (non-linear) arithmetic, sep, quantifiers will inherit from this class.
This PR adds basic calls to add lemmas on the output channel from InferenceManager.
It introduces a Lemma virtual class which arith::nl::NlLemma and strings::InferInfo will inherit from.
This is required to begin refactoring a flexible configurable strategy for non-linear arithmetic, and will make it easier to further develop towards a configurable approach for theory combination.
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 |