From 8a2a526b2dab5d6efaf1435afcc1b7be113a86bf Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 18 Dec 2020 08:59:43 +0100
Subject: [PATCH] (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.
---
 src/expr/proof_rule.cpp                         |  1 +
 src/expr/proof_rule.h                           | 12 ++++++++++++
 src/theory/arith/nl/ext/tangent_plane_check.cpp | 16 +++++++++++++++-
 3 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 130eff0f5..22459edd4 100644
--- 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 9754735e6..b5899af66 100644
--- 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 de6176272..18c31368f 100644
--- 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);
             }
           }
         }
-- 
2.30.2