Associate all lemmas in non-linear arithmetic with an inference identifier (#4712)

This marks all lemmas in non-linear arithmetic with an identifier, which indicates informally the kind of justification that was used for them. The main motivation for this is for debugging the behavior of the non-linear solver.

The number of inferences can then be seen with --stats:

nl::inferences, [(SPLIT_ZERO : 19), (SIGN : 4), (COMPARISON : 29)]
The same design was used in strings and has been quite helpful.

This also adds a few high level stats to the new statistics class for non-linear.

10 files changed, 304 insertions, 26 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1b7236d3a..9331b1dc7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -302,6 +302,8 @@ libcvc4_add_sources(
   theory/arith/matrix.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
@@ -314,6 +316,8 @@ libcvc4_add_sources(
   theory/arith/nl/nl_solver.h
   theory/arith/nl/nonlinear_extension.cpp
   theory/arith/nl/nonlinear_extension.h
+  theory/arith/nl/stats.cpp
+  theory/arith/nl/stats.h
   theory/arith/nl/transcendental_solver.cpp
   theory/arith/nl/transcendental_solver.h
   theory/arith/normal_form.cpp
diff --git a/src/theory/arith/nl/inference.cpp b/src/theory/arith/nl/inference.cpp
new file mode 100644
index 000000000..34242e746
--- /dev/null
+++ b/src/theory/arith/nl/inference.cpp
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \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";
+    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
new file mode 100644
index 000000000..99b7e681e
--- /dev/null
+++ b/src/theory/arith/nl/inference.h
@@ -0,0 +1,99 @@
+/*********************                                                        */
+/*! \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,
+  //-------------------- 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 eaa9adcc3..2b5158f18 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -18,6 +18,7 @@
 #include <tuple>
 #include <vector>
 #include "expr/node.h"
+#include "theory/arith/nl/inference.h"
 
 namespace CVC4 {
 namespace theory {
@@ -39,8 +40,13 @@ class NlModel;
  */
 struct NlLemma
 {
-  NlLemma(Node lem) : d_lemma(lem), d_preprocess(false) {}
+  NlLemma(Node lem, Inference id = Inference::UNKNOWN)
+      : d_id(id), d_lemma(lem), d_preprocess(false)
+  {
+  }
   ~NlLemma() {}
+  /** The inference id for the lemma */
+  Inference d_id;
   /** The lemma */
   Node d_lemma;
   /** Whether to preprocess the lemma */
diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp
index fee89caf6..521539674 100644
--- a/src/theory/arith/nl/nl_solver.cpp
+++ b/src/theory/arith/nl/nl_solver.cpp
@@ -177,7 +177,8 @@ std::vector<NlLemma> NlSolver::checkSplitZero()
       eq = Rewriter::rewrite(eq);
       Node literal = d_containing.getValuation().ensureLiteral(eq);
       d_containing.getOutputChannel().requirePhase(literal, true);
-      lemmas.push_back(literal.orNode(literal.negate()));
+      lemmas.emplace_back(literal.orNode(literal.negate()),
+                          Inference::SPLIT_ZERO);
     }
   }
   return lemmas;
@@ -273,7 +274,7 @@ int NlSolver::compareSign(Node oa,
     {
       Node lemma =
           safeConstructNary(AND, exp).impNode(mkLit(oa, d_zero, status * 2));
-      lem.push_back(lemma);
+      lem.emplace_back(lemma, Inference::SIGN);
     }
     return status;
   }
@@ -290,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.push_back(lemma);
+      lem.emplace_back(lemma, Inference::SIGN);
     }
     return 0;
   }
@@ -447,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.push_back(clem);
+      lem.emplace_back(clem, Inference::COMPARISON);
       cmp_infers[status][oa][ob] = clem;
     }
     return true;
@@ -943,6 +944,8 @@ std::vector<NlLemma> NlSolver::checkTangentPlanes()
                 nm->mkNode(
                     PLUS, nm->mkNode(MULT, b_v, a), nm->mkNode(MULT, a_v, b)),
                 nm->mkNode(MULT, a_v, b_v));
+            // conjuncts of the tangent plane lemma
+            std::vector<Node> tplaneConj;
             for (unsigned d = 0; d < 4; d++)
             {
               Node aa = nm->mkNode(d == 0 || d == 3 ? GEQ : LEQ, a, a_v);
@@ -951,7 +954,7 @@ std::vector<NlLemma> NlSolver::checkTangentPlanes()
               Node tlem = nm->mkNode(OR, aa.negate(), ab.negate(), conc);
               Trace("nl-ext-tplanes")
                   << "Tangent plane lemma : " << tlem << std::endl;
-              lemmas.push_back(tlem);
+              tplaneConj.push_back(tlem);
             }
 
             // tangent plane reverse implication
