diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-03 16:27:56 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-03 16:27:56 +0200 |
| commit | 58733b382a4a956c051d06e7318afa1deed612da (patch) | |
| tree | e41944879de5e7f1a06b1994731c9957d65acd3d /src/theory/arith/inference_manager.h | |
| parent | 337f8b791943e9b6b9a234f4f5422cf173342dd9 (diff) | |
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.
Diffstat (limited to 'src/theory/arith/inference_manager.h')
| -rw-r--r-- | src/theory/arith/inference_manager.h | 6 |
1 files changed, 3 insertions, 3 deletions
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; |