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 5d68159f7651d1f8e3160eeb89cdd5c34a497afb..d03bb0f2f7d938fc033494b66c33b9d5ec74f762 100644 (file)
--- 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 affa401d4497db93d624baf529179b97c4e108b7..496881a33a0fe186839ffac845cf41a6cfaeb766 100644 (file)
--- 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));
   }