(proof-new) Arithmetic operator elim proof producing (#4783)

This updates the interface for arithmetic operator elimination for the new proof format.

The actual proof production of the operator elimination class (providing proofs for 
introduced witness terms) will be done in a separate PR.

This also changes the witness terms introduced by this class so their body is in 
Skolem form, which simplifies term formula removal.

Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>

1 files changed, 3 insertions, 9 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index fcbfd1baf..52321ffd4 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -39,7 +39,7 @@ TheoryArith::TheoryArith(context::Context* c,
                          ProofNodeManager* pnm)
     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
       d_internal(
-          new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)),
+          new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
       d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
       d_proofRecorder(nullptr)
 {
@@ -78,8 +78,7 @@ void TheoryArith::finishInit()
 
 TrustNode TheoryArith::expandDefinition(Node node)
 {
-  Node expNode = d_internal->expandDefinition(node);
-  return TrustNode::mkTrustRewrite(node, expNode, nullptr);
+  return d_internal->expandDefinition(node);
 }
 
 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -93,12 +92,7 @@ void TheoryArith::addSharedTerm(TNode n){
 TrustNode TheoryArith::ppRewrite(TNode atom)
 {
   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
-  Node ret = d_internal->ppRewrite(atom);
-  if (ret != atom)
-  {
-    return TrustNode::mkTrustRewrite(atom, ret, nullptr);
-  }
-  return TrustNode::null();
+  return d_internal->ppRewrite(atom);
 }
 
 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {