(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, 35 insertions, 31 deletions

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(