(proof-new) New proofs in arith::Constraint::externalExplain (#5176)

This commit threads proofs through the core of arith:
Constraint::externalExplain, which recursively explain arith literals.
One of the base cases here is asking the EE for an explanation, through
the congruence manager. To delay implementing proofs in
ArithCongruenceManager to a separate commit, we stub out proof
production in ArithCongruenceManager::explain for now.

5 files changed, 288 insertions, 64 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 520903562..465128b1b 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -375,11 +375,20 @@ Node ArithCongruenceManager::explainInternal(TNode internal){
   }
 }
 
-Node ArithCongruenceManager::explain(TNode external){
+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;
-  return explainInternal(internal);
+  Node exp = explainInternal(internal);
+  if (isProofEnabled())
+  {
+    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);
+  }
+  return TrustNode::mkTrustPropExp(external, exp, nullptr);
 }
 
 void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
@@ -474,6 +483,23 @@ void ArithCongruenceManager::addSharedTerm(Node x){
 
 bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
 
+std::vector<Node> andComponents(TNode an)
+{
+  auto nm = NodeManager::currentNM();
+  if (an == nm->mkConst(true))
+  {
+    return {};
+  }
+  else if (an.getKind() != Kind::AND)
+  {
+    return {an};
+  }
+  std::vector<Node> a{};
+  a.reserve(an.getNumChildren());
+  a.insert(a.end(), an.begin(), an.end());
+  return a;
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 3565d86b5..67df9237c 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -196,7 +196,7 @@ public:
   void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee);
   //--------------------------------- end initialization
 
-  Node explain(TNode literal);
+  TrustNode explain(TNode literal);
   void explain(TNode lit, NodeBuilder<>& out);
 
   void addWatchedPair(ArithVar s, TNode x, TNode y);
@@ -244,6 +244,8 @@ public:
 
 };/* class ArithCongruenceManager */
 
+std::vector<Node> andComponents(TNode an);
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 06ecb9618..ecccca35b 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -554,14 +554,11 @@ void Constraint::printProofTree(std::ostream& out, size_t depth) const
   {
     const ConstraintRule& rule = getConstraintRule();
     out << std::string(2 * depth, ' ') << "* " << getVariable() << " [";
-    if (hasLiteral())
+    out << getProofLiteral();
+    if (assertedToTheTheory())
     {
-      out << getLiteral();
+      out << " | wit: " << getWitness();
     }
-    else
-    {
-      out << "NOLIT";
-    };
     out << "]" << ' ' << getType() << ' ' << getValue() << " ("
         << getProofType() << ")";
     if (getProofType() == FarkasAP)
@@ -1522,68 +1519,208 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order)
   return safeConstructNary(nb);
 }
 
