(proof-new) pfs in TheoryArith(Private) explainations (#5258)

Very simple, just threading the proofs through.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 47595e0bb233ba00c4c854541fa678b72fe153e9..532aaf55c328c539cbbe53deb70c64b6bc7a75c3 100644 (file)
--- 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 58483200a9952f43247f4c90d52a826b02130239..49432d552c7ecffad69eb112f354b3a58a25ba9d 100644 (file)
--- 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 7c4aff2ca9e634cbc7ea1b7a619acec67b4f72e5..3abf17c3dfcb3363d3e5de38a4f0138f71cb4e4a 100644 (file)
--- 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;