(proof-new) Add proof for tangent plane lemmas (#5700)

This PR adds a proof for the tangent plane lemmas from nl-ext.
As this lemma uses some insight about the tangent plane of a multiplication term, this PR adds a new proof rule.

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 130eff0f5a85ac10e9706f9be8284825224102b2..22459edd49baf94f962f1ea1b2782f4200f97b5e 100644 (file)
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -158,6 +158,7 @@ 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_TANGENT: return "ARITH_MULT_TANGENT";
     case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 9754735e6fe2a0063ac0e11aaf7d9e0417a8c46e..b5899af665e59d91d89f050292ebf67aa0237e86 100644 (file)
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1092,6 +1092,18 @@ enum class PfRule : uint32_t
   // Conclusion: (Q)
   INT_TRUST,
 
+  //======== Multiplication tangent plane
+  // Children: none
+  // Arguments: (t, x, y, a, b, sgn)
+  // ---------------------
+  // Conclusion:
+  //   sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y b)))
+  //   sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) (>= y b)))
+  // Where x,y are real terms (variables or extended terms), t = (* x y)
+  // (possibly under rewriting), a,b are real constants, and sgn is either -1
+  // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b
+  ARITH_MULT_TANGENT,
+
   //================================================= Unknown rule
   UNKNOWN,
 };

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index de6176272e7dc42f197e0c22e8a8f81152f5fd39..18c31368fedf3475c910df307f23d25efd21d9c5 100644 (file)
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -132,8 +132,22 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
                           Kind::AND, nm->mkNode(Kind::GEQ, a, a_v), b2)));
               Trace("nl-ext-tplanes")
                   << "Tangent plane lemma : " << tlem << std::endl;
+              CDProof* proof = nullptr;
+              if (d_data->isProofEnabled())
+              {
+                proof = d_data->getProof();
+                proof->addStep(tlem,
+                               PfRule::ARITH_MULT_TANGENT,
+                               {},
+                               {t,
+                                a,
+                                b,
+                                a_v,
+                                b_v,
+                                nm->mkConst(Rational(d == 0 ? -1 : 1))});
+              }
               d_data->d_im.addPendingArithLemma(
-                  tlem, InferenceId::NL_TANGENT_PLANE, nullptr, asWaitingLemmas);
+                  tlem, InferenceId::NL_TANGENT_PLANE, proof, asWaitingLemmas);
             }
           }
         }