Add ArithLemma and arith::InferenceManager (#4960)

This PR adds a new ArithLemma that is essentiall NlLemma, but derived from the new theory::Lemma and meant to be used all across the arithmetic theory.
Also, based on theory::InferenceManagerBuffered this PR adds arith::InferenceManager that shall become the sole interface between the arithmetic theory and the OutputChannel.

1 files changed, 6 insertions, 1 deletions

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index e6e7822c5..762b7d4e0 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -35,7 +35,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   InferenceManagerBuffered(Theory& t,
                            TheoryState& state,
                            ProofNodeManager* pnm);
-  ~InferenceManagerBuffered() {}
+  virtual ~InferenceManagerBuffered() {}
   /**
    * Have we processed an inference during this call to check? In particular,
    * this returns true if we have a pending fact or lemma, or have encountered
@@ -124,6 +124,11 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   /** Clear pending phase requirements, without processing */
   void clearPendingPhaseRequirements();
 
+  /** Returns the number of pending lemmas. */
+  std::size_t numPendingLemmas() const;
+  /** Returns the number of pending facts. */
+  std::size_t numPendingFacts() const;
+
  protected:
   /** A set of pending inferences to be processed as lemmas */
   std::vector<std::shared_ptr<TheoryInference>> d_pendingLem;