(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.

1 files changed, 11 insertions, 7 deletions

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  */