(proof-new) Update ppRewrite to use skolem lemmas (#6102)

This is required for proofs. The internal calculus no longer uses witness forms for reasoning, and hence we cannot return witness terms in ppRewrite. This is required to fix a debug failure, as well as making life easier on external proof conversions.

As a result of this PR, for example, given (P a) as input to ppRewrite, previous we returned:

(P (witness ((x T)) (A x)))

now we return:

(P k), with skolem lemma ( (A k), k )

Followup PRs will remove the use of WITNESS in ppRewrite (e.g. in sets and strings); this PR modifies arithmetic to not return WITNESS in response to ppRewrite.

25 files changed, 104 insertions, 68 deletions

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 23ae919d3..c65180ed3 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -44,8 +44,7 @@ Node SkolemManager::mkSkolem(Node v,
                              const std::string& prefix,
                              const std::string& comment,
                              int flags,
-                             ProofGenerator* pg,
-                             bool retWitness)
+                             ProofGenerator* pg)
 {
   // We do not currently insist that pred does not contain witness terms
   Assert(v.getKind() == BOUND_VARIABLE);
@@ -72,11 +71,6 @@ Node SkolemManager::mkSkolem(Node v,
   k.setAttribute(wfa, w);
   Trace("sk-manager-skolem")
       << "skolem: " << k << " witness " << w << std::endl;
-  // if we want to return the witness term, make it
-  if (retWitness)
-  {
-    return nm->mkNode(WITNESS, bvl, pred);
-  }
   return k;
 }
 
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 1a78bfc83..1cb048cf2 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -107,12 +107,6 @@ class SkolemManager
    * @param pg The proof generator for this skolem. If non-null, this proof
    * generator must respond to a call to getProofFor(exists v. pred) during
    * the lifetime of the current node manager.
-   * @param retWitness Whether we wish to return the witness term for the
-   * given Skolem, which notice is of the form (witness v. pred), where pred
-   * is in Skolem form. A typical use case of setting this flag to true
-   * is preprocessing passes that eliminate terms. Using a witness term
-   * instead of its corresponding Skolem indicates that the body of the witness
-   * term needs to be added as an assertion, e.g. by the term formula remover.
    * @return The skolem whose witness form is registered by this class.
    */
   Node mkSkolem(Node v,
@@ -120,8 +114,7 @@ class SkolemManager
                 const std::string& prefix,
                 const std::string& comment = "",
                 int flags = NodeManager::SKOLEM_DEFAULT,
-                ProofGenerator* pg = nullptr,
-                bool retWitness = false);
+                ProofGenerator* pg = nullptr);
   /**
    * Make skolemized form of existentially quantified formula q, and store its
    * Skolems into the argument skolems.
diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index c6f961129..100116fd7 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -479,9 +479,21 @@ Node OperatorElim::mkWitnessTerm(Node v,
   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
+  Node k =
+      sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this);
+  TNode tv = v;
+  TNode tk = k;
+  Node lem = pred.substitute(tv, tk);
+  if (d_pnm != nullptr)
+  {
+    TrustNode tlem =
+        mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
+    lems.push_back(SkolemLemma(tlem, k));
+  }
+  else
+  {
+    lems.push_back(SkolemLemma(TrustNode::mkTrustLemma(lem), k));
+  }
   return k;
 }
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 937901c57..e3c4919a3 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -112,7 +112,7 @@ TrustNode TheoryArith::expandDefinition(Node node)
 
 void TheoryArith::notifySharedTerm(TNode n) { d_internal->notifySharedTerm(n); }
 
-TrustNode TheoryArith::ppRewrite(TNode atom)
+TrustNode TheoryArith::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
 {
   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
@@ -121,8 +121,6 @@ TrustNode TheoryArith::ppRewrite(TNode atom)
   {
     return ppRewriteEq(atom);
   }
-  // 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
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index a208c9b10..41cc9591d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -119,7 +119,7 @@ class TheoryArith : public Theory {
    * This calls the operator elimination utility to eliminate extended
    * symbols.
    */
-  TrustNode ppRewrite(TNode atom) override;
+  TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 
   std::string identify() const override { return std::string("TheoryArith"); }
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index dbe69dbe5..2335fb491 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -318,7 +318,7 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
   return term;
 }
 
