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.

17 files changed, 147 insertions, 155 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9523f9600..a0fd277f8 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -291,6 +291,8 @@ libcvc4_add_sources(
   theory/arith/fc_simplex.h
   theory/arith/infer_bounds.cpp
   theory/arith/infer_bounds.h
+  theory/arith/inference_id.cpp
+  theory/arith/inference_id.h
   theory/arith/inference_manager.cpp
   theory/arith/inference_manager.h
   theory/arith/linear_equality.cpp
@@ -313,8 +315,6 @@ libcvc4_add_sources(
   theory/arith/nl/ext_theory_callback.h
   theory/arith/nl/iand_solver.cpp
   theory/arith/nl/iand_solver.h
-  theory/arith/nl/inference.cpp
-  theory/arith/nl/inference.h
   theory/arith/nl/nl_constraint.cpp
   theory/arith/nl/nl_constraint.h
   theory/arith/nl/nl_lemma_utils.cpp
diff --git a/src/theory/arith/arith_lemma.h b/src/theory/arith/arith_lemma.h
index a06cb83f3..8af620286 100644
--- a/src/theory/arith/arith_lemma.h
+++ b/src/theory/arith/arith_lemma.h
@@ -19,7 +19,7 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/nl/inference.h"
+#include "theory/arith/inference_id.h"
 #include "theory/inference_manager_buffered.h"
 #include "theory/output_channel.h"
 #include "theory/theory_inference.h"
@@ -40,14 +40,14 @@ class ArithLemma : public SimpleTheoryLemma
   ArithLemma(Node n,
              LemmaProperty p,
              ProofGenerator* pg,
-             nl::Inference inf = nl::Inference::UNKNOWN)
+             InferenceId inf = InferenceId::UNKNOWN)
       : SimpleTheoryLemma(n, p, pg), d_inference(inf)
   {
   }
   virtual ~ArithLemma() {}
 
   /** The inference id for the lemma */
-  nl::Inference d_inference;
+  InferenceId d_inference;
 };
 /**
  * Writes an arithmetic lemma to a stream.
diff --git a/src/theory/arith/inference_id.cpp b/src/theory/arith/inference_id.cpp
new file mode 100644
index 000000000..7ecbb364d
--- /dev/null
+++ b/src/theory/arith/inference_id.cpp
@@ -0,0 +1,57 @@
+/*********************                                                        */
+/*! \file inference_id.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of inference enumeration.
+ **/
+
+#include "theory/arith/inference_id.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+const char* toString(InferenceId i)
+{
+  switch (i)
+  {
+    case InferenceId::NL_CONGRUENCE: return "CONGRUENCE";
+    case InferenceId::NL_SHARED_TERM_VALUE_SPLIT: return "SHARED_TERM_VALUE_SPLIT";
+    case InferenceId::NL_SPLIT_ZERO: return "SPLIT_ZERO";
+    case InferenceId::NL_SIGN: return "SIGN";
+    case InferenceId::NL_COMPARISON: return "COMPARISON";
+    case InferenceId::NL_INFER_BOUNDS: return "INFER_BOUNDS";
+    case InferenceId::NL_INFER_BOUNDS_NT: return "INFER_BOUNDS_NT";
+    case InferenceId::NL_FACTOR: return "FACTOR";
+    case InferenceId::NL_RES_INFER_BOUNDS: return "RES_INFER_BOUNDS";
+    case InferenceId::NL_TANGENT_PLANE: return "TANGENT_PLANE";
+    case InferenceId::NL_T_PURIFY_ARG: return "T_PURIFY_ARG";
+    case InferenceId::NL_T_INIT_REFINE: return "T_INIT_REFINE";
+    case InferenceId::NL_T_PI_BOUND: return "T_PI_BOUND";
+    case InferenceId::NL_T_MONOTONICITY: return "T_MONOTONICITY";
+    case InferenceId::NL_T_SECANT: return "T_SECANT";
+    case InferenceId::NL_T_TANGENT: return "T_TANGENT";
+    case InferenceId::NL_IAND_INIT_REFINE: return "IAND_INIT_REFINE";
+    case InferenceId::NL_IAND_VALUE_REFINE: return "IAND_VALUE_REFINE";
+    case InferenceId::NL_CAD_CONFLICT: return "CAD_CONFLICT";
+    case InferenceId::NL_CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL";
+    default: return "?";
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, InferenceId i)
+{
+  out << toString(i);
+  return out;
+}
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/nl/inference.h b/src/theory/arith/inference_id.h
index 0cf6ad3bd..56aeb3d24 100644
--- a/src/theory/arith/nl/inference.h
+++ b/src/theory/arith/inference_id.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file inference.h
+/*! \file inference_id.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds
@@ -9,13 +9,13 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Inference enumeration for non-linear arithmetic.
+ ** \brief Inference enumeration for arithmetic.
  **/
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__INFER_INFO_H
-#define CVC4__THEORY__ARITH__NL__INFER_INFO_H
+#ifndef CVC4__THEORY__ARITH__INFERENCE_ID_H
+#define CVC4__THEORY__ARITH__INFERENCE_ID_H
 
 #include <map>
 #include <vector>
@@ -25,58 +25,57 @@
 namespace CVC4 {
 namespace theory {
 namespace arith {
-namespace nl {
 
 /**
  * Types of inferences used in the procedure
  */
-enum class Inference : uint32_t
+enum class InferenceId : uint32_t
 {
   //-------------------- core
   // simple congruence x=y => f(x)=f(y)
-  CONGRUENCE,
+  NL_CONGRUENCE,
   // shared term value split (for naive theory combination)
-  SHARED_TERM_VALUE_SPLIT,
+  NL_SHARED_TERM_VALUE_SPLIT,
   //-------------------- incremental linearization solver
   // splitting on zero (NlSolver::checkSplitZero)
-  SPLIT_ZERO,
+  NL_SPLIT_ZERO,
   // based on sign (NlSolver::checkMonomialSign)
-  SIGN,
+  NL_SIGN,
   // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude)
-  COMPARISON,
+  NL_COMPARISON,
   // based on inferring bounds (NlSolver::checkMonomialInferBounds)
-  INFER_BOUNDS,
+  NL_INFER_BOUNDS,
   // same as above, for inferences that introduce new terms
-  INFER_BOUNDS_NT,
+  NL_INFER_BOUNDS_NT,
   // factoring (NlSolver::checkFactoring)
-  FACTOR,
+  NL_FACTOR,
   // resolution bound inferences (NlSolver::checkMonomialInferResBounds)
-  RES_INFER_BOUNDS,
+  NL_RES_INFER_BOUNDS,
   // tangent planes (NlSolver::checkTangentPlanes)
-  TANGENT_PLANE,
+  NL_TANGENT_PLANE,
   //-------------------- transcendental solver
   // purification of arguments to transcendental functions
-  T_PURIFY_ARG,
+  NL_T_PURIFY_ARG,
   // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine)
-  T_INIT_REFINE,
+  NL_T_INIT_REFINE,
   // pi bounds
-  T_PI_BOUND,
+  NL_T_PI_BOUND,
   // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic)
-  T_MONOTONICITY,
+  NL_T_MONOTONICITY,
   // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes)
-  T_TANGENT,
+  NL_T_TANGENT,
   // secant refinement, the dual of the above inference
-  T_SECANT,
+  NL_T_SECANT,
   //-------------------- iand solver
   // initial refinements (IAndSolver::checkInitialRefine)
-  IAND_INIT_REFINE,
+  NL_IAND_INIT_REFINE,
   // value refinements (IAndSolver::checkFullRefine)
-  IAND_VALUE_REFINE,
+  NL_IAND_VALUE_REFINE,
   //-------------------- cad solver
   // conflict / infeasible subset obtained from cad
-  CAD_CONFLICT,
+  NL_CAD_CONFLICT,
   // excludes an interval for a single variable
-  CAD_EXCLUDED_INTERVAL,
+  NL_CAD_EXCLUDED_INTERVAL,
   //-------------------- unknown
   UNKNOWN,
 };
@@ -90,7 +89,7 @@ enum class Inference : uint32_t
  * @param i The inference
  * @return The name of the inference
  */
-const char* toString(Inference i);
+const char* toString(InferenceId i);
 
 /**
  * Writes an inference name to a stream.
@@ -99,11 +98,10 @@ const char* toString(Inference i);
  * @param i The inference to write to the stream
  * @return The stream
  */
-std::ostream& operator<<(std::ostream& out, Inference i);
+std::ostream& operator<<(std::ostream& out, InferenceId i);
 
-}  // namespace nl
 }  // namespace arith
 }  // namespace theory
 }  // namespace CVC4
 
-#endif /* CVC4__THEORY__ARITH__NL__INFER_INFO_H */
+#endif /* CVC4__THEORY__ARITH__INFERENCE_H */
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));
 }
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;
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index ac939c341..473e067b7 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -18,7 +18,7 @@
 #include <poly/polyxx.h>
 #endif
 