-void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{
-  Assert(hasProof());
-  Assert(!isAssumption() || assertedToTheTheory());
-  Assert(!isInternalAssumption());
+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
+{
   if (Debug.isOn("pf::arith::explain"))
   {
+    this->printProofTree(Debug("arith::pf::tree"));
     Debug("pf::arith::explain") << "Explaining: " << this << " with rule ";
     getConstraintRule().print(Debug("pf::arith::explain"));
     Debug("pf::arith::explain") << std::endl;
   }
+  Assert(hasProof());
+  Assert(!isAssumption() || assertedToTheTheory());
+  Assert(!isInternalAssumption());
+  std::shared_ptr<ProofNode> pf{};
 
-  if(assertedBefore(order)){
+  ProofNodeManager* pnm = d_database->d_pnm;
+
+  if (assertedBefore(order))
+  {
+    Debug("pf::arith::explain") << "  already asserted" << std::endl;
     nb << getWitness();
-  }else if(hasEqualityEngineProof()){
-    d_database->eeExplain(this, nb);
-  }else{
+    if (d_database->isProofEnabled())
+    {
+      pf = pnm->mkAssume(getWitness());
+      // If the witness and literal differ, prove the difference through a
+      // rewrite.
+      if (getWitness() != getProofLiteral())
+      {
+        pf = pnm->mkNode(
+            PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {getProofLiteral()});
+      }
+    }
+  }
+  else if (hasEqualityEngineProof())
+  {
+    Debug("pf::arith::explain") << "  going to ee:" << std::endl;
+    TrustNode exp = d_database->eeExplain(this);
+    if (d_database->isProofEnabled())
+    {
+      Assert(exp.getProven().getKind() == Kind::IMPLIES);
+      std::vector<std::shared_ptr<ProofNode>> hypotheses;
+      hypotheses.push_back(exp.getGenerator()->getProofFor(exp.getProven()));
+      if (exp.getNode().getKind() == Kind::AND)
+      {
+        for (const auto& h : exp.getNode())
+        {
+          hypotheses.push_back(
+              pnm->mkNode(PfRule::TRUE_INTRO, {pnm->mkAssume(h)}, {}));
+        }
+      }
+      else
+      {
+        hypotheses.push_back(pnm->mkNode(
+            PfRule::TRUE_INTRO, {pnm->mkAssume(exp.getNode())}, {}));
+      }
+      pf = pnm->mkNode(
+          PfRule::MACRO_SR_PRED_TRANSFORM, {hypotheses}, {getProofLiteral()});
+    }
+    Debug("pf::arith::explain")
+        << "    explanation: " << exp.getNode() << std::endl;
+    if (exp.getNode().getKind() == Kind::AND)
+    {
+      nb.append(exp.getNode().begin(), exp.getNode().end());
+    }
+    else
+    {
+      nb << exp.getNode();
+    }
+  }
+  else
+  {
+    Debug("pf::arith::explain") << "  recursion!" << std::endl;
     Assert(!isAssumption());
     AntecedentId p = getEndAntecedent();
     ConstraintCP antecedent = d_database->d_antecedents[p];
+    std::vector<std::shared_ptr<ProofNode>> children;
 
-    while(antecedent != NullConstraint){
+    while (antecedent != NullConstraint)
+    {
       Debug("pf::arith::explain") << "Explain " << antecedent << std::endl;
-      antecedent->externalExplain(nb, order);
+      auto pn = antecedent->externalExplain(nb, order);
+      if (d_database->isProofEnabled())
+      {
+        children.push_back(pn);
+      }
       --p;
       antecedent = d_database->d_antecedents[p];
     }
-  }
-}
 
-Node Constraint::externalExplain(AssertionOrder order) const{
-  Assert(hasProof());
-  Assert(!isAssumption() || assertedBefore(order));
-  Assert(!isInternalAssumption());
-  if(assertedBefore(order)){
-    return getWitness();
-  }else if(hasEqualityEngineProof()){
-    return d_database->eeExplain(this);
-  }else{
-    Assert(hasFarkasProof() || hasIntHoleProof() || hasIntTightenProof() || hasTrichotomyProof());
-    Assert(!antecentListIsEmpty());
-    //Force the selection of the layer above if the node is
-    // assertedToTheTheory()!
-
-    AntecedentId listEnd = getEndAntecedent();
-    if(antecedentListLengthIsOne()){
-      ConstraintCP antecedent = d_database->d_antecedents[listEnd];
-      return antecedent->externalExplain(order);
-    }else{
-      NodeBuilder<> nb(kind::AND);
-      Assert(!isAssumption());
-
-      AntecedentId p = listEnd;
-      ConstraintCP antecedent = d_database->d_antecedents[p];
-      while(antecedent != NullConstraint){
-        antecedent->externalExplain(nb, order);
-        --p;
-        antecedent = d_database->d_antecedents[p];
+    if (d_database->isProofEnabled())
+    {
+      switch (getProofType())
+      {
+        case ArithProofType::AssumeAP:
+        case ArithProofType::EqualityEngineAP:
+        {
+          Unreachable() << "These should be handled above";
+          break;
+        }
+        case ArithProofType::FarkasAP:
+        {
+          // Per docs in constraint.h,
+          // the 0th farkas coefficient is for the negation of the deduced
+          // constraint the 1st corresponds to the last antecedent the nth
+          // corresponds to the first antecedent Then, the farkas coefficients
+          // and the antecedents are in the same order.
+
+          // Enumerate child proofs (negation included) in d_farkasCoefficients
+          // order
+          std::vector<std::shared_ptr<ProofNode>> farkasChildren;
+          farkasChildren.push_back(
+              pnm->mkAssume(getNegation()->getProofLiteral()));
+          farkasChildren.insert(
+              farkasChildren.end(), children.rbegin(), children.rend());
+
+          NodeManager* nm = NodeManager::currentNM();
+
+          // Enumerate d_farkasCoefficients as nodes.
+          std::vector<Node> farkasCoeffs;
+          for (Rational r : *getFarkasCoefficients())
+          {
+            farkasCoeffs.push_back(nm->mkConst<Rational>(r));
+          }
+
+          // Apply the scaled-sum rule.
+          std::shared_ptr<ProofNode> sumPf =
+              pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS,
+                          farkasChildren,
+                          farkasCoeffs);
+
+          // Provable rewrite the result
+          auto botPf = pnm->mkNode(
+              PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)});
+
+          // Scope out the negated constraint, yielding a proof of the
+          // constraint.
+          std::vector<Node> assump{getNegation()->getProofLiteral()};
+          auto maybeDoubleNotPf = pnm->mkScope(botPf, assump, false);
+
+          // No need to ensure that the expected node aggrees with `assump`
+          // because we are not providing an expected node.
+          //
+          // Prove that this is the literal (may need to clean a double-not)
+          pf = pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
+                           {maybeDoubleNotPf},
+                           {getProofLiteral()});
+
+          break;
+        }
+        case ArithProofType::IntTightenAP:
+        {
+          if (isUpperBound())
+          {
+            pf = pnm->mkNode(
+                PfRule::INT_TIGHT_UB, children, {}, getProofLiteral());
+          }
+          else if (isLowerBound())
+          {
+            pf = pnm->mkNode(
+                PfRule::INT_TIGHT_LB, children, {}, getProofLiteral());
+          }
+          else
+          {
+            Unreachable();
+          }
+          break;
+        }
+        case ArithProofType::IntHoleAP:
+        {
+          pf = pnm->mkNode(PfRule::INT_TRUST,
+                           children,
+                           {getProofLiteral()},
+                           getProofLiteral());
+          break;
+        }
+        case ArithProofType::TrichotomyAP:
+        {
+          pf = pnm->mkNode(PfRule::ARITH_TRICHOTOMY,
+                           children,
+                           {getProofLiteral()},
+                           getProofLiteral());
+          break;
+        }
+        case ArithProofType::InternalAssumeAP:
+        case ArithProofType::NoAP:
+        default:
+        {
+          Unreachable() << getProofType()
+                        << " should not be visible in explanation";
+          break;
+        }
       }
-      return nb;
     }
   }
+  return pf;
 }
 
 Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){
@@ -1706,14 +1843,11 @@ ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t
     }
   }
 }
