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.

10 files changed, 39 insertions, 223 deletions

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/inference.h b/src/theory/arith/nl/inference.h
deleted file mode 100644
index 0cf6ad3bd..000000000
--- a/src/theory/arith/nl/inference.h
+++ /dev/null
@@ -1,109 +0,0 @@
-/*********************                                                        */
-/*! \file inference.h
- ** \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 Inference enumeration for non-linear arithmetic.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__THEORY__ARITH__NL__INFER_INFO_H
-#define CVC4__THEORY__ARITH__NL__INFER_INFO_H
-
-#include <map>
-#include <vector>
-
-#include "util/safe_print.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-namespace nl {
-
-/**
- * Types of inferences used in the procedure
- */
-enum class Inference : uint32_t
-{
-  //-------------------- core
-  // simple congruence x=y => f(x)=f(y)
-  CONGRUENCE,
-  // shared term value split (for naive theory combination)
-  SHARED_TERM_VALUE_SPLIT,
-  //-------------------- incremental linearization solver
-  // splitting on zero (NlSolver::checkSplitZero)
-  SPLIT_ZERO,
-  // based on sign (NlSolver::checkMonomialSign)
-  SIGN,
-  // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude)
-  COMPARISON,
-  // based on inferring bounds (NlSolver::checkMonomialInferBounds)
-  INFER_BOUNDS,
-  // same as above, for inferences that introduce new terms
-  INFER_BOUNDS_NT,
-  // factoring (NlSolver::checkFactoring)
-  FACTOR,
-  // resolution bound inferences (NlSolver::checkMonomialInferResBounds)
-  RES_INFER_BOUNDS,
-  // tangent planes (NlSolver::checkTangentPlanes)
-  TANGENT_PLANE,
-  //-------------------- transcendental solver
-  // purification of arguments to transcendental functions
-  T_PURIFY_ARG,
-  // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine)
-  T_INIT_REFINE,
-  // pi bounds
-  T_PI_BOUND,
-  // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic)
-  T_MONOTONICITY,
-  // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes)
-  T_TANGENT,
-  // secant refinement, the dual of the above inference
-  T_SECANT,
-  //-------------------- iand solver
-  // initial refinements (IAndSolver::checkInitialRefine)
-  IAND_INIT_REFINE,
-  // value refinements (IAndSolver::checkFullRefine)
-  IAND_VALUE_REFINE,
-  //-------------------- cad solver
-  // conflict / infeasible subset obtained from cad
-  CAD_CONFLICT,
-  // excludes an interval for a single variable
-  CAD_EXCLUDED_INTERVAL,
-  //-------------------- unknown
-  UNKNOWN,
-};
-
-/**
- * Converts an inference to a string. Note: This function is also used in
- * `safe_print()`. Changing this functions name or signature will result in
- * `safe_print()` printing "<unsupported>" instead of the proper strings for
- * the enum values.
- *
- * @param i The inference
- * @return The name of the inference
- */
-const char* toString(Inference i);
-
-/**
- * Writes an inference name to a stream.
- *
- * @param out The stream to write to
- * @param i The inference to write to the stream
- * @return The stream
- */
-std::ostream& operator<<(std::ostream& out, Inference i);
-
-}  // namespace nl
-}  // namespace arith
-}  // namespace theory
-}  // namespace CVC4
-
-#endif /* CVC4__THEORY__ARITH__NL__INFER_INFO_H */
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));