From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 6 Jun 2020 17:25:50 +0000 (-0500)
Subject: Use NlLemma utility for all lemmas in non-linear. (#4573)
X-Git-Tag: cvc5-1.0.0~3241
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=79d0e47c14a9e8213d6c6e112835142cf2417943;p=cvc5.git

Use NlLemma utility for all lemmas in non-linear. (#4573)

This makes it much easier to set custom properties of lemmas (e.g. preprocess) and also will allow proof tracking and debugging in the future.

This also enables a fix on the IAND branch related to preprocessing lemmas.
---

diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp
index ca34d91a9..c1ec42497 100644
--- a/src/theory/arith/nl/nl_lemma_utils.cpp
+++ b/src/theory/arith/nl/nl_lemma_utils.cpp
@@ -21,6 +21,12 @@ namespace theory {
 namespace arith {
 namespace nl {
 
+std::ostream& operator<<(std::ostream& out, NlLemma& n)
+{
+  out << n.d_lemma;
+  return out;
+}
+
 bool SortNlModel::operator()(Node i, Node j)
 {
   int cv = d_nlm->compare(i, j, d_isConcrete, d_isAbsolute);
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index 64a4deb17..a0fce378f 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -27,16 +27,24 @@ namespace nl {
 class NlModel;
 
 /**
- * A side effect of adding a lemma in the non-linear solver. This is used
- * to specify how the state of the non-linear solver should update. This
- * includes:
+ * The data structure for a single lemma to process by the non-linear solver,
+ * including the lemma itself and whether it should be preprocessed (see
+ * OutputChannel::lemma).
+ *
+ * This also includes data structures that encapsulate the side effect of adding
+ * this lemma in the non-linear solver. This is used to specify how the state of
+ * the non-linear solver should update. This includes:
  * - A set of secant points to record (for transcendental secant plane
  * inferences).
  */
-struct NlLemmaSideEffect
+struct NlLemma
 {
-  NlLemmaSideEffect() {}
-  ~NlLemmaSideEffect() {}
+  NlLemma(Node lem) : d_lemma(lem), d_preprocess(false) {}
+  ~NlLemma() {}
+  /** The lemma */
+  Node d_lemma;
+  /** Whether to preprocess the lemma */
+  bool d_preprocess;
   /** secant points to add
    *
    * A member (tf, d, c) in this vector indicates that point c should be added
@@ -48,6 +56,10 @@ struct NlLemmaSideEffect
    */
   std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint;
 };
+/**
+ * Writes a non-linear lemma to a stream.
+ */
+std::ostream& operator<<(std::ostream& out, NlLemma& n);
 
 struct SortNlModel
 {
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index d5df96bd8..2ed901f1f 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -213,7 +213,7 @@ int NlModel::compareValue(Node i, Node j, bool isAbsolute) const
 bool NlModel::checkModel(const std::vector<Node>& assertions,
                          const std::vector<Node>& false_asserts,
                          unsigned d,
-                         std::vector<Node>& lemmas,
+                         std::vector<NlLemma>& lemmas,
                          std::vector<Node>& gs)
 {
   Trace("nl-ext-cm-debug") << "  solve for equalities..." << std::endl;
@@ -478,7 +478,7 @@ void NlModel::addTautology(Node n)
 
 bool NlModel::solveEqualitySimple(Node eq,
                                   unsigned d,
-                                  std::vector<Node>& lemmas)
+                                  std::vector<NlLemma>& lemmas)
 {
   Node seq = eq;
   if (!d_check_model_vars.empty())
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index 61193fc12..7a40e3926 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -23,6 +23,7 @@
 #include "context/context.h"
 #include "expr/kind.h"
 #include "expr/node.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {
@@ -152,7 +153,7 @@ class NlModel
   bool checkModel(const std::vector<Node>& assertions,
                   const std::vector<Node>& false_asserts,
                   unsigned d,
-                  std::vector<Node>& lemmas,
+                  std::vector<NlLemma>& lemmas,
                   std::vector<Node>& gs);
   /**
    * Set that we have used an approximation during this check. This flag is
@@ -233,7 +234,7 @@ class NlModel
    * For instance, if eq reduces to a univariate quadratic equation with no
    * root, we send a conflict clause of the form a*x^2 + b*x + c != 0.
    */
-  bool solveEqualitySimple(Node eq, unsigned d, std::vector<Node>& lemmas);
+  bool solveEqualitySimple(Node eq, unsigned d, std::vector<NlLemma>& lemmas);
 
   /** simple check model for transcendental functions for literal
    *
diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp
index 12cb02c70..c24ea41c8 100644
--- a/src/theory/arith/nl/nl_solver.cpp
+++ b/src/theory/arith/nl/nl_solver.cpp
@@ -165,9 +165,9 @@ void NlSolver::setMonomialFactor(Node a, Node b, const NodeMultiset& common)
   }
 }
 
-std::vector<Node> NlSolver::checkSplitZero()
+std::vector<NlLemma> NlSolver::checkSplitZero()
 {
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   for (unsigned i = 0; i < d_ms_vars.size(); i++)
   {
     Node v = d_ms_vars[i];
@@ -260,7 +260,7 @@ int NlSolver::compareSign(Node oa,
                           unsigned a_index,
                           int status,
                           std::vector<Node>& exp,
-                          std::vector<Node>& lem)
+                          std::vector<NlLemma>& lem)
 {
   Trace("nl-ext-debug") << "Process " << a << " at index " << a_index
                         << ", status is " << status << std::endl;
@@ -311,7 +311,7 @@ bool NlSolver::compareMonomial(
     Node b,
     NodeMultiset& b_exp_proc,
     std::vector<Node>& exp,
-    std::vector<Node>& lem,
+    std::vector<NlLemma>& lem,
     std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers)
 {
   Trace("nl-ext-comp-debug")
@@ -415,7 +415,7 @@ bool NlSolver::compareMonomial(
     NodeMultiset& b_exp_proc,
     int status,
     std::vector<Node>& exp,
-    std::vector<Node>& lem,
+    std::vector<NlLemma>& lem,
     std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers)
 {
   Trace("nl-ext-comp-debug")
@@ -628,9 +628,9 @@ bool NlSolver::compareMonomial(
   return false;
 }
 
-std::vector<Node> NlSolver::checkMonomialSign()
+std::vector<NlLemma> NlSolver::checkMonomialSign()
 {
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   std::map<Node, int> signs;
   Trace("nl-ext") << "Get monomial sign lemmas..." << std::endl;
   for (unsigned j = 0; j < d_ms.size(); j++)
@@ -667,7 +667,7 @@ std::vector<Node> NlSolver::checkMonomialSign()
   return lemmas;
 }
 
-std::vector<Node> NlSolver::checkMonomialMagnitude(unsigned c)
+std::vector<NlLemma> NlSolver::checkMonomialMagnitude(unsigned c)
 {
   // ensure information is setup
   if (c == 0)
@@ -681,7 +681,7 @@ std::vector<Node> NlSolver::checkMonomialMagnitude(unsigned c)
   }
 
   unsigned r = 1;
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L
   // in lemmas
   std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers;
@@ -803,7 +803,7 @@ std::vector<Node> NlSolver::checkMonomialMagnitude(unsigned c)
   Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size()
                        << " lemmas." << std::endl;
   // naive
-  std::vector<Node> r_lemmas;
+  std::unordered_set<Node, NodeHashFunction> r_lemmas;
   for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb =
            cmp_infers.begin();
        itb != cmp_infers.end();
@@ -828,7 +828,7 @@ std::vector<Node> NlSolver::checkMonomialMagnitude(unsigned c)
             std::vector<Node> exp;
             if (cmp_holds(itc3->first, itc2->first, itb->second, exp, visited))
             {
-              r_lemmas.push_back(itc2->second);
+              r_lemmas.insert(itc2->second);
               Trace("nl-ext-comp")
                   << "...inference of " << itc->first << " > " << itc2->first
                   << " was redundant." << std::endl;
@@ -839,11 +839,10 @@ std::vector<Node> NlSolver::checkMonomialMagnitude(unsigned c)
       }
     }
   }
-  std::vector<Node> nr_lemmas;
+  std::vector<NlLemma> nr_lemmas;
   for (unsigned i = 0; i < lemmas.size(); i++)
   {
-    if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i])
-        == r_lemmas.end())
+    if (r_lemmas.find(lemmas[i].d_lemma) == r_lemmas.end())
     {
       nr_lemmas.push_back(lemmas[i]);
     }
@@ -855,9 +854,9 @@ std::vector<Node> NlSolver::checkMonomialMagnitude(unsigned c)
   return nr_lemmas;
 }
 
-std::vector<Node> NlSolver::checkTangentPlanes()
+std::vector<NlLemma> NlSolver::checkTangentPlanes()
 {
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   const std::map<Node, std::vector<Node> >& ccMap =
@@ -1013,8 +1012,8 @@ std::vector<Node> NlSolver::checkTangentPlanes()
   return lemmas;
 }
 
-std::vector<Node> NlSolver::checkMonomialInferBounds(
-    std::vector<Node>& nt_lemmas,
+std::vector<NlLemma> NlSolver::checkMonomialInferBounds(
+    std::vector<NlLemma>& nt_lemmas,
     const std::vector<Node>& asserts,
     const std::vector<Node>& false_asserts)
 {
@@ -1028,7 +1027,7 @@ std::vector<Node> NlSolver::checkMonomialInferBounds(
   const std::map<Node, std::map<Node, ConstraintInfo> >& cim =
       d_cdb.getConstraints();
 
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   NodeManager* nm = NodeManager::currentNM();
   // register constraints
   Trace("nl-ext-debug") << "Register bound constraints..." << std::endl;
@@ -1271,10 +1270,10 @@ std::vector<Node> NlSolver::checkMonomialInferBounds(
   return lemmas;
 }
 
-std::vector<Node> NlSolver::checkFactoring(
+std::vector<NlLemma> NlSolver::checkFactoring(
     const std::vector<Node>& asserts, const std::vector<Node>& false_asserts)
 {
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   NodeManager* nm = NodeManager::currentNM();
   Trace("nl-ext") << "Get factoring lemmas..." << std::endl;
   for (const Node& lit : asserts)
@@ -1401,7 +1400,7 @@ std::vector<Node> NlSolver::checkFactoring(
   return lemmas;
 }
 
-Node NlSolver::getFactorSkolem(Node n, std::vector<Node>& lemmas)
+Node NlSolver::getFactorSkolem(Node n, std::vector<NlLemma>& lemmas)
 {
   std::map<Node, Node>::iterator itf = d_factor_skolem.find(n);
   if (itf == d_factor_skolem.end())
@@ -1416,9 +1415,9 @@ Node NlSolver::getFactorSkolem(Node n, std::vector<Node>& lemmas)
   return itf->second;
 }
 
-std::vector<Node> NlSolver::checkMonomialInferResBounds()
+std::vector<NlLemma> NlSolver::checkMonomialInferResBounds()
 {
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   NodeManager* nm = NodeManager::currentNM();
   Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..."
                   << std::endl;
diff --git a/src/theory/arith/nl/nl_solver.h b/src/theory/arith/nl/nl_solver.h
index 35c51569b..a2f514b9d 100644
--- a/src/theory/arith/nl/nl_solver.h
+++ b/src/theory/arith/nl/nl_solver.h
@@ -79,7 +79,7 @@ class NlSolver
    *   t = 0 V t != 0
    * where t is a term that exists in the current context.
    */
-  std::vector<Node> checkSplitZero();
+  std::vector<NlLemma> checkSplitZero();
 
   /** check monomial sign
    *
@@ -96,7 +96,7 @@ class NlSolver
    * x < 0 => x*y*y < 0
    * x = 0 => x*y*z = 0
    */
-  std::vector<Node> checkMonomialSign();
+  std::vector<NlLemma> checkMonomialSign();
 
   /** check monomial magnitude
    *
@@ -118,7 +118,7 @@ class NlSolver
    * against 1, 1 : compare non-linear monomials against variables, 2 : compare
    * non-linear monomials against other non-linear monomials.
    */
-  std::vector<Node> checkMonomialMagnitude(unsigned c);
+  std::vector<NlLemma> checkMonomialMagnitude(unsigned c);
 
   /** check monomial inferred bounds
    *
@@ -137,8 +137,8 @@ class NlSolver
    *   ...where (y > z + w) and x*y are a constraint and term
    *      that occur in the current context.
    */
-  std::vector<Node> checkMonomialInferBounds(
-      std::vector<Node>& nt_lemmas,
+  std::vector<NlLemma> checkMonomialInferBounds(
+      std::vector<NlLemma>& nt_lemmas,
       const std::vector<Node>& asserts,
       const std::vector<Node>& false_asserts);
 
@@ -154,8 +154,8 @@ class NlSolver
    *   ...where k is fresh and x*z + y*z > t is a
    *      constraint that occurs in the current context.
    */
-  std::vector<Node> checkFactoring(const std::vector<Node>& asserts,
-                                   const std::vector<Node>& false_asserts);
+  std::vector<NlLemma> checkFactoring(const std::vector<Node>& asserts,
+                                      const std::vector<Node>& false_asserts);
 
   /** check monomial infer resolution bounds
    *
@@ -171,7 +171,7 @@ class NlSolver
    *  ...where s <= x*z and x*y <= t are constraints
    *     that occur in the current context.
    */
-  std::vector<Node> checkMonomialInferResBounds();
+  std::vector<NlLemma> checkMonomialInferResBounds();
 
   /** check tangent planes
    *
@@ -197,7 +197,7 @@ class NlSolver
    * ( ( x>2 ^ y>5) ^ (x<2 ^ y<5) ) => x*y > 5*x + 2*y - 10
    * ( ( x>2 ^ y<5) ^ (x<2 ^ y>5) ) => x*y < 5*x + 2*y - 10
    */
-  std::vector<Node> checkTangentPlanes();
+  std::vector<NlLemma> checkTangentPlanes();
 
   //-------------------------------------------- end lemma schemas
  private:
@@ -295,7 +295,7 @@ class NlSolver
                   unsigned a_index,
                   int status,
                   std::vector<Node>& exp,
-                  std::vector<Node>& lem);
+                  std::vector<NlLemma>& lem);
   /** compare monomials a and b
    *
    * Initially, a call to this function is such that :
@@ -338,7 +338,7 @@ class NlSolver
       Node b,
       NodeMultiset& b_exp_proc,
       std::vector<Node>& exp,
-      std::vector<Node>& lem,
+      std::vector<NlLemma>& lem,
       std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
   /** helper function for above
    *
@@ -356,10 +356,10 @@ class NlSolver
       NodeMultiset& b_exp_proc,
       int status,
       std::vector<Node>& exp,
-      std::vector<Node>& lem,
+      std::vector<NlLemma>& lem,
       std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
   /** Get factor skolem for n, add resulting lemmas to lemmas */
-  Node getFactorSkolem(Node n, std::vector<Node>& lemmas);
+  Node getFactorSkolem(Node n, std::vector<NlLemma>& lemmas);
 }; /* class NlSolver */
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 4b2d2fd37..bf3e7fdda 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -33,6 +33,7 @@ namespace nl {
 NonlinearExtension::NonlinearExtension(TheoryArith& containing,
                                        eq::EqualityEngine* ee)
     : d_lemmas(containing.getUserContext()),
+      d_lemmasPp(containing.getUserContext()),
       d_containing(containing),
       d_ee(ee),
       d_needsLastCall(false),
@@ -143,23 +144,22 @@ std::pair<bool, Node> NonlinearExtension::isExtfReduced(
   return std::make_pair(true, Node::null());
 }
 
-void NonlinearExtension::sendLemmas(const std::vector<Node>& out,
-                                    bool preprocess,
-                                    std::map<Node, NlLemmaSideEffect>& lemSE)
+void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
 {
-  std::map<Node, NlLemmaSideEffect>::iterator its;
-  for (const Node& lem : out)
+  for (const NlLemma& nlem : out)
   {
+    Node lem = nlem.d_lemma;
+    bool preprocess = nlem.d_preprocess;
     Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
     d_containing.getOutputChannel().lemma(lem, false, preprocess);
     // process the side effect
-    its = lemSE.find(lem);
-    if (its != lemSE.end())
+    processSideEffect(nlem);
+    // add to cache if not preprocess
+    if (preprocess)
     {
-      processSideEffect(its->second);
+      d_lemmasPp.insert(lem);
     }
-    // add to cache if not preprocess
-    if (!preprocess)
+    else
     {
       d_lemmas.insert(lem);
     }
@@ -168,36 +168,37 @@ void NonlinearExtension::sendLemmas(const std::vector<Node>& out,
   }
 }
 
-void NonlinearExtension::processSideEffect(const NlLemmaSideEffect& se)
+void NonlinearExtension::processSideEffect(const NlLemma& se)
 {
   d_trSlv.processSideEffect(se);
 }
 
-unsigned NonlinearExtension::filterLemma(Node lem, std::vector<Node>& out)
+unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
 {
   Trace("nl-ext-lemma-debug")
-      << "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl;
-  lem = Rewriter::rewrite(lem);
-  if (d_lemmas.find(lem) != d_lemmas.end()
-      || std::find(out.begin(), out.end(), lem) != out.end())
+      << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_lemma << std::endl;
+  lem.d_lemma = Rewriter::rewrite(lem.d_lemma);
+  // get the proper cache
+  NodeSet& lcache = lem.d_preprocess ? d_lemmasPp : d_lemmas;
+  if (lcache.find(lem.d_lemma) != lcache.end())
   {
     Trace("nl-ext-lemma-debug")
-        << "NonlinearExtension::Lemma duplicate : " << lem << std::endl;
+        << "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl;
     return 0;
   }
   out.push_back(lem);
   return 1;
 }
 
-unsigned NonlinearExtension::filterLemmas(std::vector<Node>& lemmas,
-                                          std::vector<Node>& out)
+unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
+                                          std::vector<NlLemma>& out)
 {
   if (options::nlExtEntailConflicts())
   {
     // check if any are entailed to be false
-    for (const Node& lem : lemmas)
+    for (const NlLemma& lem : lemmas)
     {
-      Node ch_lemma = lem.negate();
+      Node ch_lemma = lem.d_lemma.negate();
       ch_lemma = Rewriter::rewrite(ch_lemma);
       Trace("nl-ext-et-debug")
           << "Check entailment of " << ch_lemma << "..." << std::endl;
@@ -207,8 +208,8 @@ unsigned NonlinearExtension::filterLemmas(std::vector<Node>& lemmas,
                                << et.second << std::endl;
       if (et.first)
       {
-        Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " << lem
-                           << std::endl;
+        Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : "
+                           << lem.d_lemma << std::endl;
         // return just this lemma
         if (filterLemma(lem, out) > 0)
         {
@@ -220,7 +221,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector<Node>& lemmas,
   }
 
   unsigned sum = 0;
-  for (const Node& lem : lemmas)
+  for (const NlLemma& lem : lemmas)
   {
     sum += filterLemma(lem, out);
   }
@@ -371,7 +372,7 @@ std::vector<Node> NonlinearExtension::checkModelEval(
 
 bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
                                     const std::vector<Node>& false_asserts,
-                                    std::vector<Node>& lemmas,
+                                    std::vector<NlLemma>& lemmas,
                                     std::vector<Node>& gs)
 {
   Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
@@ -396,24 +397,22 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
 int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                                       const std::vector<Node>& false_asserts,
                                       const std::vector<Node>& xts,
-                                      std::vector<Node>& lems,
-                                      std::vector<Node>& lemsPp,
-                                      std::vector<Node>& wlems,
-                                      std::map<Node, NlLemmaSideEffect>& lemSE)
+                                      std::vector<NlLemma>& lems,
+                                      std::vector<NlLemma>& wlems)
 {
   // initialize the non-linear solver
   d_nlSlv.initLastCall(assertions, false_asserts, xts);
   // initialize the trancendental function solver
-  std::vector<Node> lemmas;
-  d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas, lemsPp);
+  std::vector<NlLemma> lemmas;
+  d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas);
 
   // process lemmas that may have been generated by the transcendental solver
   filterLemmas(lemmas, lems);
-  if (!lems.empty() || !lemsPp.empty())
+  if (!lems.empty())
   {
     Trace("nl-ext") << "  ...finished with " << lems.size()
                     << " new lemmas during registration." << std::endl;
-    return lems.size() + lemsPp.size();
+    return lems.size();
   }
 
   //----------------------------------- possibly split on zero
@@ -480,7 +479,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
 
   //-----------------------------------inferred bounds lemmas
   //  e.g. x >= t => y*x >= y*t
-  std::vector<Node> nt_lemmas;
+  std::vector<NlLemma> nt_lemmas;
   lemmas =
       d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts);
   // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
@@ -546,7 +545,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
   if (options::nlExtTfTangentPlanes())
   {
-    lemmas = d_trSlv.checkTranscendentalTangentPlanes(lemSE);
+    lemmas = d_trSlv.checkTranscendentalTangentPlanes();
     filterLemmas(lemmas, wlems);
   }
   Trace("nl-ext") << "  ...finished with " << wlems.size() << " waiting lemmas."
@@ -585,10 +584,9 @@ void NonlinearExtension::check(Theory::Effort e)
   else
   {
     // If we computed lemmas during collectModelInfo, send them now.
-    if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty())
+    if (!d_cmiLemmas.empty())
     {
-      sendLemmas(d_cmiLemmas, false, d_cmiLemmasSE);
-      sendLemmas(d_cmiLemmasPp, true, d_cmiLemmasSE);
+      sendLemmas(d_cmiLemmas);
       return;
     }
     // Otherwise, we will answer SAT. The values that we approximated are
@@ -608,10 +606,7 @@ void NonlinearExtension::check(Theory::Effort e)
   }
 }
 
-bool NonlinearExtension::modelBasedRefinement(
-    std::vector<Node>& mlems,
-    std::vector<Node>& mlemsPp,
-    std::map<Node, NlLemmaSideEffect>& lemSE)
+bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
 {
   // get the assertions
   std::vector<Node> assertions;
@@ -691,15 +686,14 @@ bool NonlinearExtension::modelBasedRefinement(
     //   1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown
     int complete_status = 1;
     // lemmas that should be sent later
-    std::vector<Node> wlems;
+    std::vector<NlLemma> wlems;
     // We require a check either if an assertion is false or a shared term has
     // a wrong value
     if (!false_asserts.empty() || num_shared_wrong_value > 0)
     {
       complete_status = num_shared_wrong_value > 0 ? -1 : 0;
-      checkLastCall(
-          assertions, false_asserts, xts, mlems, mlemsPp, wlems, lemSE);
-      if (!mlems.empty() || !mlemsPp.empty())
+      checkLastCall(assertions, false_asserts, xts, mlems, wlems);
+      if (!mlems.empty())
       {
         return true;
       }
@@ -715,7 +709,7 @@ bool NonlinearExtension::modelBasedRefinement(
           << std::endl;
       // check the model based on simple solving of equalities and using
       // error bounds on the Taylor approximation of transcendental functions.
-      std::vector<Node> lemmas;
+      std::vector<NlLemma> lemmas;
       std::vector<Node> gs;
       if (checkModel(assertions, false_asserts, lemmas, gs))
       {
@@ -753,7 +747,7 @@ bool NonlinearExtension::modelBasedRefinement(
         complete_status = -1;
         if (!shared_term_value_splits.empty())
         {
-          std::vector<Node> stvLemmas;
+          std::vector<NlLemma> stvLemmas;
           for (const Node& eq : shared_term_value_splits)
           {
             Node req = Rewriter::rewrite(eq);
@@ -814,12 +808,10 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel)
   d_model.reset(d_containing.getValuation().getModel(), arithModel);
   // run a last call effort check
   d_cmiLemmas.clear();
-  d_cmiLemmasPp.clear();
-  d_cmiLemmasSE.clear();
   if (!d_builtModel.get())
   {
     Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
-    modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp, d_cmiLemmasSE);
+    modelBasedRefinement(d_cmiLemmas);
   }
   if (d_builtModel.get())
   {
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 855310daa..5cf2eb84b 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -147,8 +147,8 @@ class NonlinearExtension
    * involve e.g. solving for variables in nonlinear equations.
    *
    * Notice that in the former case, the lemmas it constructs are not sent out
-   * immediately. Instead, they are put in temporary vectors d_cmiLemmas
-   * and d_cmiLemmasPp, which are then sent out (if necessary) when a last call
+   * immediately. Instead, they are put in temporary vector d_cmiLemmas, which
+   * are then sent out (if necessary) when a last call
    * effort check is issued to this class.
    */
   void interceptModel(std::map<Node, Node>& arithModel);
@@ -173,17 +173,12 @@ class NonlinearExtension
    * described in Reynolds et al. FroCoS 2017 that are based on ruling out
    * the current candidate model.
    *
-   * This function returns true if a lemma was added to the vector lems/lemsPp.
+   * This function returns true if a lemma was added to the vector lems.
    * Otherwise, it returns false. In the latter case, the model object d_model
    * may have information regarding how to construct a model, in the case that
    * we determined the problem is satisfiable.
-   *
-   * The argument lemSE is the "side effect" of the lemmas in mlems and mlemsPp
-   * (for details, see checkLastCall).
    */
-  bool modelBasedRefinement(std::vector<Node>& mlems,
-                            std::vector<Node>& mlemsPp,
-                            std::map<Node, NlLemmaSideEffect>& lemSE);
+  bool modelBasedRefinement(std::vector<NlLemma>& mlems);
 
   /** check last call
    *
@@ -192,32 +187,24 @@ class NonlinearExtension
    *
    * xts : the list of (non-reduced) extended terms in the current context.
    *
-   * This method adds lemmas to arguments lems, lemsPp, and wlems, each of
+   * This method adds lemmas to arguments lems and wlems, each of
    * which are intended to be sent out on the output channel of TheoryArith
    * under certain conditions.
    *
-   * If the set lems or lemsPp is non-empty, then no further processing is
+   * If the set lems is non-empty, then no further processing is
    * necessary. The last call effort check should terminate and these
-   * lemmas should be sent. The set lemsPp is distinguished from lems since
-   * the preprocess flag on the lemma(...) call should be set to true.
+   * lemmas should be sent.
    *
    * The "waiting" lemmas wlems contain lemmas that should be sent on the
    * output channel as a last resort. In other words, only if we are not
    * able to establish SAT via a call to checkModel(...) should wlems be
    * considered. This set typically contains tangent plane lemmas.
-   *
-   * The argument lemSE is the "side effect" of the lemmas from the previous
-   * three calls. If a lemma is mapping to a side effect, it should be
-   * processed via a call to processSideEffect(...) immediately after the
-   * lemma is sent (if it is indeed sent on this call to check).
    */
   int checkLastCall(const std::vector<Node>& assertions,
                     const std::vector<Node>& false_asserts,
                     const std::vector<Node>& xts,
-                    std::vector<Node>& lems,
-                    std::vector<Node>& lemsPp,
-                    std::vector<Node>& wlems,
-                    std::map<Node, NlLemmaSideEffect>& lemSE);
+                    std::vector<NlLemma>& lems,
+                    std::vector<NlLemma>& wlems);
 
   /** get assertions
    *
@@ -259,7 +246,7 @@ class NonlinearExtension
    */
   bool checkModel(const std::vector<Node>& assertions,
                   const std::vector<Node>& false_asserts,
-                  std::vector<Node>& lemmas,
+                  std::vector<NlLemma>& lemmas,
                   std::vector<Node>& gs);
   //---------------------------end check model
 
@@ -271,21 +258,22 @@ class NonlinearExtension
    * the number of lemmas added to out. We do not add lemmas that have already
    * been sent on the output channel of TheoryArith.
    */
-  unsigned filterLemmas(std::vector<Node>& lemmas, std::vector<Node>& out);
+  unsigned filterLemmas(std::vector<NlLemma>& lemmas,
+                        std::vector<NlLemma>& out);
   /** singleton version of above */
-  unsigned filterLemma(Node lem, std::vector<Node>& out);
+  unsigned filterLemma(NlLemma lem, std::vector<NlLemma>& out);
 
   /**
    * Send lemmas in out on the output channel of theory of arithmetic.
    */
-  void sendLemmas(const std::vector<Node>& out,
-                  bool preprocess,
-                  std::map<Node, NlLemmaSideEffect>& lemSE);
+  void sendLemmas(const std::vector<NlLemma>& out);
   /** Process side effect se */
-  void processSideEffect(const NlLemmaSideEffect& se);
+  void processSideEffect(const NlLemma& se);
 
   /** 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;
@@ -316,14 +304,10 @@ class NonlinearExtension
    */
   NlSolver d_nlSlv;
   /**
-   * The lemmas we computed during collectModelInfo. We store two vectors of
-   * lemmas to be sent out on the output channel of TheoryArith. The first
-   * is not preprocessed, the second is.
+   * The lemmas we computed during collectModelInfo, to be sent out on the
+   * output channel of TheoryArith.
    */
-  std::vector<Node> d_cmiLemmas;
-  std::vector<Node> d_cmiLemmasPp;
-  /** the side effects of the above lemmas */
-  std::map<Node, NlLemmaSideEffect> d_cmiLemmasSE;
+  std::vector<NlLemma> d_cmiLemmas;
   /**
    * The approximations computed during collectModelInfo. For details, see
    * NlModel::getModelValueRepair.
diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp
index 3e10f6397..3b5bdb17f 100644
--- a/src/theory/arith/nl/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental_solver.cpp
@@ -50,8 +50,7 @@ TranscendentalSolver::~TranscendentalSolver() {}
 void TranscendentalSolver::initLastCall(const std::vector<Node>& assertions,
                                         const std::vector<Node>& false_asserts,
                                         const std::vector<Node>& xts,
-                                        std::vector<Node>& lems,
-                                        std::vector<Node>& lemsPp)
+                                        std::vector<NlLemma>& lems)
 {
   d_funcCongClass.clear();
   d_funcMap.clear();
@@ -213,7 +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;
-    lemsPp.push_back(lem);
+    NlLemma nlem(lem);
+    nlem.d_preprocess = true;
+    lems.push_back(nlem);
   }
 
   if (Trace.isOn("nl-ext-mv"))
@@ -333,7 +334,7 @@ unsigned TranscendentalSolver::getTaylorDegree() const
   return d_taylor_degree;
 }
 
-void TranscendentalSolver::processSideEffect(const NlLemmaSideEffect& se)
+void TranscendentalSolver::processSideEffect(const NlLemma& se)
 {
   for (const std::tuple<Node, unsigned, Node>& sp : se.d_secantPoint)
   {
@@ -362,7 +363,7 @@ void TranscendentalSolver::mkPi()
   }
 }
 
-void TranscendentalSolver::getCurrentPiBounds(std::vector<Node>& lemmas)
+void TranscendentalSolver::getCurrentPiBounds(std::vector<NlLemma>& lemmas)
 {
   NodeManager* nm = NodeManager::currentNM();
   Node pi_lem = nm->mkNode(AND,
@@ -371,10 +372,10 @@ void TranscendentalSolver::getCurrentPiBounds(std::vector<Node>& lemmas)
   lemmas.push_back(pi_lem);
 }
 
-std::vector<Node> TranscendentalSolver::checkTranscendentalInitialRefine()
+std::vector<NlLemma> TranscendentalSolver::checkTranscendentalInitialRefine()
 {
   NodeManager* nm = NodeManager::currentNM();
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   Trace("nl-ext")
       << "Get initial refinement lemmas for transcendental functions..."
       << std::endl;
@@ -462,9 +463,9 @@ std::vector<Node> TranscendentalSolver::checkTranscendentalInitialRefine()
   return lemmas;
 }
 
-std::vector<Node> TranscendentalSolver::checkTranscendentalMonotonic()
+std::vector<NlLemma> TranscendentalSolver::checkTranscendentalMonotonic()
 {
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..."
                   << std::endl;
 
@@ -644,10 +645,9 @@ std::vector<Node> TranscendentalSolver::checkTranscendentalMonotonic()
   return lemmas;
 }
 
-std::vector<Node> TranscendentalSolver::checkTranscendentalTangentPlanes(
-    std::map<Node, NlLemmaSideEffect>& lemSE)
+std::vector<NlLemma> TranscendentalSolver::checkTranscendentalTangentPlanes()
 {
-  std::vector<Node> lemmas;
+  std::vector<NlLemma> lemmas;
   Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..."
                   << std::endl;
   // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
@@ -683,7 +683,7 @@ std::vector<Node> TranscendentalSolver::checkTranscendentalTangentPlanes(
       {
         Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
         unsigned prev = lemmas.size();
-        if (checkTfTangentPlanesFun(tf, d, lemmas, lemSE))
+        if (checkTfTangentPlanesFun(tf, d, lemmas))
         {
           Trace("nl-ext-tftp")
               << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl;
@@ -700,11 +700,9 @@ std::vector<Node> TranscendentalSolver::checkTranscendentalTangentPlanes(
   return lemmas;
 }
 
-bool TranscendentalSolver::checkTfTangentPlanesFun(
-    Node tf,
-    unsigned d,
-    std::vector<Node>& lemmas,
-    std::map<Node, NlLemmaSideEffect>& lemSE)
+bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf,
+                                                   unsigned d,
+                                                   std::vector<NlLemma>& lemmas)
 {
   NodeManager* nm = NodeManager::currentNM();
   Kind k = tf.getKind();
@@ -1020,10 +1018,11 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(
     Assert(!lemmaConj.empty());
     Node lem =
         lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj);
-    lemmas.push_back(lem);
+    NlLemma nlem(lem);
     // The side effect says that if lem is added, then we should add the
     // secant point c for (tf,d).
-    lemSE[lem].d_secantPoint.push_back(std::make_tuple(tf, d, c));
+    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
+    lemmas.push_back(nlem);
   }
   return true;
 }
diff --git a/src/theory/arith/nl/transcendental_solver.h b/src/theory/arith/nl/transcendental_solver.h
index 5cd57d8fa..0285b49e3 100644
--- a/src/theory/arith/nl/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental_solver.h
@@ -55,14 +55,13 @@ class TranscendentalSolver
    * model, and xts is the set of extended function terms that are active in
    * the current context.
    *
-   * This call may add lemmas to lems/lemsPp based on registering term
+   * This call may add lemmas to lems based on registering term
    * information (for example, purification of sine terms).
    */
   void initLastCall(const std::vector<Node>& assertions,
                     const std::vector<Node>& false_asserts,
                     const std::vector<Node>& xts,
-                    std::vector<Node>& lems,
-                    std::vector<Node>& lemsPp);
+                    std::vector<NlLemma>& lems);
   /** increment taylor degree */
   void incrementTaylorDegree();
   /** get taylor degree */
@@ -76,8 +75,8 @@ class TranscendentalSolver
    * was conflicting.
    */
   bool preprocessAssertionsCheckModel(std::vector<Node>& assertions);
-  /** Process side effect se */
-  void processSideEffect(const NlLemmaSideEffect& se);
+  /** Process side effects in lemma se */
+  void processSideEffect(const NlLemma& se);
   //-------------------------------------------- lemma schemas
   /** check transcendental initial refine
    *
@@ -95,7 +94,7 @@ class TranscendentalSolver
    * exp( x )>0
    * x<0 => exp( x )<1
    */
-  std::vector<Node> checkTranscendentalInitialRefine();
+  std::vector<NlLemma> checkTranscendentalInitialRefine();
 
   /** check transcendental monotonic
    *
@@ -109,7 +108,7 @@ class TranscendentalSolver
    * PI/2 > x > y > 0 => sin( x ) > sin( y )
    * PI > x > y > PI/2 => sin( x ) < sin( y )
    */
-  std::vector<Node> checkTranscendentalMonotonic();
+  std::vector<NlLemma> checkTranscendentalMonotonic();
 
   /** check transcendental tangent planes
    *
@@ -168,12 +167,8 @@ class TranscendentalSolver
    *   ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2)
    *     where c1, c2 are rationals (for brevity, omitted here)
    *     such that c1 ~= .277 and c2 ~= 2.032.
-   *
-   * The argument lemSE is the "side effect" of the lemmas in the return
-   * value of this function (for details, see checkLastCall).
    */
-  std::vector<Node> checkTranscendentalTangentPlanes(
-      std::map<Node, NlLemmaSideEffect>& lemSE);
+  std::vector<NlLemma> checkTranscendentalTangentPlanes();
   /** check transcendental function refinement for tf
    *
    * This method is called by the above method for each "master"
@@ -185,16 +180,13 @@ class TranscendentalSolver
    *
    * This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental
    * function application tf for Taylor degree d. It may add a secant or
-   * tangent plane lemma to lems and its side effect (if one exists)
-   * to lemSE.
+   * tangent plane lemma to lems, which includes the side effect of the lemma
+   * (if one exists).
    *
    * It returns false if the bounds are not precise enough to add a
    * secant or tangent plane lemma.
    */
-  bool checkTfTangentPlanesFun(Node tf,
-                               unsigned d,
-                               std::vector<Node>& lems,
-                               std::map<Node, NlLemmaSideEffect>& lemSE);
+  bool checkTfTangentPlanesFun(Node tf, unsigned d, std::vector<NlLemma>& lems);
   //-------------------------------------------- end lemma schemas
  private:
   /** polynomial approximation bounds
@@ -276,7 +268,7 @@ class TranscendentalSolver
   Node getDerivative(Node n, Node x);
 
   void mkPi();
-  void getCurrentPiBounds(std::vector<Node>& lemmas);
+  void getCurrentPiBounds(std::vector<NlLemma>& lemmas);
   /** Make the node -pi <= a <= pi */
   static Node mkValidPhase(Node a, Node pi);