-Node ConstraintDatabase::eeExplain(const Constraint* const c) const{
-  Assert(c->hasLiteral());
-  return d_congruenceManager.explain(c->getLiteral());
-}
 
-void ConstraintDatabase::eeExplain(const Constraint* const c, NodeBuilder<>& nb) const{
+TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const
+{
   Assert(c->hasLiteral());
-  d_congruenceManager.explain(c->getLiteral(), nb);
+  return d_congruenceManager.explain(c->getLiteral());
 }
 
 bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
@@ -1740,6 +1874,58 @@ void Constraint::setLiteral(Node n) {
   map.insert(make_pair(d_literal, this));
 }
 
+Node Constraint::getProofLiteral() const
+{
+  Assert(d_database != nullptr);
+  Assert(d_database->d_avariables.hasNode(d_variable));
+  Node varPart = d_database->d_avariables.asNode(d_variable);
+  Kind cmp;
+  bool neg = false;
+  switch (d_type)
+  {
+    case ConstraintType::UpperBound:
+    {
+      if (d_value.infinitesimalIsZero())
+      {
+        cmp = Kind::LEQ;
+      }
+      else
+      {
+        cmp = Kind::LT;
+      }
+      break;
+    }
+    case ConstraintType::LowerBound:
+    {
+      if (d_value.infinitesimalIsZero())
+      {
+        cmp = Kind::GEQ;
+      }
+      else
+      {
+        cmp = Kind::GT;
+      }
+      break;
+    }
+    case ConstraintType::Equality:
+    {
+      cmp = Kind::EQUAL;
+      break;
+    }
+    case ConstraintType::Disequality:
+    {
+      cmp = Kind::EQUAL;
+      neg = true;
+      break;
+    }
+    default: Unreachable() << d_type;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node constPart = nm->mkConst<Rational>(d_value.getNoninfinitesimalPart());
+  Node posLit = nm->mkNode(cmp, varPart, constPart);
+  return neg ? posLit.negate() : posLit;
+}
+
 void implies(std::vector<Node>& out, ConstraintP a, ConstraintP b){
   Node la = a->getLiteral();
   Node lb = b->getLiteral();
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 0afc0bc2f..f78d8d22f 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -92,6 +92,7 @@
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/proof_macros.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace theory {
@@ -463,6 +464,14 @@ class Constraint {
     return d_literal;
   }
 
+  /** Gets a literal in the normal form suitable for proofs.
+   * That is, (sum of non-const monomials) >< const.
+   *
+   * This is a sister method to `getLiteral`, which returns a normal form
+   * literal, suitable for external solving use.
+   */
+  Node getProofLiteral() const;
+
   /**
    * Set the node as having a proof and being an assumption.
    * The node must be assertedToTheTheory().
@@ -848,7 +857,6 @@ class Constraint {
   static std::pair<int, int> unateFarkasSigns(ConstraintCP a, ConstraintCP b);
 
   Node externalExplain(AssertionOrder order) const;
-
   /**
    * Returns an explanation of that was assertedBefore(order).
    * The constraint must have a proof.
@@ -857,7 +865,8 @@ class Constraint {
    * This is the minimum fringe of the implication tree
    * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
    */
-  void externalExplain(NodeBuilder<>& nb, AssertionOrder order) const;
+  std::shared_ptr<ProofNode> externalExplain(NodeBuilder<>& nb,
+                                             AssertionOrder order) const;
 
   static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
 
@@ -1144,8 +1153,7 @@ private:
   bool variableDatabaseIsSetup(ArithVar v) const;
   void removeVariable(ArithVar v);
 
-  Node eeExplain(ConstraintCP c) const;
-  void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const;
+  TrustNode eeExplain(ConstraintCP c) const;
 
   /**
    * Returns a constraint with the variable v, the constraint type t, and a value
@@ -1208,7 +1216,9 @@ private:
   /** AntecendentID must be in range. */
   ConstraintCP getAntecedent(AntecedentId p) const;
 
-private:
+  bool isProofEnabled() const { return d_pnm != nullptr; }
+
+ private:
   /** returns true if cons is now in conflict. */
   bool handleUnateProp(ConstraintP ant, ConstraintP cons);
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d2293131f..1a13f44fa 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3865,12 +3865,12 @@ Node TheoryArithPrivate::explain(TNode n)
       Debug("arith::explain") << "this is a strange mismatch" << n << endl;
       Assert(d_congruenceManager.canExplain(n));
       Debug("arith::explain") << "this is a strange mismatch" << n << endl;
-      return d_congruenceManager.explain(n);
+      return d_congruenceManager.explain(n).getNode();
     }
   }else{
     Assert(d_congruenceManager.canExplain(n));
     Debug("arith::explain") << "dm explanation" << n << endl;
-    return d_congruenceManager.explain(n);
+    return d_congruenceManager.explain(n).getNode();
   }
 }
 
@@ -3930,7 +3930,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) {
 
       outputPropagate(toProp);
     }else if(constraint->negationHasProof()){
-      Node exp = d_congruenceManager.explain(toProp);
+      Node exp = d_congruenceManager.explain(toProp).getNode();
       Node notNormalized = normalized.getKind() == NOT ?
         normalized[0] : normalized.notNode();
       Node lp = flattenAnd(exp.andNode(notNormalized));