Add trans secant proofs. (#5957)

This PR adds proofs for secant lemmas in the transcendental lemmas for both exponential and sine functions.
It also adds proof rules and corresponding proof checkers.

3 files changed, 120 insertions, 7 deletions

diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp
index 6dc2df201..e09c8509a 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.cpp
+++ b/src/theory/arith/nl/transcendental/proof_checker.cpp
@@ -64,7 +64,10 @@ void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::ARITH_TRANS_EXP_POSITIVITY, this);
   pc->registerChecker(PfRule::ARITH_TRANS_EXP_SUPER_LIN, this);
   pc->registerChecker(PfRule::ARITH_TRANS_EXP_ZERO, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG, this);
   pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_BELOW, this);
+  pc->registerChecker(PfRule::ARITH_TRANS_SINE_BOUNDS, this);
   pc->registerChecker(PfRule::ARITH_TRANS_SINE_SHIFT, this);
   pc->registerChecker(PfRule::ARITH_TRANS_SINE_SYMMETRY, this);
   pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_ZERO, this);
@@ -133,6 +136,62 @@ Node TranscendentalProofRuleChecker::checkInternal(
     Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
     return nm->mkNode(EQUAL, args[0].eqNode(zero), e.eqNode(one));
   }
+  else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 4);
+    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+           && args[0].getConst<Rational>().isIntegral());
+    Assert(args[1].getType().isReal());
+    Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL);
+    Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL);
+    std::uint64_t d =
+        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+    Node t = args[1];
+    Node l = args[2];
+    Node u = args[3];
+    TaylorGenerator tg;
+    TaylorGenerator::ApproximationBounds bounds;
+    tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
+    Node evall = Rewriter::rewrite(
+        bounds.d_upperPos.substitute(tg.getTaylorVariable(), l));
+    Node evalu = Rewriter::rewrite(
+        bounds.d_upperPos.substitute(tg.getTaylorVariable(), u));
+    Node evalsecant = mkSecant(t, l, u, evall, evalu);
+    Node lem = nm->mkNode(
+        Kind::IMPLIES,
+        mkBounds(t, l, u),
+        nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
+    return Rewriter::rewrite(lem);
+  }
+  else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 4);
+    Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+           && args[0].getConst<Rational>().isIntegral());
+    Assert(args[1].getType().isReal());
+    Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL);
+    Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL);
+    std::uint64_t d =
+        args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+    Node t = args[1];
+    Node l = args[2];
+    Node u = args[3];
+    TaylorGenerator tg;
+    TaylorGenerator::ApproximationBounds bounds;
+    tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
+    Node evall = Rewriter::rewrite(
+        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
+    Node evalu = Rewriter::rewrite(
+        bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
+    Node evalsecant = mkSecant(t, l, u, evall, evalu);
+    Node lem = nm->mkNode(
+        Kind::IMPLIES,
+        mkBounds(t, l, u),
+        nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
+    return Rewriter::rewrite(lem);
+  }
   else if (id == PfRule::ARITH_TRANS_EXP_APPROX_BELOW)
   {
     Assert(children.empty());
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 0548c6a41..e58da1aad 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -323,14 +323,14 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
     Node v_pab = r == 0 ? mvb.first : mvb.second;
     if (!v_pab.isNull())
     {
-      Trace("nl-ext-tftp-debug2")
-          << "...model value of " << pab << " is " << v_pab << std::endl;
+      Trace("nl-trans") << "...model value of " << pab << " is " << v_pab
+                        << std::endl;
 
       Assert(v_pab.isConst());
       Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab);
-      Trace("nl-ext-tftp-debug2") << "...compare : " << comp << std::endl;
+      Trace("nl-trans") << "...compare : " << comp << std::endl;
       Node compr = Rewriter::rewrite(comp);
-      Trace("nl-ext-tftp-debug2") << "...got : " << compr << std::endl;
+      Trace("nl-trans") << "...got : " << compr << std::endl;
       if (compr == d_tstate.d_true)
       {
         poly_approx_c = Rewriter::rewrite(v_pab);
@@ -374,8 +374,8 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
   // Figure 3: P( c )
   if (is_tangent || is_secant)
   {
-    Trace("nl-ext-tftp-debug2")
-        << "...poly approximation at c is " << poly_approx_c << std::endl;
+    Trace("nl-trans") << "...poly approximation at c is " << poly_approx_c
+                      << std::endl;
   }
   else
   {
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 35967a39a..76c3d5357 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -319,7 +319,61 @@ NlLemma TranscendentalState::mkSecantLemma(TNode lower,
   lem = Rewriter::rewrite(lem);
   Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl;
   Assert(d_model.computeAbstractModelValue(lem) == d_false);
-  return NlLemma(InferenceId::ARITH_NL_T_SECANT, lem);
+  CDProof* proof = nullptr;
+  if (isProofEnabled())
+  {
+    proof = getProof();
+    if (tf.getKind() == Kind::EXPONENTIAL)
+    {
+      if (csign == 1)
+      {
+        proof->addStep(
+            lem,
+            PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS,
+            {},
+            {nm->mkConst<Rational>(2 * actual_d), tf[0], lower, upper});
+      }
+      else
+      {
+        proof->addStep(
+            lem,
+            PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG,
+            {},
+            {nm->mkConst<Rational>(2 * actual_d), tf[0], lower, upper});
+      }
+    }
+    else if (tf.getKind() == Kind::SINE)
+    {
+      if (convexity == Convexity::CONCAVE)
+      {
+        proof->addStep(lem,
+                       PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS,
+                       {},
+                       {nm->mkConst<Rational>(2 * actual_d),
+                        tf[0],
+                        lower,
+                        upper,
+                        lapprox,
+                        uapprox
+
+                       });
+      }
+      else
+      {
+        proof->addStep(lem,
+                       PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG,
+                       {},
+                       {nm->mkConst<Rational>(2 * actual_d),
+                        tf[0],
+                        lower,
+                        upper,
+                        lapprox,
+                        uapprox});
+      }
+    }
+  }
+  return NlLemma(
+      InferenceId::ARITH_NL_T_SECANT, lem, LemmaProperty::NONE, proof);
 }
 
 void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,