From 909a0aa67266d7659decf56f2e6eb8101a802d45 Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Mon, 25 Jan 2021 20:20:58 -0800
Subject: Add proofs to TheoryArithPrivate::propagate (#5812)

Specifically, add proofs to conflicts between (a) a propagation from the
congruence manager and (b) a constraint from the main solver.
---
 src/theory/arith/theory_arith_private.cpp | 52 ++++++++++++++++++++++++++++---
 1 file changed, 47 insertions(+), 5 deletions(-)

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index f905c971b..d51efa707 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4028,12 +4028,54 @@ void TheoryArithPrivate::propagate(Theory::Effort e) {
 
       outputPropagate(toProp);
     }else if(constraint->negationHasProof()){
-      Node exp = d_congruenceManager.explain(toProp).getNode();
-      Node notNormalized = normalized.getKind() == NOT ?
-        normalized[0] : normalized.notNode();
-      Node lp = flattenAnd(exp.andNode(notNormalized));
+      // The congruence manager can prove: antecedents => toProp,
+      // ergo. antecedents ^ ~toProp is a conflict.
+      TrustNode exp = d_congruenceManager.explain(toProp);
+      Node notNormalized = normalized.negate();
+      std::vector<Node> ants(exp.getNode().begin(), exp.getNode().end());
+      ants.push_back(notNormalized);
+      Node lp = safeConstructNary(kind::AND, ants);
       Debug("arith::prop") << "propagate conflict" <<  lp << endl;
-      raiseBlackBoxConflict(lp);
+      if (proofsEnabled())
+      {
+        // Assume all of antecedents and ~toProp (rewritten)
+        std::vector<Pf> pfAntList;
+        for (size_t i = 0; i < ants.size(); ++i)
+        {
+          pfAntList.push_back(d_pnm->mkAssume(ants[i]));
+        }
+        Pf pfAnt = pfAntList.size() > 1
+                       ? d_pnm->mkNode(PfRule::AND_INTRO, pfAntList, {})
+                       : pfAntList[0];
+        // Use modus ponens to get toProp (un rewritten)
+        Pf pfConc = d_pnm->mkNode(
+            PfRule::MODUS_PONENS,
+            {pfAnt, exp.getGenerator()->getProofFor(exp.getProven())},
+            {});
+        // prove toProp (rewritten)
+        Pf pfConcRewritten = d_pnm->mkNode(
+            PfRule::MACRO_SR_PRED_TRANSFORM, {pfConc}, {normalized});
+        Pf pfNotNormalized = d_pnm->mkAssume(notNormalized);
+        // prove bottom from toProp and ~toProp
+        Pf pfBot;
+        if (normalized.getKind() == kind::NOT)
+        {
+          pfBot = d_pnm->mkNode(
+              PfRule::CONTRA, {pfNotNormalized, pfConcRewritten}, {});
+        }
+        else
+        {
+          pfBot = d_pnm->mkNode(
+              PfRule::CONTRA, {pfConcRewritten, pfNotNormalized}, {});
+        }
+        // close scope
+        Pf pfNotAnd = d_pnm->mkScope(pfBot, ants);
+        raiseBlackBoxConflict(lp, pfNotAnd);
+      }
+      else
+      {
+        raiseBlackBoxConflict(lp);
+      }
       outputConflicts();
       return;
     }else{
-- 
cgit v1.2.3