From 58733b382a4a956c051d06e7318afa1deed612da Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 3 Sep 2020 16:27:56 +0200 Subject: Basic integration of arith::InferenceManager (#4999) This PR adds a first basic integration of the arith::InferenceManager into the arithmetic theory and the nonlinear extension in particular. While the lemma collection mechanism (in the nonlinear extension) remains unchanged, the lemmas are ultimately not directly pushed to the output channel but instead added to the inference manager. Additionally, we no longer use the cache within the nonlinear extension but instead rely on the inference manager. This PR is based on #4960. --- src/theory/arith/inference_manager.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/theory/arith/inference_manager.h') diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 1c0678e60..33e4f424b 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -22,7 +22,7 @@ #include "theory/arith/arith_lemma.h" #include "theory/arith/arith_state.h" -#include "theory/arith/nl/inference.h" +#include "theory/arith/inference_id.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/inference_manager_buffered.h" @@ -69,7 +69,7 @@ class InferenceManager : public InferenceManagerBuffered * added as pending lemma when calling flushWaitingLemmas. */ void addPendingArithLemma(const Node& lemma, - nl::Inference inftype, + InferenceId inftype, bool isWaiting = false); /** @@ -79,7 +79,7 @@ class InferenceManager : public InferenceManagerBuffered void flushWaitingLemmas(); /** Add a conflict to the this inference manager. */ - void addConflict(const Node& conf, nl::Inference inftype); + void addConflict(const Node& conf, InferenceId inftype); /** Returns the number of pending lemmas. */ std::size_t numWaitingLemmas() const; -- cgit v1.2.3