-#include "inference.h"
+#include "theory/arith/inference_id.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/poly_conversion.h"
 #include "util/poly_util.h"
@@ -89,11 +89,11 @@ std::vector<NlLemma> CadSolver::checkFull()
     Assert(!mis.empty()) << "Infeasible subset can not be empty";
     if (mis.size() == 1)
     {
-      lems.emplace_back(mis.front(), Inference::CAD_CONFLICT);
+      lems.emplace_back(mis.front(), InferenceId::NL_CAD_CONFLICT);
     }
     else
     {
-      lems.emplace_back(nm->mkNode(Kind::OR, mis), Inference::CAD_CONFLICT);
+      lems.emplace_back(nm->mkNode(Kind::OR, mis), InferenceId::NL_CAD_CONFLICT);
     }
     Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_node << std::endl;
   }
@@ -138,7 +138,7 @@ std::vector<NlLemma> CadSolver::checkPartial()
       if (!conclusion.isNull()) {
         Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion);
         Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl;
-        lems.emplace_back(lemma, Inference::CAD_EXCLUDED_INTERVAL);
+        lems.emplace_back(lemma, InferenceId::NL_CAD_EXCLUDED_INTERVAL);
        }
     }
   }
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 3b6c3cbe4..08c85cafe 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -101,7 +101,7 @@ std::vector<NlLemma> IAndSolver::checkInitialRefine()
       Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj);
       Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE"
                           << std::endl;
