From 9380d6fa2691da1bd8ce7c5501fde1e972ca7d3f Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Wed, 14 Oct 2020 10:17:35 -0700
Subject: [PATCH] (proof-new) pfs in TheoryArith(Private) explainations (#5258)

Very simple, just threading the proofs through.
---
 src/theory/arith/theory_arith.cpp         |  6 +-----
 src/theory/arith/theory_arith_private.cpp | 15 +++++++--------
 src/theory/arith/theory_arith_private.h   |  2 +-
 3 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 47595e0bb..532aaf55c 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -211,11 +211,7 @@ bool TheoryArith::needsCheckLastEffort() {
   return false;
 }
 
-TrustNode TheoryArith::explain(TNode n)
-{
-  Node exp = d_internal->explain(n);
-  return TrustNode::mkTrustPropExp(n, exp, nullptr);
-}
+TrustNode TheoryArith::explain(TNode n) { return d_internal->explain(n); }
 
 void TheoryArith::propagate(Effort e) {
   d_internal->propagate(e);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 58483200a..49432d552 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3832,33 +3832,32 @@ void TheoryArithPrivate::debugPrintModel(std::ostream& out) const{
   }
 }
 
-Node TheoryArithPrivate::explain(TNode n)
+TrustNode TheoryArithPrivate::explain(TNode n)
 {
   Debug("arith::explain") << "explain @" << getSatContext()->getLevel() << ": " << n << endl;
 
   ConstraintP c = d_constraintDatabase.lookup(n);
+  TrustNode exp;
   if(c != NullConstraint){
     Assert(!c->isAssumption());
-    Node exp = c->externalExplainForPropagation().getNode();
+    exp = c->externalExplainForPropagation();
     Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
-    return exp;
   }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
     c = d_assertionsThatDoNotMatchTheirLiterals[n];
     if(!c->isAssumption()){
-      Node exp = c->externalExplainForPropagation().getNode();
+      exp = c->externalExplainForPropagation();
       Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
-      return exp;
     }else{
       Debug("arith::explain") << "this is a strange mismatch" << n << endl;
       Assert(d_congruenceManager.canExplain(n));
-      Debug("arith::explain") << "this is a strange mismatch" << n << endl;
-      return d_congruenceManager.explain(n).getNode();
+      exp = d_congruenceManager.explain(n);
     }
   }else{
     Assert(d_congruenceManager.canExplain(n));
     Debug("arith::explain") << "dm explanation" << n << endl;
-    return d_congruenceManager.explain(n).getNode();
+    exp = d_congruenceManager.explain(n);
   }
+  return exp;
 }
 
 void TheoryArithPrivate::propagate(Theory::Effort e) {
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 7c4aff2ca..3abf17c3d 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -446,7 +446,7 @@ private:
   void preRegisterTerm(TNode n);
 
   void propagate(Theory::Effort e);
-  Node explain(TNode n);
+  TrustNode explain(TNode n);
 
   Rational deltaValueForTotalOrder() const;
 
-- 
2.30.2