Thread proofs through arith channels & similar (#5818)

Thread proofs through conflict/lemma storages & channels in TheoryArithPrivate

d_acTmp
d_approxCuts
lemma output channel
conflict output channel

2 files changed, 40 insertions, 13 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d51efa707..3b5f0dd82 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1704,12 +1704,28 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion)
     Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
     Assert(!isSetup(eq));
     Node reEq = Rewriter::rewrite(eq);
+    Debug("arith::distinct::const") << "Assertion: " << assertion << std::endl;
+    Debug("arith::distinct::const") << "Eq       : " << eq << std::endl;
+    Debug("arith::distinct::const") << "reEq     : " << reEq << std::endl;
     if(reEq.getKind() == CONST_BOOLEAN){
       if(reEq.getConst<bool>() == isDistinct){
         // if is (not true), or false
         Assert((reEq.getConst<bool>() && isDistinct)
                || (!reEq.getConst<bool>() && !isDistinct));
-        raiseBlackBoxConflict(assertion);
+        if (proofsEnabled())
+        {
+          Pf assume = d_pnm->mkAssume(assertion);
+          std::vector<Node> assumptions = {assertion};
+          Pf pf = d_pnm->mkScope(d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
+                                               {d_pnm->mkAssume(assertion)},
+                                               {}),
+                                 assumptions);
+          raiseBlackBoxConflict(assertion, pf);
+        }
+        else
+        {
+          raiseBlackBoxConflict(assertion);
+        }
       }
       return NullConstraint;
     }
@@ -1978,7 +1994,7 @@ void TheoryArithPrivate::outputConflicts(){
 void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma)
 {
   Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl;
-  (d_containing.d_out)->lemma(lemma.getNode());
+  (d_containing.d_out)->trustedLemma(lemma);
 }
 
 void TheoryArithPrivate::outputLemma(TNode lem) {
@@ -1989,7 +2005,7 @@ void TheoryArithPrivate::outputLemma(TNode lem) {
 void TheoryArithPrivate::outputTrustedConflict(TrustNode conf)
 {
   Debug("arith::channel") << "Arith trusted conflict: " << conf << std::endl;
-  (d_containing.d_out)->conflict(conf.getNode());
+  (d_containing.d_out)->trustedConflict(conf);
 }
 
 void TheoryArithPrivate::outputConflict(TNode lit) {
@@ -2663,7 +2679,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
         d_replayedLemmas = replayLemmas(approx);
         Assert(d_acTmp.empty());
         while(!d_approxCuts.empty()){
-          Node lem = d_approxCuts.front();
+          TrustNode lem = d_approxCuts.front();
           d_approxCuts.pop();
           d_acTmp.push_back(lem);
         }
@@ -2673,7 +2689,7 @@ std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex
 
   /* move into the current context. */
   while(!d_acTmp.empty()){
-    Node lem = d_acTmp.back();
+    TrustNode lem = d_acTmp.back();
     d_acTmp.pop_back();
     d_approxCuts.push_back(lem);
   }
@@ -2812,7 +2828,8 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
 
         Node implication = asLemma.impNode(implied);
         // DO NOT CALL OUTPUT LEMMA!
-        d_approxCuts.push_back(implication);
+        // TODO (project #37): justify
+        d_approxCuts.push_back(TrustNode::mkTrustLemma(implication, nullptr));
         Debug("approx::lemmas") << "cut["<<i<<"] " << implication << endl;
         ++(d_statistics.d_mipExternalCuts);
       }
@@ -2822,7 +2839,14 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){
       if(!lit.isNull()){
         anythingnew = anythingnew || !isSatLiteral(lit);
         Node branch = lit.orNode(lit.notNode());
-        d_approxCuts.push_back(branch);
+        if (proofsEnabled())
+        {
+          d_pfGen->mkTrustNode(branch, PfRule::SPLIT, {}, {lit});
+        }
+        else
+        {
+          d_approxCuts.push_back(TrustNode::mkTrustLemma(branch, nullptr));
+        }
         ++(d_statistics.d_mipExternalBranch);
         Debug("approx::lemmas") << "branching "<< root <<" as " << branch << endl;
       }
@@ -3068,7 +3092,7 @@ bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel){
       Assert(branch.getNode().getKind() == kind::OR);
       Node rwbranch = Rewriter::rewrite(branch.getNode()[0]);
       if(!isSatLiteral(rwbranch)){
-        d_approxCuts.push_back(branch.getNode());
+        d_approxCuts.push_back(branch);
         return true;
       }
     }
@@ -3523,12 +3547,12 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
   if(!d_approxCuts.empty()){
     bool anyFresh = false;
     while(!d_approxCuts.empty()){
-      Node lem = d_approxCuts.front();
+      TrustNode lem = d_approxCuts.front();
       d_approxCuts.pop();
       Debug("arith::approx::cuts") << "approximate cut:" << lem << endl;
-      anyFresh = anyFresh || hasFreshArithLiteral(lem);
+      anyFresh = anyFresh || hasFreshArithLiteral(lem.getNode());
       Debug("arith::lemma") << "approximate cut:" << lem << endl;
-      outputLemma(lem);
+      outputTrustedLemma(lem);
     }
     if(anyFresh){
       emmittedConflictOrSplit = true;
@@ -3630,6 +3654,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
       if(possibleConflict != Node::null()){
         revertOutOfConflict();
         Debug("arith::conflict") << "dio conflict   " << possibleConflict << endl;
+        // TODO (project #37): justify (proofs in the DIO solver)
         raiseBlackBoxConflict(possibleConflict);
         outputConflicts();
         emmittedConflictOrSplit = true;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 1a06355a0..56e8fa4b0 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -713,8 +713,10 @@ private:
     return (d_containing.d_valuation).getSatValue(n);
   }
 
-  context::CDQueue<Node> d_approxCuts;
-  std::vector<Node> d_acTmp;
+  /** Used for replaying approximate simplex */
+  context::CDQueue<TrustNode> d_approxCuts;
+  /** Also used for replaying approximate simplex. "approximate cuts temporary storage" */
+  std::vector<TrustNode> d_acTmp;
 
   /** Counts the number of fullCheck calls to arithmetic. */
   uint32_t d_fullCheckCounter;