@@ -974,13 +977,13 @@ std::vector<NlLemma> NlSolver::checkTangentPlanes()
             Trace("nl-ext-tplanes")
                 << "Tangent plane lemma (reverse) : " << ub_reverse1
                 << std::endl;
-            lemmas.push_back(ub_reverse1);
+            tplaneConj.push_back(ub_reverse1);
             Node ub_reverse2 =
                 nm->mkNode(OR, t_leq_tplane.negate(), b_geq_bv_or_a_geq_av);
             Trace("nl-ext-tplanes")
                 << "Tangent plane lemma (reverse) : " << ub_reverse2
                 << std::endl;
-            lemmas.push_back(ub_reverse2);
+            tplaneConj.push_back(ub_reverse2);
 
             // t >= tplane -> ( (a <= a_v ^ b <= b_v) v
             // (a >= a_v ^ b >= b_v) ).
@@ -995,13 +998,16 @@ std::vector<NlLemma> NlSolver::checkTangentPlanes()
             Trace("nl-ext-tplanes")
                 << "Tangent plane lemma (reverse) : " << lb_reverse1
                 << std::endl;
-            lemmas.push_back(lb_reverse1);
+            tplaneConj.push_back(lb_reverse1);
             Node lb_reverse2 =
                 nm->mkNode(OR, t_geq_tplane.negate(), a_geq_av_or_b_leq_bv);
             Trace("nl-ext-tplanes")
                 << "Tangent plane lemma (reverse) : " << lb_reverse2
                 << std::endl;
-            lemmas.push_back(lb_reverse2);
+            tplaneConj.push_back(lb_reverse2);
+
+            Node tlem = nm->mkNode(AND, tplaneConj);
+            lemmas.emplace_back(tlem, Inference::TANGENT_PLANE);
           }
         }
       }
@@ -1256,11 +1262,11 @@ std::vector<NlLemma> NlSolver::checkMonomialInferBounds(
             // monomials = " << introNewTerms << std::endl;
             if (!introNewTerms)
             {
-              lemmas.push_back(iblem);
+              lemmas.emplace_back(iblem, Inference::INFER_BOUNDS);
             }
             else
             {
-              nt_lemmas.push_back(iblem);
+              nt_lemmas.emplace_back(iblem, Inference::INFER_BOUNDS_NT);
             }
           }
         }
@@ -1392,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.push_back(flem);
+          lemmas.emplace_back(flem, Inference::FACTOR);
         }
       }
     }
@@ -1564,7 +1570,7 @@ std::vector<NlLemma> NlSolver::checkMonomialInferResBounds()
                   rblem = Rewriter::rewrite(rblem);
                   Trace("nl-ext-rbound-lemma")
                       << "Resolution bound lemma : " << rblem << std::endl;
-                  lemmas.push_back(rblem);
+                  lemmas.emplace_back(rblem, Inference::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 bd48a726a..97f0ce2c1 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -152,7 +152,8 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
   {
     Node lem = nlem.d_lemma;
     bool preprocess = nlem.d_preprocess;
-    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
+    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_id
+                          << " : " << lem << std::endl;
     d_containing.getOutputChannel().lemma(lem, false, preprocess);
     // process the side effect
     processSideEffect(nlem);
@@ -165,6 +166,7 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
     {
       d_lemmas.insert(lem);
     }
+    d_stats.d_inferences << nlem.d_id;
     // also indicate this is a tautology
     d_model.addTautology(lem);
   }
@@ -188,7 +190,7 @@ unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
         << "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl;
     return 0;
   }
-  out.push_back(lem);
+  out.emplace_back(lem);
   return 1;
 }
 
