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

5 files changed, 37 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;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d185049e0..2c480da3a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -68,6 +68,7 @@ set(regress_0_tests
   regress0/arith/mod-simp.smt2
   regress0/arith/mod.01.smt2
   regress0/arith/mult.01.smt2
+  regress0/arith/non-normal.smt2
   regress0/arr1.smt2
   regress0/arr1.smtv1.smt2
   regress0/arr2.smtv1.smt2
diff --git a/test/regress/regress0/arith/non-normal.smt2 b/test/regress/regress0/arith/non-normal.smt2
new file mode 100644
index 000000000..389bd6d2b
--- /dev/null
+++ b/test/regress/regress0/arith/non-normal.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --proof-new-eager-checking
+; EXPECT: sat
+(set-logic QF_UFLRA)
+(declare-fun v1 () Real)
+(declare-fun v2 () Real)
+(declare-fun f1 (Real) Real)
+(declare-fun f0 (Real Real) Real)
+(declare-fun p0 (Real Real) Bool)
+(assert 
+(ite 
+  (or (= 0.0 v2) (> 1 (ite (< (- (- v1)) 1.0) 1.0 (ite (p0 0.0 v1) 0.0 1.0)))) 
+  (= 0.0 (ite (= 1.0 (f1 0.0)) 0.0 (f1 1.0))) 
+  (and 
+    (= 1.0 (ite (= 0.0 (f1 1.0)) v2 (- 1.0))) 
+    (=> (not (p0 0.0 (- (- (- v2))))) (= 1.0 (ite (= 1.0 v2) (ite (= 0 (f0 0.0 1.0)) 1.0 (f0 0.0 (- v2 (- v1)))) 0.0))))))
+(check-sat)