(proof-new) pfs for conflicts in TheoryArithPrivate (#5257)

Threads conflict proofs through TheoryArithPrivate.

Mostly just wiring things up.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 119be6307a06b755c102624e1a57f931c631314a..58483200a9952f43247f4c90d52a826b02130239 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -531,6 +531,11 @@ bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){
   return true;
 }
 
+bool TheoryArithPrivate::isProofEnabled() const
+{
+  return d_pnm != nullptr;
+}
+
 void TheoryArithPrivate::raiseConflict(ConstraintCP a){
   Assert(a->inConflict());
   d_conflicts.push_back(a);
@@ -542,7 +547,7 @@ void TheoryArithPrivate::raiseBlackBoxConflict(Node bb,
   Debug("arith::bb") << "raiseBlackBoxConflict: " << bb << std::endl;
   if (d_blackBoxConflict.get().isNull())
   {
-    if (options::proofNew())
+    if (isProofEnabled())
     {
       Debug("arith::bb") << "  with proof " << pf << std::endl;
       d_blackBoxConflictPf.set(pf);
@@ -1890,7 +1895,15 @@ void TheoryArithPrivate::outputConflicts(){
         pf.print(std::cout);
         std::cout << std::endl;
       }
-      Node conflict = confConstraint->externalExplainConflict().getNode();
+      if (Debug.isOn("arith::pf::tree"))
+      {
+        Debug("arith::pf::tree") << "\n\nTree:\n";
+        confConstraint->printProofTree(Debug("arith::pf::tree"));
+        confConstraint->getNegation()->printProofTree(Debug("arith::pf::tree"));
+      }
+
+      TrustNode trustedConflict = confConstraint->externalExplainConflict();
+      Node conflict = trustedConflict.getNode();
 
       ++conflicts;
       Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
@@ -1900,7 +1913,14 @@ void TheoryArithPrivate::outputConflicts(){
         Debug("arith::conflict") << "(normalized to) " << conflict << endl;
       }
 
-      outputConflict(conflict);
+      if (isProofEnabled())
+      {
+        outputTrustedConflict(trustedConflict);
+      }
+      else
+      {
+        outputConflict(conflict);
+      }
     }
   }
   if(!d_blackBoxConflict.get().isNull()){
@@ -1913,8 +1933,15 @@ void TheoryArithPrivate::outputConflicts(){
       bb = flattenAndSort(bb);
       Debug("arith::conflict") << "(normalized to) " << bb << endl;
     }
-
-    outputConflict(bb);
+    if (isProofEnabled() && d_blackBoxConflictPf.get())
+    {
+      auto confPf = d_blackBoxConflictPf.get();
+      outputTrustedConflict(d_pfGen->mkTrustNode(bb, confPf, true));
+    }
+    else
+    {
+      outputConflict(bb);
+    }
   }
 }
 
@@ -1929,6 +1956,12 @@ void TheoryArithPrivate::outputLemma(TNode lem) {
   (d_containing.d_out)->lemma(lem);
 }
 
+void TheoryArithPrivate::outputTrustedConflict(TrustNode conf)
+{
+  Debug("arith::channel") << "Arith trusted conflict: " << conf << std::endl;
+  (d_containing.d_out)->conflict(conf.getNode());
+}
+
 void TheoryArithPrivate::outputConflict(TNode lit) {
   Debug("arith::channel") << "Arith conflict: " << lit << std::endl;
   (d_containing.d_out)->conflict(lit);

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index be192e8805cac896da7f65fc125faa3bfcfea56d..7c4aff2ca9e634cbc7ea1b7a619acec67b4f72e5 100644 (file)
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -316,6 +316,8 @@ private:
   /** For holding the proof of the above conflict node. */
   context::CDO<std::shared_ptr<ProofNode>> d_blackBoxConflictPf;
 
+  bool isProofEnabled() const;
+
  public:
   /**
    * This adds the constraint a to the queue of conflicts in d_conflicts.
@@ -691,6 +693,7 @@ private:
   inline context::Context* getSatContext() const { return d_containing.getSatContext(); }
   void outputTrustedLemma(TrustNode lem);
   void outputLemma(TNode lem);
+  void outputTrustedConflict(TrustNode conf);
   void outputConflict(TNode lit);
   void outputPropagate(TNode lit);
   void outputRestart();