(proof-new) Proof production for term formula removal (#4687)

This adds proof support in the term formula removal pass.

It also refactors this class heavily so that its interface is more intuitive and does not depend on AssertionPipeline.

1 files changed, 17 insertions, 8 deletions

diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h
index 2488cf162..2f3813e68 100644
--- a/src/theory/theory_preprocessor.h
+++ b/src/theory/theory_preprocessor.h
@@ -46,15 +46,24 @@ class TheoryPreprocessor
   /** Clear the cache of this class */
   void clearCache();
   /**
-   * Preprocesses node and stores it along with lemmas generated by
-   * preprocessing into the assertion pipeline lemmas. The (optional) argument
-   * lcp is the proof that stores a proof of all top-level formulas in lemmas,
-   * assuming that lcp initially contains a proof of node. The flag
-   * doTheoryPreprocess is whether we should run theory-specific preprocessing.
+   * Preprocesses the given assertion node. It returns a TrustNode of kind
+   * TrustNodeKind::REWRITE indicating the preprocessed form of node. It stores
+   * additional lemmas in newLemmas, which are trust nodes of kind
+   * TrustNodeKind::LEMMA. These correspond to e.g. lemmas corresponding to ITE
+   * removal. For each lemma in newLemmas, we add the corresponding skolem that
+   * the lemma defines. The flag doTheoryPreprocess is whether we should run
+   * theory-specific preprocessing.
+   *
+   * @param node The assertion to preprocess,
+   * @param newLemmas The lemmas to add to the set of assertions,
+   * @param newSkolems The skolems that newLemmas correspond to,
+   * @param doTheoryPreprocess whether to run theory-specific preprocessing.
+   * @return The trust node corresponding to rewriting node via preprocessing.
    */
-  void preprocess(TNode node,
-                  preprocessing::AssertionPipeline& lemmas,
-                  bool doTheoryPreprocess);
+  TrustNode preprocess(TNode node,
+                       std::vector<TrustNode>& newLemmas,
+                       std::vector<Node>& newSkolems,
+                       bool doTheoryPreprocess);
   /**
    * Runs theory specific preprocessing on the non-Boolean parts of
    * the formula.  This is only called on input assertions, after ITEs