1 files changed, 15 insertions, 1 deletions
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index d12bd40b3..985bad3bc 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -35,7 +35,8 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   InferenceManagerBuffered(Theory& t,
                            TheoryState& state,
                            ProofNodeManager* pnm,
-                           const std::string& name);
+                           const std::string& name,
+                           bool cacheLemmas = true);
   virtual ~InferenceManagerBuffered() {}
   /**
    * Do we have a pending fact or lemma?
@@ -145,6 +146,19 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   /** Returns the number of pending facts. */
   std::size_t numPendingFacts() const;
 
+  /**
+   * Send the given theory inference as a lemma on the output channel of this
+   * inference manager. This calls TheoryInferenceManager::trustedLemma based
+   * on the provided theory inference.
+   */
+  void lemmaTheoryInference(TheoryInference* lem);
+  /**
+   * Add the given theory inference as an internal fact. This calls
+   * TheoryInferenceManager::assertInternalFact based on the provided theory
+   * inference.
+   */
+  void assertInternalFactTheoryInference(TheoryInference* fact);
+
  protected:
   /** A set of pending inferences to be processed as lemmas */
   std::vector<std::unique_ptr<TheoryInference>> d_pendingLem;