(proof-new) proofs in ee -> arith pipeline (#5215)

Threads proofs through the flow of information from the equality engine
into the theory of arithmetic.

Pretty straightforward. You just have to bundle up information from the EE.

6 files changed, 92 insertions, 42 deletions

diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 0c9cb6c9c..e1cb1c3ca 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -172,11 +172,12 @@ RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
 {}
 
 /* If you are not an equality engine, don't use this! */
-void RaiseEqualityEngineConflict::raiseEEConflict(Node n) const{
-  d_ta.raiseBlackBoxConflict(n);
+void RaiseEqualityEngineConflict::raiseEEConflict(
+    Node n, std::shared_ptr<ProofNode> pf) const
+{
+  d_ta.raiseBlackBoxConflict(n, pf);
 }
 
-
 BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
 : d_ta(ta)
 {}
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 1ce61f46f..796a93ea4 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -19,6 +19,7 @@
 #pragma once
 
 #include "expr/node.h"
+#include "expr/proof_node.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/constraint_forward.h"
@@ -177,8 +178,11 @@ private:
 public:
   RaiseEqualityEngineConflict(TheoryArithPrivate& ta);
 
-  /* If you are not an equality engine, don't use this! */
-  void raiseEEConflict(Node n) const;
+  /* If you are not an equality engine, don't use this!
+   *
+   * The proof should prove that `n` is a conflict.
+   * */
+  void raiseEEConflict(Node n, std::shared_ptr<ProofNode> pf) const;
 };
 
 class BoundCountingLookup {
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 404b5bcd0..57214e0f8 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -148,11 +148,13 @@ void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyMerge(TNode t1,
 void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 }
 
-void ArithCongruenceManager::raiseConflict(Node conflict){
+void ArithCongruenceManager::raiseConflict(Node conflict,
+                                           std::shared_ptr<ProofNode> pf)
+{
   Assert(!inConflict());
   Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
   d_inConflict.raise();
-  d_raiseConflict.raiseEEConflict(conflict);
+  d_raiseConflict.raiseEEConflict(conflict, pf);
 }
 bool ArithCongruenceManager::inConflict() const{
   return d_inConflict.isRaised();
@@ -345,11 +347,22 @@ bool ArithCongruenceManager::propagate(TNode x){
     if(rewritten.getConst<bool>()){
       return true;
     }else{
+      // x rewrites to false.
       ++(d_statistics.d_conflicts);
-
-      Node conf = flattenAnd(explainInternal(x));
-      raiseConflict(conf);
+      TrustNode trn = explainInternal(x);
+      Node conf = flattenAnd(trn.getNode());
       Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
+      if (isProofEnabled())
+      {
+        auto pf = trn.getGenerator()->getProofFor(trn.getProven());
+        auto confPf = d_pnm->mkNode(
+            PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {conf.negate()});
+        raiseConflict(conf, confPf);
+      }
+      else
+      {
+        raiseConflict(conf);
+      }
       return false;
     }
   }
@@ -371,9 +384,10 @@ bool ArithCongruenceManager::propagate(TNode x){
                                    << c->negationHasProof() << std::endl;
 
   if(c->negationHasProof()){
-    Node expC = explainInternal(x);
+    TrustNode texpC = explainInternal(x);
+    Node expC = texpC.getNode();
     ConstraintCP negC = c->getNegation();
-    Node neg = negC->externalExplainByAssertions();
+    Node neg = Constraint::externalExplainByAssertions({negC});
     Node conf = expC.andNode(neg);
     Node final = flattenAnd(conf);
 
@@ -443,21 +457,15 @@ void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<
   }
 }
 
-Node ArithCongruenceManager::explainInternal(TNode internal){
-  std::vector<TNode> assumptions;
-  explain(internal, assumptions);
-
-  std::set<TNode> assumptionSet;
-  assumptionSet.insert(assumptions.begin(), assumptions.end());
-
-  if (assumptionSet.size() == 1) {
-    // All the same, or just one
-    return assumptions[0];
-  }else{
-    NodeBuilder<> conjunction(kind::AND);
-    enqueueIntoNB(assumptionSet, conjunction);
-    return conjunction;
+TrustNode ArithCongruenceManager::explainInternal(TNode internal)
+{
+  if (isProofEnabled())
+  {
+    return d_pfee->explain(internal);
   }
+  // otherwise, explain without proof generator
+  Node exp = d_ee->mkExplainLit(internal);
+  return TrustNode::mkTrustPropExp(internal, exp, nullptr);
 }
 
 TrustNode ArithCongruenceManager::explain(TNode external)
@@ -465,15 +473,28 @@ TrustNode ArithCongruenceManager::explain(TNode external)
   Trace("arith-ee") << "Ask for explanation of " << external << std::endl;
   Node internal = externalToInternal(external);
   Trace("arith-ee") << "...internal = " << internal << std::endl;
-  Node exp = explainInternal(internal);
-  if (isProofEnabled())
+  TrustNode trn = explainInternal(internal);
+  if (isProofEnabled() && trn.getProven()[1] != external)
   {
-    Node impl = NodeManager::currentNM()->mkNode(Kind::IMPLIES, exp, external);
-    // For now, we just trust
-    auto pfOfImpl = d_pnm->mkNode(PfRule::INT_TRUST, {}, {impl});
-    return d_pfGenExplain->mkTrustNode(impl, pfOfImpl);
+    Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
+    Assert(trn.getProven().getKind() == Kind::IMPLIES);
+    Assert(trn.getGenerator() != nullptr);
+    Trace("arith-ee") << "tweaking proof to prove " << external << " not "
+                      << trn.getProven()[1] << std::endl;
+    std::vector<std::shared_ptr<ProofNode>> assumptionPfs;
+    std::vector<Node> assumptions = andComponents(trn.getNode());
+    assumptionPfs.push_back(trn.toProofNode());
+    for (const auto& a : assumptions)
+    {
+      assumptionPfs.push_back(
+          d_pnm->mkNode(PfRule::TRUE_INTRO, {d_pnm->mkAssume(a)}, {}));
+    }
+    auto litPf = d_pnm->mkNode(
+        PfRule::MACRO_SR_PRED_TRANSFORM, {assumptionPfs}, {external});
+    auto extPf = d_pnm->mkScope(litPf, assumptions);
+    return d_pfGenExplain->mkTrustedPropagation(external, trn.getNode(), extPf);
   }
-  return TrustNode::mkTrustPropExp(external, exp, nullptr);
+  return trn;
 }
 
 void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 8b9086eb0..3698f46d8 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -129,8 +129,12 @@ private:
   /** Pointer to the proof equality engine of TheoryArith */
   theory::eq::ProofEqEngine* d_pfee;
 
-
-  void raiseConflict(Node conflict);
+  /** Raise a conflict node `conflict` to the theory of arithmetic.
+   *
+   * When proofs are enabled, a (closed) proof of the conflict should be
+   * provided.
+   */
+  void raiseConflict(Node conflict, std::shared_ptr<ProofNode> pf = nullptr);
   /**
    * Are proofs enabled? This is true if a non-null proof manager was provided
    * to the constructor of this class.
@@ -195,8 +199,13 @@ private:
 
   void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
 
-  Node explainInternal(TNode internal);
-public:
+  /**
+   * Determine an explaination for `internal`. That is a conjunction of theory
+   * literals which imply `internal`.
+   *
+   * The TrustNode here is a trusted propagation.
+   */
+  TrustNode explainInternal(TNode internal);
 
  public:
   ArithCongruenceManager(context::Context* satContext,
@@ -221,7 +230,12 @@ public:
   void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee);
   //--------------------------------- end initialization
 
+  /**
+   * Return the trust node for the explanation of literal. The returned
+   * trust node is generated by the proof equality engine of this class.
+   */
   TrustNode explain(TNode literal);
+
   void explain(TNode lit, NodeBuilder<>& out);
 
   void addWatchedPair(ArithVar s, TNode x, TNode y);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 4e4259482..6652d3ee9 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -536,8 +536,17 @@ void TheoryArithPrivate::raiseConflict(ConstraintCP a){
   d_conflicts.push_back(a);
 }
 
-void TheoryArithPrivate::raiseBlackBoxConflict(Node bb){
-  if(d_blackBoxConflict.get().isNull()){
+void TheoryArithPrivate::raiseBlackBoxConflict(Node bb,
+                                               std::shared_ptr<ProofNode> pf)
+{
+  Debug("arith::bb") << "raiseBlackBoxConflict: " << bb << std::endl;
+  if (d_blackBoxConflict.get().isNull())
+  {
+    if (options::proofNew())
+    {
+      Debug("arith::bb") << "  with proof " << pf << std::endl;
+      d_blackBoxConflictPf.set(pf);
+    }
     d_blackBoxConflict = bb;
   }
 }
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 5cb281b36..012e45b2f 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -17,9 +17,10 @@
 
 #pragma once
 
+#include <stdint.h>
+
 #include <map>
 #include <queue>
-#include <stdint.h>
 #include <vector>
 
 #include "context/cdhashset.h"
@@ -57,6 +58,7 @@
 #include "theory/eager_proof_generator.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_node.h"
 #include "theory/valuation.h"
 #include "util/dense_map.h"
 #include "util/integer.h"
@@ -329,8 +331,7 @@ private:
   // void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
 
   /** This is a conflict that is magically known to hold. */
-  void raiseBlackBoxConflict(Node bb);
-
+  void raiseBlackBoxConflict(Node bb, std::shared_ptr<ProofNode> pf = nullptr);
   /**
    * Returns true iff a conflict has been raised. This method is public since
    * it is needed by the ArithState class to know whether we are in conflict.