(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)

Due to recent simplifications in the internal calculus, we will no longer reason about WITNESS terms in conclusions of ProofNode, instead WITNESS terms will only be for bookkeeping.This means that some implementations of ppRewrite must change to return SKOLEM instead of WITNESS terms.

Since witness terms are currently used as a way of specifying "replace t by skolem k, and send a lemma about k", a followup PR will update Theory::ppRewrite to take an additional argument std::vector<SkolemLemma>& lems where new lemmas must be explicitly added to a vector (instead of encoded as witness). Then, all Theory::ppRewrite will return skolems instead of witness terms.

This PR changes arithmetic in preparation for this change.

Notice that I'm introducing SkolemLemma in this PR, which is a very common pattern that can simplify some of our interfaces, e.g. see https://github.com/CVC4/CVC4/blob/master/src/smt/term_formula_removal.h#L93, https://github.com/CVC4/CVC4/blob/master/src/prop/prop_engine.h#L94.

Note that the indentation of code in operator_elim.cpp changed.

10 files changed, 316 insertions, 236 deletions

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 26f51c8b8..f4f9df43c 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -27,10 +27,13 @@ ArithPreprocess::ArithPreprocess(ArithState& state,
     : d_im(im), d_opElim(pnm, info), d_reduced(state.getUserContext())
 {
 }
-TrustNode ArithPreprocess::eliminate(TNode n, bool partialOnly)
+TrustNode ArithPreprocess::eliminate(TNode n,
+                                     std::vector<SkolemLemma>& lems,
+                                     bool partialOnly)
 {
-  return d_opElim.eliminate(n, partialOnly);
+  return d_opElim.eliminate(n, lems, partialOnly);
 }
+
 bool ArithPreprocess::reduceAssertion(TNode atom)
 {
   context::CDHashMap<Node, bool, NodeHashFunction>::const_iterator it =
@@ -40,7 +43,12 @@ bool ArithPreprocess::reduceAssertion(TNode atom)
     // already computed
     return (*it).second;
   }
-  TrustNode tn = eliminate(atom);
+  std::vector<SkolemLemma> lems;
+  TrustNode tn = eliminate(atom, lems);
+  for (const SkolemLemma& lem : lems)
+  {
+    d_im.trustedLemma(lem.d_lemma, InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA);
+  }
   if (tn.isNull())
   {
     // did not reduce
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 622357e73..e1f43db1b 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -22,6 +22,7 @@
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/logic_info.h"
+#include "theory/skolem_lemma.h"
 
 namespace CVC4 {
 namespace theory {
@@ -52,7 +53,9 @@ class ArithPreprocess
    * @return the trust node proving (= n nr) where nr is the return of
    * eliminating operators in n, or the null trust node if n was unchanged.
    */
-  TrustNode eliminate(TNode n, bool partialOnly = false);
+  TrustNode eliminate(TNode n,
+                      std::vector<SkolemLemma>& lems,
+                      bool partialOnly = false);
   /**
    * Reduce assertion. This sends a lemma via the inference manager if atom
    * contains any extended operators. When applicable, the lemma is of the form:
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index e34c0110e..8aaab3f69 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/arith/operator_elim.h"
 
+#include "expr/attribute.h"
+#include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
 #include "options/arith_options.h"
 #include "smt/logic_exception.h"
@@ -27,6 +29,31 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+/**
+ * Attribute used for constructing unique bound variables that are binders
+ * for witness terms below. In other words, this attribute maps nodes to
+ * the bound variable of a witness term for eliminating that node.
+ *
+ * Notice we use the same attribute for most bound variables below, since using
+ * a node itself is a sufficient cache key for constructing a bound variable.
+ * The exception is to_int / is_int, which share a skolem based on their
+ * argument.
+ */
+struct ArithWitnessVarAttributeId
+{
+};
+using ArithWitnessVarAttribute = expr::Attribute<ArithWitnessVarAttributeId, Node>;
+/**
+ * Similar to above, shared for to_int and is_int. This is used for introducing
+ * an integer bound variable used to construct the witness term for t in the
+ * contexts (to_int t) and (is_int t).
+ */
+struct ToIntWitnessVarAttributeId
+{
+};
+using ToIntWitnessVarAttribute
+ = expr::Attribute<ToIntWitnessVarAttributeId, Node>;
+
 OperatorElim::OperatorElim(ProofNodeManager* pnm, const LogicInfo& info)
     : EagerProofGenerator(pnm), d_info(info)
 {
@@ -46,10 +73,12 @@ void OperatorElim::checkNonLinearLogic(Node term)
   }
 }
 
-TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
+TrustNode OperatorElim::eliminate(Node n,
+                                  std::vector<SkolemLemma>& lems,
+                                  bool partialOnly)
 {
   TConvProofGenerator* tg = nullptr;
-  Node nn = eliminateOperators(n, tg, partialOnly);
+  Node nn = eliminateOperators(n, lems, tg, partialOnly);
   if (nn != n)
   {
     return TrustNode::mkTrustRewrite(n, nn, nullptr);
@@ -58,10 +87,12 @@ TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
 }
 
 Node OperatorElim::eliminateOperators(Node node,
+                                      std::vector<SkolemLemma>& lems,
                                       TConvProofGenerator* tg,
                                       bool partialOnly)
 {
   NodeManager* nm = NodeManager::currentNM();
+  BoundVarManager* bvm = nm->getBoundVarManager();
   Kind k = node.getKind();
   switch (k)
   {
@@ -82,26 +113,21 @@ Node OperatorElim::eliminateOperators(Node node,
         // not eliminating total operators
         return node;
       }
-      Node toIntSkolem;
-      std::map<Node, Node>::const_iterator it = d_to_int_skolem.find(node[0]);
-      if (it == d_to_int_skolem.end())
-      {
-        // node[0] - 1 < toIntSkolem <= node[0]
-        // -1 < toIntSkolem - node[0] <= 0
-        // 0 <= node[0] - toIntSkolem < 1
-        Node v = nm->mkBoundVar(nm->integerType());
-        Node one = mkRationalNode(1);
-        Node zero = mkRationalNode(0);
-        Node diff = nm->mkNode(MINUS, node[0], v);
-        Node lem = mkInRange(diff, zero, one);
-        toIntSkolem = mkWitnessTerm(
-            v, lem, "toInt", "a conversion of a Real term to its Integer part");
-        d_to_int_skolem[node[0]] = toIntSkolem;
-      }
-      else
-      {
-        toIntSkolem = (*it).second;
-      }
+      // node[0] - 1 < toIntSkolem <= node[0]
+      // -1 < toIntSkolem - node[0] <= 0
+      // 0 <= node[0] - toIntSkolem < 1
+      Node v =
+          bvm->mkBoundVar<ToIntWitnessVarAttribute>(node[0], nm->integerType());
+      Node one = mkRationalNode(1);
+      Node zero = mkRationalNode(0);
+      Node diff = nm->mkNode(MINUS, node[0], v);
+      Node lem = mkInRange(diff, zero, one);
+      Node toIntSkolem =
+          mkWitnessTerm(v,
+                        lem,
+                        "toInt",
+                        "a conversion of a Real term to its Integer part",
+                        lems);
       if (k == IS_INTEGER)
       {
         return nm->mkNode(EQUAL, node[0], toIntSkolem);
@@ -120,89 +146,77 @@ Node OperatorElim::eliminateOperators(Node node,
       }
       Node den = Rewriter::rewrite(node[1]);
       Node num = Rewriter::rewrite(node[0]);
-      Node intVar;
       Node rw = nm->mkNode(k, num, den);
-      std::map<Node, Node>::const_iterator it = d_int_div_skolem.find(rw);
-      if (it == d_int_div_skolem.end())
+      Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->integerType());
+      Node lem;
+      Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
+      if (den.isConst())
       {
-        Node v = nm->mkBoundVar(nm->integerType());
-        Node lem;
-        Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
-        if (den.isConst())
+        const Rational& rat = den.getConst<Rational>();
+        if (num.isConst() || rat == 0)
         {
-          const Rational& rat = den.getConst<Rational>();
-          if (num.isConst() || rat == 0)
-          {
-            // just rewrite
-            return Rewriter::rewrite(node);
-          }
-          if (rat > 0)
-          {
-            lem = nm->mkNode(
-                AND,
-                leqNum,
-                nm->mkNode(
-                    LT,
-                    num,
-                    nm->mkNode(MULT,
-                               den,
-                               nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
-          }
-          else
-          {
-            lem = nm->mkNode(
-                AND,
-                leqNum,
-                nm->mkNode(
-                    LT,
-                    num,
-                    nm->mkNode(
-                        MULT,
-                        den,
-                        nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
-          }
+          // just rewrite
+          return Rewriter::rewrite(node);
         }
-        else
+        if (rat > 0)
         {
-          checkNonLinearLogic(node);
           lem = nm->mkNode(
               AND,
+              leqNum,
               nm->mkNode(
-                  IMPLIES,
-                  nm->mkNode(GT, den, nm->mkConst(Rational(0))),
-                  nm->mkNode(
-                      AND,
-                      leqNum,
-                      nm->mkNode(
-                          LT,
-                          num,
-                          nm->mkNode(
-                              MULT,
-                              den,
-                              nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
+                  LT,
+                  num,
+                  nm->mkNode(MULT,
+                             den,
+                             nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
+        }
+        else
+        {
+          lem = nm->mkNode(
+              AND,
+              leqNum,
               nm->mkNode(
-                  IMPLIES,
-                  nm->mkNode(LT, den, nm->mkConst(Rational(0))),
-                  nm->mkNode(
-                      AND,
-                      leqNum,
-                      nm->mkNode(
-                          LT,
-                          num,
-                          nm->mkNode(
-                              MULT,
-                              den,
-                              nm->mkNode(
-                                  PLUS, v, nm->mkConst(Rational(-1))))))));
+                  LT,
+                  num,
+                  nm->mkNode(MULT,
+                             den,
+                             nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
         }
-        intVar = mkWitnessTerm(
-            v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
-        d_int_div_skolem[rw] = intVar;
       }
       else
       {
-        intVar = (*it).second;
+        checkNonLinearLogic(node);
+        lem = nm->mkNode(
+            AND,
+            nm->mkNode(
+                IMPLIES,
+                nm->mkNode(GT, den, nm->mkConst(Rational(0))),
+                nm->mkNode(
+                    AND,
+                    leqNum,
+                    nm->mkNode(
+                        LT,
+                        num,
+                        nm->mkNode(
+                            MULT,
+                            den,
+                            nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
+            nm->mkNode(
+                IMPLIES,
+                nm->mkNode(LT, den, nm->mkConst(Rational(0))),
+                nm->mkNode(
+                    AND,
+                    leqNum,
+                    nm->mkNode(
+                        LT,
+                        num,
+                        nm->mkNode(
+                            MULT,
+                            den,
+                            nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))))));
       }
+      Node intVar = mkWitnessTerm(
+          v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
       if (k == INTS_MODULUS_TOTAL)
       {
         Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
@@ -231,24 +245,13 @@ Node OperatorElim::eliminateOperators(Node node,
         return node;
       }
       checkNonLinearLogic(node);
-      Node var;
       Node rw = nm->mkNode(k, num, den);
-      std::map<Node, Node>::const_iterator it = d_div_skolem.find(rw);
-      if (it == d_div_skolem.end())
-      {
-        Node v = nm->mkBoundVar(nm->realType());
-        Node lem = nm->mkNode(IMPLIES,
-                              den.eqNode(nm->mkConst(Rational(0))).negate(),
-                              nm->mkNode(MULT, den, v).eqNode(num));
-        var = mkWitnessTerm(
-            v, lem, "nonlinearDiv", "the result of a non-linear div term");
-        d_div_skolem[rw] = var;
-      }
-      else
-      {
-        var = (*it).second;
-      }
-      return var;
+      Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->realType());
+      Node lem = nm->mkNode(IMPLIES,
+                            den.eqNode(nm->mkConst(Rational(0))).negate(),
+                            nm->mkNode(MULT, den, v).eqNode(num));
+      return mkWitnessTerm(
+          v, lem, "nonlinearDiv", "the result of a non-linear div term", lems);
       break;
     }
     case DIVISION:
@@ -325,79 +328,72 @@ Node OperatorElim::eliminateOperators(Node node,
       }
       checkNonLinearLogic(node);
       // eliminate inverse functions here
-      std::map<Node, Node>::const_iterator it =
-          d_nlin_inverse_skolem.find(node);
-      if (it == d_nlin_inverse_skolem.end())
+      Node var =
+          bvm->mkBoundVar<ArithWitnessVarAttribute>(node, nm->realType());
+      Node lem;
+      if (k == SQRT)
       {
-        Node var = nm->mkBoundVar(nm->realType());
-        Node lem;
-        if (k == SQRT)
-        {
-          Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
-          Node uf = skolemApp.eqNode(var);
-          Node nonNeg =
-              nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
+        Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
+        Node uf = skolemApp.eqNode(var);
+        Node nonNeg =
+            nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
+
+        // sqrt(x) reduces to:
+        // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
+        //
+        // Uf(x) makes sure that the reduction still behaves like a function,
+        // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
+        // satisfiable. On the original formula, this would require that we
+        // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
+        // model.
+        lem = nm->mkNode(ITE,
+                         nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
+                         nonNeg,
+                         uf);
+      }
+      else
+      {
+        Node pi = mkPi();
 
-          // sqrt(x) reduces to:
-          // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
-          //
-          // Uf(x) makes sure that the reduction still behaves like a function,
-          // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
-          // satisfiable. On the original formula, this would require that we
-          // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
-          // model.
-          lem = nm->mkNode(ITE,
-                           nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
-                           nonNeg,
-                           uf);
+        // range of the skolem
+        Node rlem;
+        if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
+        {
+          Node half = nm->mkConst(Rational(1) / Rational(2));
+          Node pi2 = nm->mkNode(MULT, half, pi);
+          Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
+          // -pi/2 < var <= pi/2
+          rlem = nm->mkNode(
+              AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
         }
         else
         {
-          Node pi = mkPi();
-
-          // range of the skolem
-          Node rlem;
-          if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
-          {
-            Node half = nm->mkConst(Rational(1) / Rational(2));
-            Node pi2 = nm->mkNode(MULT, half, pi);
-            Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
-            // -pi/2 < var <= pi/2
-            rlem = nm->mkNode(
-                AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
-          }
-          else
-          {
-            // 0 <= var < pi
-            rlem = nm->mkNode(AND,
-                              nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
-                              nm->mkNode(LT, var, pi));
-          }
-
-          Kind rk = k == ARCSINE
-                        ? SINE
-                        : (k == ARCCOSINE
-                               ? COSINE
-                               : (k == ARCTANGENT
-                                      ? TANGENT
-                                      : (k == ARCCOSECANT
-                                             ? COSECANT
-                                             : (k == ARCSECANT ? SECANT
-                                                               : COTANGENT))));
-          Node invTerm = nm->mkNode(rk, var);
-          lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
+          // 0 <= var < pi
+          rlem = nm->mkNode(AND,
+                            nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
+                            nm->mkNode(LT, var, pi));
         }
-        Assert(!lem.isNull());
-        Node ret = mkWitnessTerm(
-            var,
-            lem,
-            "tfk",
-            "Skolem to eliminate a non-standard transcendental function");
-        Assert(ret.getKind() == WITNESS);
-        d_nlin_inverse_skolem[node] = ret;
-        return ret;
+
+        Kind rk =
+            k == ARCSINE
+                ? SINE
+                : (k == ARCCOSINE
+                       ? COSINE
+                       : (k == ARCTANGENT
+                              ? TANGENT
+                              : (k == ARCCOSECANT
+                                     ? COSECANT
+                                     : (k == ARCSECANT ? SECANT : COTANGENT))));
+        Node invTerm = nm->mkNode(rk, var);
+        lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
       }
-      return (*it).second;
+      Assert(!lem.isNull());
+      return mkWitnessTerm(
+          var,
+          lem,
+          "tfk",
+          "Skolem to eliminate a non-standard transcendental function",
+          lems);
       break;
     }
 
@@ -476,12 +472,15 @@ Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
 Node OperatorElim::mkWitnessTerm(Node v,
                                  Node pred,
                                  const std::string& prefix,
-                                 const std::string& comment)
+                                 const std::string& comment,
+                                 std::vector<SkolemLemma>& lems)
 {
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
+  // we mark that we should send a lemma
   Node k = sm->mkSkolem(
       v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this, true);
+  // TODO: (project #37) add to lems
   return k;
 }
 
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index cf5b9248c..49638d9fb 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -20,6 +20,7 @@
 #include "expr/term_conversion_proof_generator.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/logic_info.h"
+#include "theory/skolem_lemma.h"
 
 namespace CVC4 {
 namespace theory {
@@ -31,13 +32,22 @@ class OperatorElim : public EagerProofGenerator
   OperatorElim(ProofNodeManager* pnm, const LogicInfo& info);
   ~OperatorElim() {}
   /** Eliminate operators in this term.
-    *
-    * Eliminate operators in term n. If n has top symbol that is not a core
-    * one (including division, int division, mod, to_int, is_int, syntactic sugar
-    * transcendental functions), then we replace it by a form that eliminates
-    * that operator. This may involve the introduction of witness terms.
-    */
-  TrustNode eliminate(Node n, bool partialOnly = false);
+   *
+   * Eliminate operators in term n. If n has top symbol that is not a core
+   * one (including division, int division, mod, to_int, is_int, syntactic sugar
+   * transcendental functions), then we replace it by a form that eliminates
+   * that operator. This may involve the introduction of witness terms.
+   *
+   * @param n The node to eliminate
+   * @param lems The lemmas that we wish to add concerning n. It is the
+   * responsbility of the caller to process these lemmas.
+   * @param partialOnly Whether we only want to eliminate partial operators.
+   * @return the trust node of kind REWRITE encapsulating the eliminated form
+   * of n and a proof generator for proving this equivalence.
+   */
+  TrustNode eliminate(Node n,
+                      std::vector<SkolemLemma>& lems,
+                      bool partialOnly = false);
   /**
    * Get axiom for term n. This returns the axiom that this class uses to
    * eliminate the term n, which is determined by its top-most symbol.
@@ -48,15 +58,6 @@ class OperatorElim : public EagerProofGenerator
   /** Logic info of the owner of this class */
   const LogicInfo& d_info;
 
-  /**
-   *  Maps for Skolems for to-integer, real/integer div-by-k, and inverse
-   *  non-linear operators that are introduced during ppRewriteTerms.
-   */
-  std::map<Node, Node> d_to_int_skolem;
-  std::map<Node, Node> d_div_skolem;
-  std::map<Node, Node> d_int_div_skolem;
-  std::map<Node, Node> d_nlin_inverse_skolem;
-
   /** Arithmetic skolem identifier */
   enum class ArithSkolemId
   {
@@ -101,7 +102,10 @@ class OperatorElim : public EagerProofGenerator
    * @param n The node to eliminate operators from.
    * @return The (single step) eliminated form of n.
    */
-  Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly);
+  Node eliminateOperators(Node n,
+                          std::vector<SkolemLemma>& lems,
+                          TConvProofGenerator* tg,
+                          bool partialOnly);
   /** get arithmetic skolem
    *
    * Returns the Skolem in the above map for the given id, creating it if it
@@ -115,7 +119,8 @@ class OperatorElim : public EagerProofGenerator
   Node mkWitnessTerm(Node v,
                      Node pred,
                      const std::string& prefix,
-                     const std::string& comment);
+                     const std::string& comment,
+                     std::vector<SkolemLemma>& lems);
   /** get arithmetic skolem application
    *
    * By default, this returns the term f( n ), where f is the Skolem function
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 9bca5e182..2638fa3ae 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -102,7 +102,10 @@ void TheoryArith::preRegisterTerm(TNode n)
 TrustNode TheoryArith::expandDefinition(Node node)
 {
   // call eliminate operators, to eliminate partial operators only
-  return d_arithPreproc.eliminate(node, true);
+  std::vector<SkolemLemma> lems;
+  TrustNode ret = d_arithPreproc.eliminate(node, lems, true);
+  Assert(lems.empty());
+  return ret;
 }
 
 void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
@@ -112,43 +115,44 @@ TrustNode TheoryArith::ppRewrite(TNode atom)
   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
-  if (options::arithRewriteEq())
+  if (atom.getKind() == kind::EQUAL)
   {
-    if (atom.getKind() == kind::EQUAL)
-    {
-      Assert(atom[0].getType().isReal());
-      Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
-      Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
-      Node rewritten = Rewriter::rewrite(leq.andNode(geq));
-      Debug("arith::preprocess")
-          << "arith::preprocess() : returning " << rewritten << endl;
-      // don't need to rewrite terms since rewritten is not a non-standard op
-      if (proofsEnabled())
-      {
-        return d_ppPfGen.mkTrustedRewrite(
-            atom,
-            rewritten,
-            d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
-      }
-      else
-      {
-        return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
-      }
-    }
+    return ppRewriteEq(atom);
   }
-  return ppRewriteTerms(atom);
-}
-
-TrustNode TheoryArith::ppRewriteTerms(TNode n)
-{
-  Assert(Theory::theoryOf(n) == THEORY_ARITH);
-  // Eliminate operators recursively. Notice we must do this here since other
+  // TODO (project #37): this will be passed to ppRewrite
+  std::vector<SkolemLemma> lems;
+  Assert(Theory::theoryOf(atom) == THEORY_ARITH);
+  // Eliminate operators. Notice we must do this here since other
   // theories may generate lemmas that involve non-standard operators. For
   // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
   // introduce non-standard arithmetic terms appearing in grammars.
   // call eliminate operators. In contrast to expandDefinitions, we eliminate
   // *all* extended arithmetic operators here, including total ones.
-  return d_arithPreproc.eliminate(n, false);
+  return d_arithPreproc.eliminate(atom, lems, false);
+}
+
+TrustNode TheoryArith::ppRewriteEq(TNode atom)
+{
+  Assert(atom.getKind() == kind::EQUAL);
+  if (!options::arithRewriteEq())
+  {
+    return TrustNode::null();
+  }
+  Assert(atom[0].getType().isReal());
+  Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
+  Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+  Node rewritten = Rewriter::rewrite(leq.andNode(geq));
+  Debug("arith::preprocess")
+      << "arith::preprocess() : returning " << rewritten << endl;
+  // don't need to rewrite terms since rewritten is not a non-standard op
+  if (proofsEnabled())
+  {
+    return d_ppPfGen.mkTrustedRewrite(
+        atom,
+        rewritten,
+        d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
+  }
+  return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
 }
 
 Theory::PPAssertStatus TheoryArith::ppAssert(
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index f3344cbda..eb53687ff 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -112,6 +112,14 @@ class TheoryArith : public Theory {
   void notifyRestart() override;
   PPAssertStatus ppAssert(TrustNode tin,
                           TrustSubstitutionMap& outSubstitutions) override;
+  /**
+   * Preprocess rewrite terms, return the trust node encapsulating the
+   * preprocessed form of n, and the proof generator that can provide the
+   * proof for the equivalence of n and this term.
+   *
+   * This calls the operator elimination utility to eliminate extended
+   * symbols.
+   */
   TrustNode ppRewrite(TNode atom) override;
   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 
@@ -133,14 +141,10 @@ class TheoryArith : public Theory {
 
  private:
   /**
-   * Preprocess rewrite terms, return the trust node encapsulating the
-   * preprocessed form of n, and the proof generator that can provide the
-   * proof for the equivalence of n and this term.
-   *
-   * This calls the operator elimination utility to eliminate extended
-   * symbols.
+   * Preprocess equality, applies ppRewrite for equalities. This method is
+   * distinct from ppRewrite since it is not allowed to construct lemmas.
    */
-  TrustNode ppRewriteTerms(TNode n);
+  TrustNode ppRewriteEq(TNode eq);
   /** Get the proof equality engine */
   eq::ProofEqEngine* getProofEqEngine();
   /** The state object wrapping TheoryArithPrivate  */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 40bd81795..940e04013 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3757,7 +3757,7 @@ TrustNode TheoryArithPrivate::branchIntegerVariable(ArithVar x) const
     TrustNode teq;
     if (Theory::theoryOf(eq) == THEORY_ARITH)
     {
-      teq = d_containing.ppRewrite(eq);
+      teq = d_containing.ppRewriteEq(eq);
       eq = teq.isNull() ? eq : teq.getNode();
     }
     Node literal = d_containing.getValuation().ensureLiteral(eq);
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 94f90bc46..822f79397 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -24,6 +24,8 @@ const char* toString(InferenceId i)
   switch (i)
   {
     case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS";
+    case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA:
+      return "ARITH_PP_ELIM_OPERATORS_LEMMA";
     case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE";
     case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT:
       return "ARITH_NL_SHARED_TERM_VALUE_SPLIT";
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 8a787ca2d..995cb1083 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -42,7 +42,10 @@ enum class InferenceId
 {
   // ---------------------------------- arith theory
   //-------------------- preprocessing
+  // equivalence of term and its preprocessed form
   ARITH_PP_ELIM_OPERATORS,
+  // a lemma from arithmetic preprocessing
+  ARITH_PP_ELIM_OPERATORS_LEMMA,
   //-------------------- nonlinear core
   // simple congruence x=y => f(x)=f(y)
   ARITH_NL_CONGRUENCE,
diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h
new file mode 100644
index 000000000..c900c818e
--- /dev/null
+++ b/src/theory/skolem_lemma.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file skolem_lemma.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 The skolem lemma utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__SKOLEM_LEMMA_H
+#define CVC4__THEORY__SKOLEM_LEMMA_H
+
+#include "expr/node.h"
+#include "theory/trust_node.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * A skolem lemma is a pair containing a trust node repreresenting a lemma
+ * and the skolem it is for. A common example would be the trust node proving
+ * the lemma:
+ *    (ite C (= k A) (= k B))
+ * and the skolem k.
+ *
+ * Skolem lemmas can be used as a way of tracking the relevance of a lemma.
+ * They can be used for things like term formula removal and preprocessing.
+ */
+class SkolemLemma
+{
+ public:
+  SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k)
+  {
+    Assert(lem.getKind() == TrustNodeKind::LEMMA);
+  }
+  /** The lemma, a trust node of kind LEMMA */
+  TrustNode d_lemma;
+  /** The skolem associated with that lemma */
+  Node d_skolem;
+};
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__SKOLEM_LEMMA_H */