From d107bf9b8b4dd206580681e601a033742029ec79 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Feb 2021 11:00:41 -0600 Subject: [PATCH] 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. --- src/theory/datatypes/inference.cpp | 4 ++-- src/theory/datatypes/inference_manager.cpp | 5 ++++- 2 files changed, 6 insertions(+), 3 deletions(-) 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)); } -- 2.30.2