(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.

2 files changed, 13 insertions, 0 deletions

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,
 };