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.

2 files changed, 52 insertions, 4 deletions

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);