diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-04 17:52:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-04 17:52:11 -0500 |
commit | 3f150596fe2186aea1c40b3210e8a0d59dc1ba94 (patch) | |
tree | d0e3fbe5e3e55ef59783b8b4eb3e15e1f7020a4c /src/theory/inference_manager_buffered.cpp | |
parent | 721ce847f4d44fb7ee2509df3b34aad49fc7f484 (diff) |
Add asLemma flag to theory inference process (#5030)
This is required for strings, which uses the same data structure, InferInfo, for both lemmas and facts. This ensures the process method of theory inference knows where we are a pending lemma or a pending fact.
It also makes a few changes necessary for the proof-new branch, including disabling the proof node manager in the inference manager for datatypes.
Diffstat (limited to 'src/theory/inference_manager_buffered.cpp')
-rw-r--r-- | src/theory/inference_manager_buffered.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 3ba41a431..b0d092d74 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -86,7 +86,7 @@ void InferenceManagerBuffered::doPendingFacts() { // process this fact, which notice may enqueue more pending facts in this // loop. - d_pendingFact[i]->process(this); + d_pendingFact[i]->process(this, false); i++; } d_pendingFact.clear(); @@ -97,7 +97,7 @@ void InferenceManagerBuffered::doPendingLemmas() for (const std::unique_ptr<TheoryInference>& plem : d_pendingLem) { // process this lemma - plem->process(this); + plem->process(this, true); } d_pendingLem.clear(); } |