-      lems.emplace_back(lem, Inference::IAND_INIT_REFINE);
+      lems.emplace_back(lem, InferenceId::NL_IAND_INIT_REFINE);
     }
   }
   return lems;
@@ -163,7 +163,7 @@ std::vector<NlLemma> IAndSolver::checkFullRefine()
         Node lem = valueBasedLemma(i);
         Trace("iand-lemma")
             << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl;
-        lems.emplace_back(lem, Inference::IAND_VALUE_REFINE);
+        lems.emplace_back(lem, InferenceId::NL_IAND_VALUE_REFINE);
       }
     }
   }
diff --git a/src/theory/arith/nl/inference.cpp b/src/theory/arith/nl/inference.cpp
deleted file mode 100644
index 0d8413777..000000000
--- a/src/theory/arith/nl/inference.cpp
+++ /dev/null
@@ -1,59 +0,0 @@
-/*********************                                                        */
-/*! \file inference.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Implementation of inference enumeration.
- **/
-
-#include "theory/arith/nl/inference.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-namespace nl {
-
-const char* toString(Inference i)
-{
-  switch (i)
-  {
-    case Inference::CONGRUENCE: return "CONGRUENCE";
-    case Inference::SHARED_TERM_VALUE_SPLIT: return "SHARED_TERM_VALUE_SPLIT";
-    case Inference::SPLIT_ZERO: return "SPLIT_ZERO";
-    case Inference::SIGN: return "SIGN";
-    case Inference::COMPARISON: return "COMPARISON";
-    case Inference::INFER_BOUNDS: return "INFER_BOUNDS";
-    case Inference::INFER_BOUNDS_NT: return "INFER_BOUNDS_NT";
-    case Inference::FACTOR: return "FACTOR";
-    case Inference::RES_INFER_BOUNDS: return "RES_INFER_BOUNDS";
-    case Inference::TANGENT_PLANE: return "TANGENT_PLANE";
-    case Inference::T_PURIFY_ARG: return "T_PURIFY_ARG";
-    case Inference::T_INIT_REFINE: return "T_INIT_REFINE";
-    case Inference::T_PI_BOUND: return "T_PI_BOUND";
-    case Inference::T_MONOTONICITY: return "T_MONOTONICITY";
-    case Inference::T_SECANT: return "T_SECANT";
-    case Inference::T_TANGENT: return "T_TANGENT";
-    case Inference::IAND_INIT_REFINE: return "IAND_INIT_REFINE";
-    case Inference::IAND_VALUE_REFINE: return "IAND_VALUE_REFINE";
-    case Inference::CAD_CONFLICT: return "CAD_CONFLICT";
-    case Inference::CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL";
-    default: return "?";
-  }
-}
-
-std::ostream& operator<<(std::ostream& out, Inference i)
-{
-  out << toString(i);
-  return out;
-}
-
-}  // namespace nl
-}  // namespace arith
-}  // namespace theory
-}  // namespace CVC4
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index c6c22c3c6..1c0635f1f 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -20,7 +20,6 @@
 
 #include "expr/node.h"
 #include "theory/arith/arith_lemma.h"
