diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-08 17:48:30 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-08 23:48:30 +0000 |
| commit | 87574c003d1ff3ab2261ac4ae77e8026dbd39403 (patch) | |
| tree | 44fd513d6f7c1e711ffb0e39641a8d0c720f56cb | |
| parent | 0e3ece61a4dbec520bcf1ef4087b3b5eb79d5771 (diff) | |
Return bool for lemmaTheoryInference (#7773)
| -rw-r--r-- | src/theory/inference_manager_buffered.cpp | 4 | ||||
| -rw-r--r-- | 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 |