From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 8 Dec 2021 23:48:30 +0000 (-0600)
Subject: Return bool for lemmaTheoryInference (#7773)
X-Git-Tag: cvc5-1.0.0~697
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=87574c003d1ff3ab2261ac4ae77e8026dbd39403;p=cvc5.git

Return bool for lemmaTheoryInference (#7773)
---

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 8b4880feb..963e0b95c 100644
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -161,14 +161,14 @@ std::size_t InferenceManagerBuffered::numPendingFacts() const
   return d_pendingFact.size();
 }
 
-void InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
+bool InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
 {
   // process this lemma
   LemmaProperty p = LemmaProperty::NONE;
   TrustNode tlem = lem->processLemma(p);
   Assert(!tlem.isNull());
   // send the lemma
-  trustedLemma(tlem, lem->getId(), p);
+  return trustedLemma(tlem, lem->getId(), p);
 }
 
 void InferenceManagerBuffered::assertInternalFactTheoryInference(
diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index e93152f72..579b1ae87 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -149,9 +149,10 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   /**
    * 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.
+   * on the provided theory inference, and returns true if the lemma was
+   * successfully sent.
    */
-  void lemmaTheoryInference(TheoryInference* lem);
+  bool lemmaTheoryInference(TheoryInference* lem);
   /**
    * Add the given theory inference as an internal fact. This calls
    * TheoryInferenceManager::assertInternalFact based on the provided theory