-#include "theory/arith/nl/inference.h"
 #include "theory/output_channel.h"
 
 namespace CVC4 {
@@ -48,11 +47,11 @@ class NlLemma : public ArithLemma
   NlLemma(Node n,
           LemmaProperty p,
           ProofGenerator* pg,
-          nl::Inference inf = nl::Inference::UNKNOWN)
+          InferenceId inf = InferenceId::UNKNOWN)
       : ArithLemma(n, p, pg, inf)
   {
   }
-  NlLemma(Node n, nl::Inference inf = nl::Inference::UNKNOWN)
+  NlLemma(Node n, InferenceId inf = InferenceId::UNKNOWN)
       : ArithLemma(n, LemmaProperty::NONE, nullptr, inf)
   {
   }
diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp
index 6c20eec76..d4a7db55f 100644
--- a/src/theory/arith/nl/nl_solver.cpp
+++ b/src/theory/arith/nl/nl_solver.cpp
@@ -178,7 +178,7 @@ std::vector<NlLemma> NlSolver::checkSplitZero()
       Node literal = d_containing.getValuation().ensureLiteral(eq);
       d_containing.getOutputChannel().requirePhase(literal, true);
       lemmas.emplace_back(literal.orNode(literal.negate()),
-                          Inference::SPLIT_ZERO);
+                          InferenceId::NL_SPLIT_ZERO);
     }
   }
   return lemmas;
@@ -274,7 +274,7 @@ int NlSolver::compareSign(Node oa,
     {
       Node lemma =
           safeConstructNary(AND, exp).impNode(mkLit(oa, d_zero, status * 2));
-      lem.emplace_back(lemma, Inference::SIGN);
+      lem.emplace_back(lemma, InferenceId::NL_SIGN);
     }
     return status;
   }
