Bugfix: proofs for props of non-normal arith lits (#5702)

Arith has a normal form for literals, which the rewriter computes.

Nonetheless, arith sometimes gets (and ultimately propagates) non-normal
literals. It normalizes them internally and goes about its business.

However, when asked for an explanation, it must prove the non-normal
literal, rather than the normal one.

Also includes a regression for the bug, courtesy of Andy.

Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu

3 files changed, 20 insertions, 8 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 03d9c50e9..c1db8e55a 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -1507,7 +1507,7 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){
   return externalExplain(b, AssertionOrderSentinel);
 }
 
-TrustNode Constraint::externalExplainForPropagation() const
+TrustNode Constraint::externalExplainForPropagation(TNode lit) const
 {
   Assert(hasProof());
   Assert(!isAssumption());
@@ -1517,6 +1517,9 @@ TrustNode Constraint::externalExplainForPropagation() const
   Node n = safeConstructNary(nb);
   if (d_database->isProofEnabled())
   {
+    // Check that the literal we're explaining via this constraint actually
+    // matches the constraint's canonical literal.
+    Assert(Rewriter::rewrite(lit) == getLiteral());
     std::vector<Node> assumptions;
     if (n.getKind() == Kind::AND)
     {
@@ -1526,18 +1529,18 @@ TrustNode Constraint::externalExplainForPropagation() const
     {
       assumptions.push_back(n);
     }
-    if (getProofLiteral() != getLiteral())
+    if (getProofLiteral() != lit)
     {
       pfFromAssumptions = d_database->d_pnm->mkNode(
-          PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {getLiteral()});
+          PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {lit});
     }
     auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions);
     return d_database->d_pfGen->mkTrustedPropagation(
-        getLiteral(), safeConstructNary(Kind::AND, assumptions), pf);
+        lit, safeConstructNary(Kind::AND, assumptions), pf);
   }
   else
   {
-    return TrustNode::mkTrustPropExp(getLiteral(), n);
+    return TrustNode::mkTrustPropExp(lit, n);
   }
 }
 
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 952879182..70b2cad20 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -601,8 +601,17 @@ class Constraint {
    * hasEqualityEngineProof().
    *
    * All return conjuncts were asserted before this constraint.
+   *
+   * Requires the given node to rewrite to the canonical literal for this
+   * constraint.
+   *
+   * @params n the literal to prove
+   *           n must rewrite to the constraint's canonical literal
+   *
+   * @returns a trust node of the form:
+   *         (=> explanation n)
    */
-  TrustNode externalExplainForPropagation() const;
+  TrustNode externalExplainForPropagation(TNode n) const;
 
   /**
    * Explain the constraint and its negation in terms of assertions.
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index ce0445d1f..d1068c6ac 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3848,12 +3848,12 @@ TrustNode TheoryArithPrivate::explain(TNode n)
   TrustNode exp;
   if(c != NullConstraint){
     Assert(!c->isAssumption());
-    exp = c->externalExplainForPropagation();
+    exp = c->externalExplainForPropagation(n);
     Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
   }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
     c = d_assertionsThatDoNotMatchTheirLiterals[n];
     if(!c->isAssumption()){
-      exp = c->externalExplainForPropagation();
+      exp = c->externalExplainForPropagation(n);
       Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
     }else{
       Debug("arith::explain") << "this is a strange mismatch" << n << endl;