From 3f150596fe2186aea1c40b3210e8a0d59dc1ba94 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 4 Sep 2020 17:52:11 -0500 Subject: 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. --- src/theory/inference_manager_buffered.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/theory/inference_manager_buffered.cpp') 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& plem : d_pendingLem) { // process this lemma - plem->process(this); + plem->process(this, true); } d_pendingLem.clear(); } -- cgit v1.2.3