-TrustNode TheoryArrays::ppRewrite(TNode term)
+TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
 {
   // first, see if we need to expand definitions
   TrustNode texp = expandDefinition(term);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 689e72a44..6a723d680 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -196,7 +196,7 @@ class TheoryArrays : public Theory {
  public:
   PPAssertStatus ppAssert(TrustNode tin,
                           TrustSubstitutionMap& outSubstitutions) override;
-  TrustNode ppRewrite(TNode atom) override;
+  TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
 
   /////////////////////////////////////////////////////////////////////////////
   // T-PROPAGATION / REGISTRATION
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index d801e4f0f..3d8a5d3ea 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -198,7 +198,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(
   return d_internal->ppAssert(tin, outSubstitutions);
 }
 
-TrustNode TheoryBV::ppRewrite(TNode t)
+TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
 {
   // first, see if we need to expand definitions
   TrustNode texp = expandDefinition(t);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 4e7cfdd2a..93e03e5ca 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -90,7 +90,7 @@ class TheoryBV : public Theory
   PPAssertStatus ppAssert(TrustNode in,
                           TrustSubstitutionMap& outSubstitutions) override;
 
-  TrustNode ppRewrite(TNode t) override;
+  TrustNode ppRewrite(TNode t, std::vector<SkolemLemma>& lems) override;
 
   void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
 
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index e20e3db9b..d0b7790b2 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -603,7 +603,7 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
   return TrustNode::null();
 }
 
-TrustNode TheoryDatatypes::ppRewrite(TNode in)
+TrustNode TheoryDatatypes::ppRewrite(TNode in, std::vector<SkolemLemma>& lems)
 {
   Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
   // first, see if we need to expand definitions
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 95dccf2e5..447c4371a 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -231,7 +231,7 @@ private:
   //--------------------------------- end standard check
   void preRegisterTerm(TNode n) override;
   TrustNode expandDefinition(Node n) override;
-  TrustNode ppRewrite(TNode n) override;
+  TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   std::string identify() const override
   {
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index c783620a7..d17e2999e 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -454,7 +454,7 @@ TrustNode TheoryFp::expandDefinition(Node node)
   return TrustNode::null();
 }
 
-TrustNode TheoryFp::ppRewrite(TNode node)
+TrustNode TheoryFp::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
 {
   Trace("fp-ppRewrite") << "TheoryFp::ppRewrite(): " << node << std::endl;
   // first, see if we need to expand definitions
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 2283756f6..1660d5799 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -64,7 +64,7 @@ class TheoryFp : public Theory
 
   void preRegisterTerm(TNode node) override;
 
-  TrustNode ppRewrite(TNode node) override;
+  TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
 
   //--------------------------------- standard check
   /** Do we need a check call at last call effort? */
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 9bc16e609..ee23aae49 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -135,7 +135,7 @@ TrustNode TheorySets::expandDefinition(Node n)
   return d_internal->expandDefinition(n);
 }
 
-TrustNode TheorySets::ppRewrite(TNode n)
+TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
 {
   Kind nk = n.getKind();
   if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
@@ -159,7 +159,7 @@ TrustNode TheorySets::ppRewrite(TNode n)
       throw LogicException(ss.str());
     }
   }
-  return d_internal->ppRewrite(n);
+  return d_internal->ppRewrite(n, lems);
 }
 
 Theory::PPAssertStatus TheorySets::ppAssert(
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 3937a32b6..56b0d6290 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -84,7 +84,7 @@ class TheorySets : public Theory
    * we throw an exception. Additionally, we expand operators like choose
    * and is_singleton.
    */
-  TrustNode ppRewrite(TNode n) override;
+  TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override;
   PPAssertStatus ppAssert(TrustNode tin,
                           TrustSubstitutionMap& outSubstitutions) override;
   void presolve() override;
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index bb7388cad..c15ea6f65 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1276,7 +1276,8 @@ TrustNode TheorySetsPrivate::expandDefinition(Node node)
   return TrustNode::null();
 }
 
-TrustNode TheorySetsPrivate::ppRewrite(Node node)
+TrustNode TheorySetsPrivate::ppRewrite(Node node,
+                                       std::vector<SkolemLemma>& lems)
 {
   Debug("sets-proc") << "ppRewrite : " << node << std::endl;
 
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 247aa245c..262a4c572 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -170,7 +170,7 @@ class TheorySetsPrivate {
   /** ppRewrite, which expands choose.  */
   TrustNode expandDefinition(Node n);
   /** ppRewrite, which expands choose and is_singleton.  */
-  TrustNode ppRewrite(Node n);
+  TrustNode ppRewrite(Node n, std::vector<SkolemLemma>& lems);
 
   void presolve();
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 73f78bddd..7f838e411 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -986,7 +986,7 @@ void TheoryStrings::checkRegisterTermsNormalForms()
   }
 }
 
-TrustNode TheoryStrings::ppRewrite(TNode atom)
+TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
 {
   Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
   if (atom.getKind() == STRING_FROM_CODE)
@@ -1001,6 +1001,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom)
     Node k = nm->mkBoundVar(nm->stringType());
     Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
     Node emp = Word::mkEmptyWord(atom.getType());
+    // TODO: use skolem manager
     Node ret = nm->mkNode(
         WITNESS,
         bvl,
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 5293a95b8..12f644fb4 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -114,7 +114,7 @@ class TheoryStrings : public Theory {
   /** called when a new equivalence class is created */
   void eqNotifyNewClass(TNode t);
   /** preprocess rewrite */
-  TrustNode ppRewrite(TNode atom) override;
+  TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
   /** Collect model values in m based on the relevant terms given by termSet */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 3278c8187..68a2e1436 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -32,6 +32,7 @@
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
 #include "theory/logic_info.h"
+#include "theory/skolem_lemma.h"
 #include "theory/theory_id.h"
 #include "theory/trust_node.h"
 #include "theory/valuation.h"
@@ -730,8 +731,22 @@ class Theory {
    * preprocessing pass, where n is an equality from the input formula,
    * and in theory preprocessing, where n is a (non-equality) term occurring
    * in the input or generated in a lemma.
+   *
+   * @param n the node to preprocess-rewrite.
+   * @param lems a set of lemmas that should be added as a consequence of
+   * preprocessing n. These are in the form of "skolem lemmas". For example,
+   * calling this method on (div x n), we return a trust node proving:
+   *   (= (div x n) k_div)
+   * for fresh skolem k, and add the skolem lemma for k that indicates that
+   * it is the division of x and n.
+   *
+   * Note that ppRewrite should not return WITNESS terms, since the internal
+   * calculus works in "original forms" and not "witness forms".
    */
-  virtual TrustNode ppRewrite(TNode n) { return TrustNode::null(); }
+  virtual TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
+  {
+    return TrustNode::null();
+  }
 
   /**
    * Notify preprocessed assertions. Called on new assertions after
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f34aebe8b..64181a8ee 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -797,7 +797,11 @@ theory::Theory::PPAssertStatus TheoryEngine::solve(
 theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
 {
   Assert(eq.getKind() == kind::EQUAL);
-  return theoryOf(eq)->ppRewrite(eq);
+  std::vector<SkolemLemma> lems;
+  TrustNode trn = theoryOf(eq)->ppRewrite(eq, lems);
+  // should never introduce a skolem to eliminate an equality
+  Assert(lems.empty());
+  return trn;
 }
 
 void TheoryEngine::notifyPreprocessedAssertions(
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 51f2155d3..ea4b0f82f 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -94,8 +94,7 @@ TrustNode TheoryPreprocessor::preprocessInternal(
 {
   // In this method, all rewriting steps of node are stored in d_tpg.
 
-  Trace("tpp-debug") << "TheoryPreprocessor::preprocess: start " << node
-                     << std::endl;
+  Trace("tpp") << "TheoryPreprocessor::preprocess: start " << node << std::endl;
 
   // We must rewrite before preprocessing, because some terms when rewritten
   // may introduce new terms that are not top-level and require preprocessing.
@@ -122,6 +121,23 @@ TrustNode TheoryPreprocessor::preprocessInternal(
     }
     Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
   }
+
+  if (procLemmas)
+  {
+    // Also must preprocess the new lemmas. This is especially important for
+    // formulas containing witness terms whose bodies are not in preprocessed
+    // form, as term formula removal introduces new lemmas for these that
+    // require theory-preprocessing.
+    size_t i = 0;
+    while (i < newLemmas.size())
+    {
+      TrustNode cur = newLemmas[i];
+      newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
+      Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl;
+      i++;
+    }
+  }
+
   if (node == ppNode)
   {
     Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
@@ -151,20 +167,9 @@ TrustNode TheoryPreprocessor::preprocessInternal(
 
   Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
                      << tret.getNode() << std::endl;
-  if (procLemmas)
-  {
-    // Also must preprocess the new lemmas. This is especially important for
-    // formulas containing witness terms whose bodies are not in preprocessed
-    // form, as term formula removal introduces new lemmas for these that
-    // require theory-preprocessing.
-    size_t i = 0;
-    while (i < newLemmas.size())
-    {
-      TrustNode cur = newLemmas[i];
-      newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
-      i++;
-    }
-  }
+  Trace("tpp") << "TheoryPreprocessor::preprocess: return " << tret.getNode()
+               << ", procLemmas=" << procLemmas
+               << ", # lemmas = " << newLemmas.size() << std::endl;
   return tret;
 }
 
@@ -278,7 +283,13 @@ TrustNode TheoryPreprocessor::theoryPreprocess(
     // If this is an atom, we preprocess its terms with the theory ppRewriter
     if (tid != THEORY_BOOL)
     {
-      Node ppRewritten = ppTheoryRewrite(current);
+      std::vector<SkolemLemma> lems;
+      Node ppRewritten = ppTheoryRewrite(current, lems);
+      for (const SkolemLemma& lem : lems)
+      {
+        newLemmas.push_back(lem.d_lemma);
+        newSkolems.push_back(lem.d_skolem);
+      }
       Assert(Rewriter::rewrite(ppRewritten) == ppRewritten);
       if (isProofEnabled() && ppRewritten != current)
       {
@@ -365,7 +376,8 @@ TrustNode TheoryPreprocessor::theoryPreprocess(
 }
 
 // Recursively traverse a term and call the theory rewriter on its sub-terms
-Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
+Node TheoryPreprocessor::ppTheoryRewrite(TNode term,
+                                         std::vector<SkolemLemma>& lems)
 {
   NodeMap::iterator find = d_ppCache.find(term);
   if (find != d_ppCache.end())
@@ -374,7 +386,7 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
   }
   if (term.getNumChildren() == 0)
   {
-    return preprocessWithProof(term);
+    return preprocessWithProof(term, lems);
   }
   // should be in rewritten form here
   Assert(term == Rewriter::rewrite(term));
@@ -390,12 +402,12 @@ Node TheoryPreprocessor::ppTheoryRewrite(TNode term)
     }
     for (const Node& nt : term)
     {
-      newNode << ppTheoryRewrite(nt);
+      newNode << ppTheoryRewrite(nt, lems);
     }
     newTerm = Node(newNode);
     newTerm = rewriteWithProof(newTerm, d_tpg.get(), false);
   }
-  newTerm = preprocessWithProof(newTerm);
+  newTerm = preprocessWithProof(newTerm, lems);
   d_ppCache[term] = newTerm;
   Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
   return newTerm;
@@ -421,13 +433,16 @@ Node TheoryPreprocessor::rewriteWithProof(Node term,
   return termr;
 }
 
-Node TheoryPreprocessor::preprocessWithProof(Node term)
+Node TheoryPreprocessor::preprocessWithProof(Node term,
+                                             std::vector<SkolemLemma>& lems)
 {
   // Important that it is in rewritten form, to ensure that the rewrite steps
   // recorded in d_tpg are functional. In other words, there should not
   // be steps from the same term to multiple rewritten forms, which would be
   // the case if we registered a preprocessing step for a non-rewritten term.
   Assert(term == Rewriter::rewrite(term));
+  Trace("tpp-debug2") << "preprocessWithProof " << term
+                      << ", #lems = " << lems.size() << std::endl;
   // We never call ppRewrite on equalities here, since equalities have a
   // special status. In particular, notice that theory preprocessing can be
   // called on all formulas asserted to theory engine, including those generated
@@ -446,10 +461,12 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
     return term;
   }
   // call ppRewrite for the given theory
-  TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term);
+  TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems);
+  Trace("tpp-debug2") << "preprocessWithProof returned " << trn
+                      << ", #lems = " << lems.size() << std::endl;
   if (trn.isNull())
   {
-    // no change, return original term
+    // no change, return
     return term;
   }
   Node termr = trn.getNode();
@@ -460,7 +477,7 @@ Node TheoryPreprocessor::preprocessWithProof(Node term)
   }
   // Rewrite again here, which notice is a *pre* rewrite.
   termr = rewriteWithProof(termr, d_tpg.get(), true);
-  return ppTheoryRewrite(termr);
+  return ppTheoryRewrite(termr, lems);
 }
 
 bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index bb4a78a02..e9abccad9 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -26,6 +26,7 @@
 #include "expr/tconv_seq_proof_generator.h"
 #include "expr/term_conversion_proof_generator.h"
 #include "smt/term_formula_removal.h"
+#include "theory/skolem_lemma.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
@@ -188,7 +189,7 @@ class TheoryPreprocessor
    * applies ppRewrite and rewriting until fixed point on term using
    * the method preprocessWithProof helper below.
    */
-  Node ppTheoryRewrite(TNode term);
+  Node ppTheoryRewrite(TNode term, std::vector<SkolemLemma>& lems);
   /**
    * Rewrite with proof, which stores a REWRITE step in pg if necessary
    * and returns the rewritten form of term.
@@ -204,7 +205,7 @@ class TheoryPreprocessor
    * the preprocessed and rewritten form of term. It should be the case that
    * term is already in rewritten form.
    */
-  Node preprocessWithProof(Node term);
+  Node preprocessWithProof(Node term, std::vector<SkolemLemma>& lems);
   /**
    * Register rewrite trn based on trust node into term conversion generator
    * pg, which uses THEORY_PREPROCESS as a step if no proof generator is
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 273e81740..32524b562 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -206,7 +206,7 @@ void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
 }
 //--------------------------------- end standard check
 
-TrustNode TheoryUF::ppRewrite(TNode node)
+TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
 {
   Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
                       << std::endl;
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index be63be373..e1184a829 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -140,7 +140,7 @@ private:
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 
-  TrustNode ppRewrite(TNode node) override;
+  TrustNode ppRewrite(TNode node, std::vector<SkolemLemma>& lems) override;
   void preRegisterTerm(TNode term) override;
   TrustNode explain(TNode n) override;