(proof-new) proofs for arith-constraint explanations (#5224)

Threads proofs through arith::Constraint's machinery for explaining
constraints. Changes, by function:

externalExplainByAssertions:
introduce scope to prove the implication
externalExplainForPropagation:
introduce scope to prove the implication
externalExplainConflict:
use other machinery to prove conflicting constraints
use the CONTRA rule
introduce scope to close the conflict proof
Future commits will pick up these proofs in theory_arith_private.cpp.
Future commits will prove the "split" lemmas produced in constraint.cpp

4 files changed, 132 insertions, 34 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 9e421efc7..55bbe67cc 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -245,8 +245,7 @@ inline Node getIdentity(Kind k){
   case kind::MULT:
   case kind::NONLINEAR_MULT:
     return mkRationalNode(1);
-  default:
-    Unreachable();
+  default: Unreachable(); return {};  // silence warning
   }
 }
 
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index ecccca35b..a08122295 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -477,6 +477,29 @@ bool Constraint::isInternalAssumption() const {
   return getProofType() == InternalAssumeAP;
 }
 
+TrustNode Constraint::externalExplainByAssertions() const
+{
+  NodeBuilder<> nb(kind::AND);
+  auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel);
+  Node exp = safeConstructNary(nb);
+  if (d_database->isProofEnabled())
+  {
+    std::vector<Node> assumptions;
+    if (exp.getKind() == Kind::AND)
+    {
+      assumptions.insert(assumptions.end(), exp.begin(), exp.end());
+    }
+    else
+    {
+      assumptions.push_back(exp);
+    }
+    auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
+    return d_database->d_pfGen->mkTrustedPropagation(
+        getLiteral(), safeConstructNary(Kind::AND, assumptions), pf);
+  }
+  return TrustNode::mkTrustPropExp(getLiteral(), exp);
+}
+
 bool Constraint::isAssumption() const {
   return getProofType() == AssumeAP;
 }
@@ -1453,14 +1476,92 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){
   return externalExplain(b, AssertionOrderSentinel);
 }
 
-Node Constraint::externalExplainConflict() const{
+TrustNode Constraint::externalExplainForPropagation() const
+{
+  Assert(hasProof());
+  Assert(!isAssumption());
+  Assert(!isInternalAssumption());
+  NodeBuilder<> nb(Kind::AND);
+  auto pfFromAssumptions = externalExplain(nb, d_assertionOrder);
+  Node n = safeConstructNary(nb);
+  if (d_database->isProofEnabled())
+  {
+    std::vector<Node> assumptions;
+    if (n.getKind() == Kind::AND)
+    {
+      assumptions.insert(assumptions.end(), n.begin(), n.end());
+    }
+    else
+    {
+      assumptions.push_back(n);
+    }
+    if (getProofLiteral() != getLiteral())
+    {
+      pfFromAssumptions = d_database->d_pnm->mkNode(
+          PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {getLiteral()});
+    }
+    auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
+    return d_database->d_pfGen->mkTrustedPropagation(
+        getLiteral(), safeConstructNary(Kind::AND, assumptions), pf);
+  }
+  else
+  {
+    return TrustNode::mkTrustPropExp(getLiteral(), n);
+  }
+}
+
+TrustNode Constraint::externalExplainConflict() const
+{
   Debug("pf::arith::explain") << this << std::endl;
   Assert(inConflict());
   NodeBuilder<> nb(kind::AND);
-  externalExplainByAssertions(nb);
-  getNegation()->externalExplainByAssertions(nb);
-
-  return safeConstructNary(nb);
+  auto pf1 = externalExplainByAssertions(nb);
+  auto not2 = getNegation()->getProofLiteral().negate();
+  auto pf2 = getNegation()->externalExplainByAssertions(nb);
+  Node n = safeConstructNary(nb);
+  if (d_database->isProofEnabled())
+  {
+    auto pfNot2 = d_database->d_pnm->mkNode(
+        PfRule::MACRO_SR_PRED_TRANSFORM, {pf1}, {not2});
+    std::vector<Node> lits;
+    if (n.getKind() == Kind::AND)
+    {
+      lits.insert(lits.end(), n.begin(), n.end());
+    }
+    else
+    {
+      lits.push_back(n);
+    }
+    if (Debug.isOn("arith::pf::externalExplainConflict"))
+    {
+      Debug("arith::pf::externalExplainConflict") << "Lits:" << std::endl;
+      for (const auto& l : lits)
+      {
+        Debug("arith::pf::externalExplainConflict") << "  : " << l << std::endl;
+      }
+    }
+    std::vector<Node> contraLits = {getProofLiteral(),
+                                    getNegation()->getProofLiteral()};
+    auto bot =
+        not2.getKind() == Kind::NOT
+            ? d_database->d_pnm->mkNode(PfRule::CONTRA, {pf2, pfNot2}, {})
+            : d_database->d_pnm->mkNode(PfRule::CONTRA, {pfNot2, pf2}, {});
+    if (Debug.isOn("arith::pf::tree"))
+    {
+      Debug("arith::pf::tree") << *this << std::endl;
+      Debug("arith::pf::tree") << *getNegation() << std::endl;
+      Debug("arith::pf::tree") << "\n\nTree:\n";
+      printProofTree(Debug("arith::pf::tree"));
+      getNegation()->printProofTree(Debug("arith::pf::tree"));
+    }
+    auto confPf = d_database->d_pnm->mkScope(bot, lits);
+    return d_database->d_pfGen->mkTrustNode(
+        safeConstructNary(Kind::AND, lits), confPf, true);
+  }
+  else
+  {
+    return TrustNode::mkTrustConflict(n);
+  }
 }
 
 struct ConstraintCPHash {
@@ -1519,13 +1620,6 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order)
   return safeConstructNary(nb);
 }
 
