Add proof for monomial bounds check (#5965)

This PR adds proofs for a nonlinear refinement lemma that deals with multiplication of inequalities with some term. This lemma is split into two proof rules for positive or negative factors.

4 files changed, 70 insertions, 4 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index bead7397a..cc5613057 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -159,6 +159,8 @@ const char* toString(PfRule id)
     case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
     case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
     case PfRule::INT_TRUST: return "INT_TRUST";
+    case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS";
+    case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";
     case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
     case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
     case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index d42175fab..bf6f1d6ae 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1092,6 +1092,22 @@ enum class PfRule : uint32_t
   // Conclusion: (Q)
   INT_TRUST,
 
+  //======== Multiplication with positive factor
+  // Children: none
+  // Arguments: (m, orig, lhs, rel, rhs)
+  // ---------------------
+  // Conclusion: (=> (and (> m 0) (rel lhs rhs)) (rel (* m lhs) (* m rhs)))
+  // Where orig is the origin that implies (rel lhs rhs) and rel is a relation
+  // symbol.
+  ARITH_MULT_POS,
+  //======== Multiplication with negative factor
+  // Children: none
+  // Arguments: (m, orig, (rel lhs rhs))
+  // ---------------------
+  // Conclusion: (=> (and (< m 0) (rel lhs rhs)) (rel_inv (* m lhs) (* m rhs)))
+  // Where orig is the origin that implies (rel lhs rhs) and rel is a relation
+  // symbol and rel_inv the inverted relation symbol.
+  ARITH_MULT_NEG,
   //======== Multiplication tangent plane
   // Children: none
   // Arguments: (t, x, y, a, b, sgn)
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 46b1c991e..5ae898bd2 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -317,11 +317,20 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
             Trace("nl-ext-bound-lemma")
                 << "*** Bound inference lemma : " << iblem
                 << " (pre-rewrite : " << pr_iblem << ")" << std::endl;
-            // Trace("nl-ext-bound-lemma") << "       intro new
-            // monomials = " << introNewTerms << std::endl;
+            CDProof* proof = nullptr;
+            if (d_data->isProofEnabled())
+            {
+              proof = d_data->getProof();
+              proof->addStep(
+                  iblem,
+                  mmv_sign == 1 ? PfRule::ARITH_MULT_POS
+                                : PfRule::ARITH_MULT_NEG,
+                  {},
+                  {mult, d_ci_exp[x][coeff][rhs], nm->mkNode(type, t, rhs)});
+            }
             d_data->d_im.addPendingLemma(iblem,
                                          InferenceId::ARITH_NL_INFER_BOUNDS_NT,
-                                         nullptr,
+                                         proof,
                                          introNewTerms);
           }
         }
diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp
index 8c594f1df..a0c5d2021 100644
--- a/src/theory/arith/nl/ext/proof_checker.cpp
+++ b/src/theory/arith/nl/ext/proof_checker.cpp
@@ -27,6 +27,8 @@ namespace nl {
 
 void ExtProofRuleChecker::registerTo(ProofChecker* pc)
 {
+  pc->registerChecker(PfRule::ARITH_MULT_POS, this);
+  pc->registerChecker(PfRule::ARITH_MULT_NEG, this);
   pc->registerChecker(PfRule::ARITH_MULT_TANGENT, this);
 }
 
@@ -45,7 +47,44 @@ Node ExtProofRuleChecker::checkInternal(PfRule id,
   {
     Trace("nl-ext-checker") << "\t" << c << std::endl;
   }
-  if (id == PfRule::ARITH_MULT_TANGENT)
+  if (id == PfRule::ARITH_MULT_POS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 3);
+    Node mult = args[0];
+    Node orig = args[1];
+    Kind rel = args[2].getKind();
+    Assert(rel == Kind::EQUAL || rel == Kind::DISTINCT || rel == Kind::LT
+           || rel == Kind::LEQ || rel == Kind::GT || rel == Kind::GEQ);
+    Node lhs = args[2][0];
+    Node rhs = args[2][1];
+    return Rewriter::rewrite(nm->mkNode(
+        Kind::IMPLIES,
+        nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GT, mult, zero), orig}),
+        nm->mkNode(rel,
+                   nm->mkNode(Kind::MULT, mult, lhs),
+                   nm->mkNode(Kind::MULT, mult, rhs))));
+  }
+  else if (id == PfRule::ARITH_MULT_NEG)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 3);
+    Node mult = args[0];
+    Node orig = args[1];
+    Kind rel = args[2].getKind();
+    Assert(rel == Kind::EQUAL || rel == Kind::DISTINCT || rel == Kind::LT
+           || rel == Kind::LEQ || rel == Kind::GT || rel == Kind::GEQ);
+    Kind rel_inv = (rel == Kind::DISTINCT ? rel : reverseRelationKind(rel));
+    Node lhs = args[2][0];
+    Node rhs = args[2][1];
+    return Rewriter::rewrite(nm->mkNode(
+        Kind::IMPLIES,
+        nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::LT, mult, zero), orig}),
+        nm->mkNode(rel_inv,
+                   nm->mkNode(Kind::MULT, mult, lhs),
+                   nm->mkNode(Kind::MULT, mult, rhs))));
+  }
+  else if (id == PfRule::ARITH_MULT_TANGENT)
   {
     Assert(children.empty());
     Assert(args.size() == 6);