From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 29 Oct 2021 22:37:39 +0000 (-0700)
Subject: Fix proof of nl lemma for a corner case (#7530)
X-Git-Tag: cvc5-1.0.0~926
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e86e6c20286af0eece976e7560b3dc400384f9c7;p=cvc5.git

Fix proof of nl lemma for a corner case (#7530)

This PR fixes the proof generated for the nonlinear monomial bounds check lemmas. In some cases, it implies an equality (multiplied by a monomial) not from the equality but from the two weak inequalities. We now properly detect this special case and add a rather involved proof.
Fixes cvc5/cvc5-projects#326.
---

diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 31bc4c662..bb6a2a5c3 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -321,25 +321,80 @@ void MonomialBoundsCheck::checkBounds(const std::vector<Node>& asserts,
             if (d_data->isProofEnabled())
             {
               proof = d_data->getProof();
+              Node simpleeq = nm->mkNode(type, t, rhs);
               // this is iblem, but uses (type t rhs) instead of the original
               // variant (which is identical under rewriting)
               // we first infer the "clean" version of the lemma and then
               // use MACRO_SR_PRED_TRANSFORM to rewrite
-              Node tmplem = nm->mkNode(
-                  Kind::IMPLIES,
-                  nm->mkNode(Kind::AND,
-                             nm->mkNode(mmv_sign == 1 ? Kind::GT : Kind::LT,
-                                        mult,
-                                        d_data->d_zero),
-                             nm->mkNode(type, t, rhs)),
-                  infer);
+              Node tmplem = nm->mkNode(Kind::IMPLIES,
+                                       nm->mkNode(Kind::AND, exp[0], simpleeq),
+                                       infer);
               proof->addStep(tmplem,
                              mmv_sign == 1 ? PfRule::ARITH_MULT_POS
                                            : PfRule::ARITH_MULT_NEG,
                              {},
-                             {mult, nm->mkNode(type, t, rhs)});
-              proof->addStep(
-                  iblem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {iblem});
+                             {mult, simpleeq});
+              theory::Rewriter* rew = d_data->d_env.getRewriter();
+              if (type == Kind::EQUAL
+                  && (rew->rewrite(simpleeq) != rew->rewrite(exp[1])))
+              {
+                // it is not identical under rewriting and we need to do some work here
+                // The proof looks like this:
+                // (SCOPE
+                //   (MODUS_PONENS
+                //     <tmplem>
+                //     (AND_INTRO
+                //       <first premise of iblem>
+                //       (ARITH_TRICHOTOMY ***
+                //         (AND_ELIM <second premise of iblem> 1)
+                //         (AND_ELIM <second premise of iblem> 2)
+                //       )
+                //     )
+                //   )
+                //   :args <the two premises of iblem>
+                // )
+                // ***: the result of the AND_ELIM are rewritten forms of what
+                // ARITH_TRICHOTOMY expects, and also their order is not clear.
+                // Hence, we apply MACRO_SR_PRED_TRANSFORM to them, and check
+                // which corresponds to which subterm of the premise.
+                proof->addStep(exp[1][0],
+                               PfRule::AND_ELIM,
+                               {exp[1]},
+                               {nm->mkConst(Rational(0))});
+                proof->addStep(exp[1][1],
+                               PfRule::AND_ELIM,
+                               {exp[1]},
+                               {nm->mkConst(Rational(1))});
+                Node lb = nm->mkNode(Kind::GEQ, simpleeq[0], simpleeq[1]);
+                Node rb = nm->mkNode(Kind::LEQ, simpleeq[0], simpleeq[1]);
+                if (rew->rewrite(lb) == rew->rewrite(exp[1][0]))
+                {
+                  proof->addStep(
+                      lb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][0]}, {lb});
+                  proof->addStep(
+                      rb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][1]}, {rb});
+                }
+                else
+                {
+                  proof->addStep(
+                      lb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][1]}, {lb});
+                  proof->addStep(
+                      rb, PfRule::MACRO_SR_PRED_TRANSFORM, {exp[1][0]}, {rb});
+                }
+                proof->addStep(
+                    simpleeq, PfRule::ARITH_TRICHOTOMY, {lb, rb}, {simpleeq});
+                proof->addStep(
+                    tmplem[0], PfRule::AND_INTRO, {exp[0], simpleeq}, {});
+                proof->addStep(
+                    tmplem[1], PfRule::MODUS_PONENS, {tmplem[0], tmplem}, {});
+                proof->addStep(
+                    iblem, PfRule::SCOPE, {tmplem[1]}, {exp[0], exp[1]});
+              }
+              else
+              {
+                proof->addStep(
+                    iblem, PfRule::MACRO_SR_PRED_TRANSFORM, {tmplem}, {iblem});
+              }
             }
             d_data->d_im.addPendingLemma(iblem,
                                          InferenceId::ARITH_NL_INFER_BOUNDS_NT,
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c6dcfa967..6df6ebe76 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -867,6 +867,7 @@ set(regress_0_tests
   regress0/proofs/open-pf-rederivation.smt2
   regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
   regress0/proofs/project-issue330-eqproof.smt2
+  regress0/proofs/proj-issue326-nl-bounds-check.smt2
   regress0/proofs/qgu-fuzz-1-bool-sat.smt2
   regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
   regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
diff --git a/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2
new file mode 100644
index 000000000..bc10e9cac
--- /dev/null
+++ b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2
@@ -0,0 +1,13 @@
+; EXPECT: unknown
+(set-logic ALL)
+(set-option :check-proofs true)
+(set-option :proof-check eager)
+(declare-const x Real)
+(assert
+    (and
+        (< 1.0 x)
+        (<= x (/ 0.0 0.0 x))
+        (<= (/ 0.0 0.0 x) x)
+    )
+)
+(check-sat)