@@ -291,7 +291,7 @@ int NlSolver::compareSign(Node oa,
     if (mvaoa.getConst<Rational>().sgn() != 0)
     {
       Node lemma = av.eqNode(d_zero).impNode(oa.eqNode(d_zero));
-      lem.emplace_back(lemma, Inference::SIGN);
+      lem.emplace_back(lemma, InferenceId::NL_SIGN);
     }
     return 0;
   }
@@ -448,7 +448,7 @@ bool NlSolver::compareMonomial(
       Node clem = nm->mkNode(
           IMPLIES, safeConstructNary(AND, exp), mkLit(oa, ob, status, true));
       Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl;
-      lem.emplace_back(clem, Inference::COMPARISON);
+      lem.emplace_back(clem, InferenceId::NL_COMPARISON);
       cmp_infers[status][oa][ob] = clem;
     }
     return true;
@@ -1007,7 +1007,7 @@ std::vector<NlLemma> NlSolver::checkTangentPlanes()
             tplaneConj.push_back(lb_reverse2);
 
             Node tlem = nm->mkNode(AND, tplaneConj);
-            lemmas.emplace_back(tlem, Inference::TANGENT_PLANE);
+            lemmas.emplace_back(tlem, InferenceId::NL_TANGENT_PLANE);
           }
         }
       }
@@ -1262,11 +1262,11 @@ std::vector<NlLemma> NlSolver::checkMonomialInferBounds(
             // monomials = " << introNewTerms << std::endl;
             if (!introNewTerms)
             {
-              lemmas.emplace_back(iblem, Inference::INFER_BOUNDS);
+              lemmas.emplace_back(iblem, InferenceId::NL_INFER_BOUNDS);
             }
             else
             {
-              nt_lemmas.emplace_back(iblem, Inference::INFER_BOUNDS_NT);
+              nt_lemmas.emplace_back(iblem, InferenceId::NL_INFER_BOUNDS_NT);
             }
           }
         }
@@ -1398,7 +1398,7 @@ std::vector<NlLemma> NlSolver::checkFactoring(
           lemma_disj.push_back(conc_lit);
           Node flem = nm->mkNode(OR, lemma_disj);
           Trace("nl-ext-factor") << "...lemma is " << flem << std::endl;
-          lemmas.emplace_back(flem, Inference::FACTOR);
+          lemmas.emplace_back(flem, InferenceId::NL_FACTOR);
         }
       }
     }
@@ -1570,7 +1570,7 @@ std::vector<NlLemma> NlSolver::checkMonomialInferResBounds()
                   rblem = Rewriter::rewrite(rblem);
                   Trace("nl-ext-rbound-lemma")
                       << "Resolution bound lemma : " << rblem << std::endl;
-                  lemmas.emplace_back(rblem, Inference::RES_INFER_BOUNDS);
+                  lemmas.emplace_back(rblem, InferenceId::NL_RES_INFER_BOUNDS);
                 }
               }
               exp.pop_back();
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 09806cbbd..537dd604c 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -33,9 +33,8 @@ namespace nl {
 
 NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                        eq::EqualityEngine* ee)
-    : d_lemmas(containing.getUserContext()),
-      d_lemmasPp(containing.getUserContext()),
-      d_containing(containing),
+    : d_containing(containing),
+      d_im(containing.getInferenceManager()),
       d_ee(ee),
       d_needsLastCall(false),
       d_checkCounter(0),
@@ -75,22 +74,9 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
 {
   for (const NlLemma& nlem : out)
   {
-    Node lem = nlem.d_node;
-    LemmaProperty p = nlem.d_property;
     Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_inference
-                          << " : " << lem << std::endl;
-    d_containing.getOutputChannel().lemma(lem, p);
-    // process the side effect
-    processSideEffect(nlem);
-    // add to cache based on preprocess
-    if (isLemmaPropertyPreprocess(p))
-    {
-      d_lemmasPp.insert(lem);
-    }
-    else
-    {
-      d_lemmas.insert(lem);
-    }
+                          << " : " << nlem.d_node << std::endl;
+    d_im.addPendingArithLemma(nlem);
     d_stats.d_inferences << nlem.d_inference;
   }
 }