@@ -405,6 +407,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
 {
   std::vector<NlLemma> lemmas;
 
+  ++(d_stats.d_checkRuns);
+
   if (options::nlExt())
   {
     // initialize the non-linear solver
@@ -639,6 +643,8 @@ void NonlinearExtension::check(Theory::Effort e)
 
 bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
 {
+  ++(d_stats.d_mbrRuns);
+
   // get the assertions
   std::vector<Node> assertions;
   getAssertions(assertions);
@@ -647,6 +653,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
       << "Getting model values... check for [model-false]" << std::endl;
   // get the assertions that are false in the model
   const std::vector<Node> false_asserts = checkModelEval(assertions);
+  Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl;
 
   // get the extended terms belonging to this theory
   std::vector<Node> xts;
@@ -786,7 +793,8 @@ 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());
-            filterLemma(split, stvLemmas);
+            NlLemma nsplit(split, Inference::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 ed1838b4b..69710265c 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -29,6 +29,7 @@
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/nl_solver.h"
+#include "theory/arith/nl/stats.h"
 #include "theory/arith/nl/transcendental_solver.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/uf/equality_engine.h"
@@ -284,6 +285,8 @@ class NonlinearExtension
   TheoryArith& d_containing;
   // pointer to used equality engine
   eq::EqualityEngine* d_ee;
+  /** The statistics class */
+  NlStats d_stats;
   // needs last call effort
   bool d_needsLastCall;
   /** The non-linear model object
diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp
new file mode 100644
index 000000000..e189d13a8
--- /dev/null
+++ b/src/theory/arith/nl/stats.cpp
@@ -0,0 +1,44 @@
+/*********************                                                        */
+/*! \file stats.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 Statistics for non-linear arithmetic
+ **/
+
+#include "theory/arith/nl/stats.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+NlStats::NlStats()
+    : d_mbrRuns("nl::mbrRuns", 0),
+      d_checkRuns("nl::checkRuns", 0),
+      d_inferences("nl::inferences")
+{
+  smtStatisticsRegistry()->registerStat(&d_mbrRuns);
+  smtStatisticsRegistry()->registerStat(&d_checkRuns);
+  smtStatisticsRegistry()->registerStat(&d_inferences);
+}
+
+NlStats::~NlStats()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_mbrRuns);
+  smtStatisticsRegistry()->unregisterStat(&d_checkRuns);
+  smtStatisticsRegistry()->unregisterStat(&d_inferences);
+}
+
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
new file mode 100644
index 000000000..1a8a9419e
--- /dev/null
+++ b/src/theory/arith/nl/stats.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file stats.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 Statistics for non-linear arithmetic
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__STATS_H
+#define CVC4__THEORY__ARITH__NL__STATS_H
+
+#include "expr/kind.h"
+#include "theory/arith/nl/inference.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+/**
+ * Statistics for non-linear arithmetic
+ */
+class NlStats
+{
+ public:
+  NlStats();
+  ~NlStats();
+  /**
+   * Number of calls to NonlinearExtension::modelBasedRefinement. Notice this
+   * may make multiple calls to NonlinearExtension::checkLastCall.
+   */
+  IntStat d_mbrRuns;
+  /** Number of calls to NonlinearExtension::checkLastCall */
+  IntStat d_checkRuns;
+  /** Counts the number of applications of each type of inference */
+  HistogramStat<Inference> d_inferences;
+};
+
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__NL__STATS_H */
diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp
index 1a80342bc..321818b94 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.push_back(cong_lemma);
+            lems.emplace_back(cong_lemma, Inference::CONGRUENCE);
           }
         }
         else
@@ -212,9 +212,9 @@ void TranscendentalSolver::initLastCall(const std::vector<Node>& assertions,
     // note we must do preprocess on this lemma
     Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
                           << std::endl;
-    NlLemma nlem(lem);
+    NlLemma nlem(lem, Inference::T_PURIFY_ARG);
     nlem.d_preprocess = true;
-    lems.push_back(nlem);
+    lems.emplace_back(nlem);
   }
 
   if (Trace.isOn("nl-ext-mv"))
@@ -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.push_back(pi_lem);
+  lemmas.emplace_back(pi_lem, Inference::T_PI_BOUND);
 }
 
 std::vector<NlLemma> TranscendentalSolver::checkTranscendentalInitialRefine()
@@ -454,7 +454,7 @@ std::vector<NlLemma> TranscendentalSolver::checkTranscendentalInitialRefine()
         }
         if (!lem.isNull())
         {
-          lemmas.push_back(lem);
+          lemmas.emplace_back(lem, Inference::T_INIT_REFINE);
         }
       }
     }
@@ -630,7 +630,7 @@ std::vector<NlLemma> TranscendentalSolver::checkTranscendentalMonotonic()
               }
               Trace("nl-ext-tf-mono")
                   << "Monotonicity lemma : " << mono_lem << std::endl;
-              lemmas.push_back(mono_lem);
+              lemmas.emplace_back(mono_lem, Inference::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.push_back(lem);
+    lemmas.emplace_back(lem, Inference::T_TANGENT);
   }
   else if (is_secant)
   {
@@ -1017,11 +1017,11 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf,
     Assert(!lemmaConj.empty());
     Node lem =
         lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj);
-    NlLemma nlem(lem);
+    NlLemma nlem(lem, Inference::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));
-    lemmas.push_back(nlem);
+    lemmas.emplace_back(nlem);
   }
   return true;
 }