-Node Constraint::externalExplain(AssertionOrder order) const
-{
-  NodeBuilder<> nb(kind::AND);
-  externalExplain(nb, order);
-  return safeConstructNary(nb);
-}
-
 std::shared_ptr<ProofNode> Constraint::externalExplain(
     NodeBuilder<>& nb, AssertionOrder order) const
 {
@@ -1843,13 +1937,19 @@ ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t
     }
   }
 }
-
 TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const
 {
   Assert(c->hasLiteral());
   return d_congruenceManager.explain(c->getLiteral());
 }
 
+void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder<>& nb) const
+{
+  Assert(c->hasLiteral());
+  // NOTE: this is not a recommended method since it ignores proofs
+  d_congruenceManager.explain(c->getLiteral(), nb);
+}
+
 bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
   return v < d_varDatabases.size();
 }
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 05845ec76..02bc3c988 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -553,9 +553,7 @@ class Constraint {
    * This is the minimum fringe of the implication tree s.t.
    * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
    */
-  Node externalExplainByAssertions() const {
-    return externalExplain(AssertionOrderSentinel);
-  }
+  TrustNode externalExplainByAssertions() const;
 
   /**
    * Writes an explanation of a constraint into the node builder.
@@ -598,22 +596,19 @@ class Constraint {
    * The constraint must have a proof.
    * The constraint cannot be an assumption.
    *
-   * This is the minimum fringe of the implication tree (excluding the constraint itself)
-   * s.t. every constraint is assertedToTheTheory() or hasEqualityEngineProof().
+   * This is the minimum fringe of the implication tree (excluding the
+   * constraint itself) s.t. every constraint is assertedToTheTheory() or
+   * hasEqualityEngineProof().
+   *
+   * All return conjuncts were asserted before this constraint.
    */
-  Node externalExplainForPropagation() const {
-    Assert(hasProof());
-    Assert(!isAssumption());
-    Assert(!isInternalAssumption());
-    return externalExplain(d_assertionOrder);
-  }
+  TrustNode externalExplainForPropagation() const;
 
   /**
    * Explain the constraint and its negation in terms of assertions.
    * The constraint must be in conflict.
    */
-  Node externalExplainConflict() const;
-
+  TrustNode externalExplainConflict() const;
 
   /** The constraint is known to be true. */
   inline bool hasProof() const {
@@ -1155,7 +1150,11 @@ private:
   bool variableDatabaseIsSetup(ArithVar v) const;
   void removeVariable(ArithVar v);
 
+  /** Get an explanation and proof for this constraint from the equality engine
+   */
   TrustNode eeExplain(ConstraintCP c) const;
+  /** Get an explanation for this constraint from the equality engine */
+  void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const;
 
   /**
    * Returns a constraint with the variable v, the constraint type t, and a value
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 6652d3ee9..760d98b1b 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1632,9 +1632,9 @@ Node TheoryArithPrivate::callDioSolver(){
 
     Node orig = Node::null();
     if(lb->isEquality()){
-      orig = lb->externalExplainByAssertions();
+      orig = lb->externalExplainByAssertions().getNode();
     }else if(ub->isEquality()){
-      orig = ub->externalExplainByAssertions();
+      orig = ub->externalExplainByAssertions().getNode();
     }else {
       orig = Constraint::externalExplainByAssertions(ub, lb);
     }
@@ -1888,7 +1888,7 @@ void TheoryArithPrivate::outputConflicts(){
         pf.print(std::cout);
         std::cout << std::endl;
       }
-      Node conflict = confConstraint->externalExplainConflict();
+      Node conflict = confConstraint->externalExplainConflict().getNode();
 
       ++conflicts;
       Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict
@@ -3797,13 +3797,13 @@ Node TheoryArithPrivate::explain(TNode n)
   ConstraintP c = d_constraintDatabase.lookup(n);
   if(c != NullConstraint){
     Assert(!c->isAssumption());
-    Node exp = c->externalExplainForPropagation();
+    Node exp = c->externalExplainForPropagation().getNode();
     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();
+      Node exp = c->externalExplainForPropagation().getNode();
       Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
       return exp;
     }else{
@@ -5006,7 +5006,7 @@ void TheoryArithPrivate::entailmentCheckBoundLookup(std::pair<Node, DeltaRationa
       ? d_partialModel.getUpperBoundConstraint(v)
       : d_partialModel.getLowerBoundConstraint(v);
     if(c != NullConstraint){
-      tmp.first = c->externalExplainByAssertions();
+      tmp.first = c->externalExplainByAssertions().getNode();
       tmp.second = c->getValue();
     }
   }