@@ -121,10 +107,8 @@ unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
   Trace("nl-ext-lemma-debug")
       << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_node << std::endl;
   lem.d_node = Rewriter::rewrite(lem.d_node);
-  // get the proper cache
-  NodeSet& lcache =
-      isLemmaPropertyPreprocess(lem.d_property) ? d_lemmasPp : d_lemmas;
-  if (lcache.find(lem.d_node) != lcache.end())
+
+  if (d_im.hasCachedLemma(lem.d_node, lem.d_property))
   {
     Trace("nl-ext-lemma-debug")
         << "NonlinearExtension::Lemma duplicate : " << lem.d_node << std::endl;
@@ -620,9 +604,12 @@ void NonlinearExtension::check(Theory::Effort e)
   else
   {
     // If we computed lemmas during collectModelInfo, send them now.
-    if (!d_cmiLemmas.empty())
+    if (!d_cmiLemmas.empty() || d_im.hasPendingLemma())
     {
       sendLemmas(d_cmiLemmas);
+      d_im.doPendingFacts();
+      d_im.doPendingLemmas();
+      d_im.doPendingPhaseRequirements();
       return;
     }
     // Otherwise, we will answer SAT. The values that we approximated are
@@ -799,7 +786,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
             d_containing.getOutputChannel().requirePhase(literal, true);
             Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
             Node split = literal.orNode(literal.negate());
-            NlLemma nsplit(split, Inference::SHARED_TERM_VALUE_SPLIT);
+            NlLemma nsplit(split, InferenceId::NL_SHARED_TERM_VALUE_SPLIT);
             filterLemma(nsplit, stvLemmas);
           }
           if (!stvLemmas.empty())
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 41f24e769..b62b81e9c 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -26,6 +26,7 @@
 #include "context/cdlist.h"
 #include "expr/kind.h"
 #include "expr/node.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad_solver.h"
 #include "theory/arith/nl/ext_theory_callback.h"
 #include "theory/arith/nl/iand_solver.h"
@@ -237,10 +238,6 @@ class NonlinearExtension
    */
   void sendLemmas(const std::vector<NlLemma>& out);
 
-  /** cache of all lemmas sent on the output channel (user-context-dependent) */
-  NodeSet d_lemmas;
-  /** Same as above, for preprocessed lemmas */
-  NodeSet d_lemmasPp;
   /** commonly used terms */
   Node d_zero;
   Node d_one;
@@ -248,6 +245,7 @@ class NonlinearExtension
   Node d_true;
   // The theory of arithmetic containing this extension.
   TheoryArith& d_containing;
+  InferenceManager& d_im;
   // pointer to used equality engine
   eq::EqualityEngine* d_ee;
   /** The statistics class */
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index 1a8a9419e..bc0791c4d 100644
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -18,7 +18,7 @@
 #define CVC4__THEORY__ARITH__NL__STATS_H
 
 #include "expr/kind.h"
-#include "theory/arith/nl/inference.h"
+#include "theory/arith/inference_id.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -42,7 +42,7 @@ class NlStats
   /** Number of calls to NonlinearExtension::checkLastCall */
   IntStat d_checkRuns;
   /** Counts the number of applications of each type of inference */
-  HistogramStat<Inference> d_inferences;
+  HistogramStat<InferenceId> d_inferences;
 };
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp
index b2ef16459..d075d5037 100644
--- a/src/theory/arith/nl/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental_solver.cpp
@@ -136,7 +136,7 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& assertions,
             }
             Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
             Node cong_lemma = nm->mkNode(OR, expn.negate(), a.eqNode(aa));
