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.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 54f33f6e7..b2da91e16 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -111,6 +111,17 @@ TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
                   << " mkTrustedConflictEqConstantMerge";
 }
 
+LemmaStatus TheoryInferenceManager::lemma(TNode lem, LemmaProperty p)
+{
+  return d_out.lemma(lem, p);
+}
+
+LemmaStatus TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
+                                                 LemmaProperty p)
+{
+  return d_out.trustedLemma(tlem, p);
+}
+
 void TheoryInferenceManager::assertInternalFact(TNode atom,
                                                 bool pol,
                                                 TNode fact)