diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-17 11:00:41 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-17 11:00:41 -0600 |
commit | d107bf9b8b4dd206580681e601a033742029ec79 (patch) | |
tree | d430fc6b653eac528c209782b9877718580e7ca9 | |
parent | bdc1b222fbc674ab1f8a48fad9f78759c3baea23 (diff) |
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.
-rw-r--r-- | src/theory/datatypes/inference.cpp | 4 | ||||
-rw-r--r-- | 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)); } |