-            lems.emplace_back(cong_lemma, Inference::CONGRUENCE);
+            lems.emplace_back(cong_lemma, InferenceId::NL_CONGRUENCE);
           }
         }
         else
@@ -213,7 +213,7 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& assertions,
     Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
                           << std::endl;
     NlLemma nlem(
-        lem, LemmaProperty::PREPROCESS, nullptr, Inference::T_PURIFY_ARG);
+        lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG);
     lems.emplace_back(nlem);
   }
 
@@ -369,7 +369,7 @@ void TranscendentalSolver::getCurrentPiBounds(std::vector<NlLemma>& lemmas)
   Node pi_lem = nm->mkNode(AND,
                            nm->mkNode(GEQ, d_pi, d_pi_bound[0]),
                            nm->mkNode(LEQ, d_pi, d_pi_bound[1]));
-  lemmas.emplace_back(pi_lem, Inference::T_PI_BOUND);
+  lemmas.emplace_back(pi_lem, InferenceId::NL_T_PI_BOUND);
 }
 
 std::vector<NlLemma> TranscendentalSolver::checkTranscendentalInitialRefine()
@@ -454,7 +454,7 @@ std::vector<NlLemma> TranscendentalSolver::checkTranscendentalInitialRefine()
         }
         if (!lem.isNull())
         {
-          lemmas.emplace_back(lem, Inference::T_INIT_REFINE);
+          lemmas.emplace_back(lem, InferenceId::NL_T_INIT_REFINE);
         }
       }
     }
@@ -630,7 +630,7 @@ std::vector<NlLemma> TranscendentalSolver::checkTranscendentalMonotonic()
               }
               Trace("nl-ext-tf-mono")
                   << "Monotonicity lemma : " << mono_lem << std::endl;
-              lemmas.emplace_back(mono_lem, Inference::T_MONOTONICITY);
+              lemmas.emplace_back(mono_lem, InferenceId::NL_T_MONOTONICITY);
             }
           }
           // store the previous values
@@ -883,7 +883,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf,
         << "*** Tangent plane lemma : " << lem << std::endl;
     Assert(d_model.computeAbstractModelValue(lem) == d_false);
     // Figure 3 : line 9
-    lemmas.emplace_back(lem, Inference::T_TANGENT);
+    lemmas.emplace_back(lem, InferenceId::NL_T_TANGENT);
   }
   else if (is_secant)
   {
@@ -1017,7 +1017,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf,
     Assert(!lemmaConj.empty());
     Node lem =
         lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj);
-    NlLemma nlem(lem, Inference::T_SECANT);
+    NlLemma nlem(lem, InferenceId::NL_T_SECANT);
     // The side effect says that if lem is added, then we should add the
     // secant point c for (tf,d).
     nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index fbf25705c..1436198a8 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -41,7 +41,8 @@ TheoryArith::TheoryArith(context::Context* c,
       d_internal(
           new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
       d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
-      d_astate(*d_internal, c, u, valuation)
+      d_astate(*d_internal, c, u, valuation),
+      d_inferenceManager(*this, d_astate, pnm)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 71a25ac12..4851f1c5d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -19,6 +19,7 @@
 
 #include "expr/node.h"
 #include "theory/arith/arith_state.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/theory_arith_private_forward.h"
 #include "theory/theory.h"
 
@@ -96,9 +97,19 @@ class TheoryArith : public Theory {
 
   std::pair<bool, Node> entailmentCheck(TNode lit) override;
 
+  /** Return a reference to the arith::InferenceManager. */
+  InferenceManager& getInferenceManager()
+  {
+    return d_inferenceManager;
+  }
+
  private:
   /** The state object wrapping TheoryArithPrivate  */
   ArithState d_astate;
+
+  /** The arith::InferenceManager. */
+  InferenceManager d_inferenceManager;
+
 };/* class TheoryArith */
 
 }/* CVC4::theory::arith namespace */