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.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index bb0bb494e..d03d2ba37 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -65,7 +65,7 @@ void InferenceManager::addPendingArithLemma(const ArithLemma& lemma,
                        isWaiting);
 }
 void InferenceManager::addPendingArithLemma(const Node& lemma,
-                                            nl::Inference inftype,
+                                            InferenceId inftype,
                                             bool isWaiting)
 {
   addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(
@@ -82,7 +82,7 @@ void InferenceManager::flushWaitingLemmas()
   d_waitingLem.clear();
 }
 
-void InferenceManager::addConflict(const Node& conf, nl::Inference inftype)
+void InferenceManager::addConflict(const Node& conf, InferenceId inftype)
 {
   conflict(Rewriter::rewrite(conf));
 }