From 87574c003d1ff3ab2261ac4ae77e8026dbd39403 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Dec 2021 17:48:30 -0600 Subject: [PATCH] Return bool for lemmaTheoryInference (#7773) --- src/theory/inference_manager_buffered.cpp | 4 ++-- src/theory/inference_manager_buffered.h | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) 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 -- 2.30.2