From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 17 Feb 2021 17:00:41 +0000 (-0600)
Subject: Compute fact or lemma in datatypes prior to buffering (#5914)
X-Git-Tag: cvc5-1.0.0~2270
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d107bf9b8b4dd206580681e601a033742029ec79;p=cvc5.git

Compute fact or lemma in datatypes prior to buffering (#5914)

This is necessary for the planned refactoring of TheoryInference::process. This forces datatypes to decide lemma vs. fact prior to buffering inferences.
---

diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp
index 5d68159f7..d03bb0f2f 100644
--- a/src/theory/datatypes/inference.cpp
+++ b/src/theory/datatypes/inference.cpp
@@ -65,8 +65,8 @@ bool DatatypesInference::process(TheoryInferenceManager* im, bool asLemma)
 {
   // Check to see if we have to communicate it to the rest of the system.
   // The flag asLemma is true when the inference was marked that it must be
-  // sent as a lemma in addPendingInference below.
-  if (asLemma || mustCommunicateFact(d_conc, d_exp))
+  // sent as a lemma.
+  if (asLemma)
   {
     return d_im->processDtLemma(d_conc, d_exp, getId());
   }
diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index affa401d4..496881a33 100644
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -58,7 +58,10 @@ void InferenceManager::addPendingInference(Node conc,
                                            bool forceLemma,
                                            InferenceId i)
 {
-  if (forceLemma)
+  // if we are forcing the inference to be processed as a lemma, or if the
+  // inference must be sent as a lemma based on the policy in
+  // mustCommunicateFact.
+  if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp))
   {
     d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, i));
   }