(proof-new) Add proofs for exponential functions (#5956)

This PR adds proofs for lemmas concerned with the exponential function. If also adds the necessary proof rules and corresponding proof checker.

2 files changed, 43 insertions, 0 deletions

diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index a5dde78ab..110d9467e 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -162,6 +162,13 @@ const char* toString(PfRule id)
     case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
     case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
     case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI";
+    case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG";
+    case PfRule::ARITH_TRANS_EXP_POSITIVITY:
+      return "ARITH_TRANS_EXP_POSITIVITY";
+    case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN";
+    case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO";
+    case PfRule::ARITH_TRANS_EXP_APPROX_BELOW:
+      return "ARITH_TRANS_EXP_APPROX_BELOW";
     case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS";
     case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT";
     case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 28ea24533..10801648f 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1113,6 +1113,42 @@ enum class PfRule : uint32_t
   // Where l (u) is a valid lower (upper) bound on pi.
   ARITH_TRANS_PI,
 
+  //======== Exp at negative values
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (= (< t 0) (< (exp t) 1))
+  ARITH_TRANS_EXP_NEG,
+  //======== Exp is always positive
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (> (exp t) 0)
+  ARITH_TRANS_EXP_POSITIVITY,
+  //======== Exp grows super-linearly for positive values
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (or (<= t 0) (> exp(t) (+ t 1)))
+  ARITH_TRANS_EXP_SUPER_LIN,
+  //======== Exp at zero
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: (= (= t 0) (= (exp t) 1))
+  ARITH_TRANS_EXP_ZERO,
+  //======== Exp is approximated from below
+  // Children: none
+  // Arguments: (d, t)
+  // ---------------------
+  // Conclusion: (>= (exp t) (maclaurin exp d t))
+  // Where d is an odd positive number and (maclaurin exp d t) is the d'th
+  // taylor polynomial at zero (also called the Maclaurin series) of the
+  // exponential function evaluated at t. The Maclaurin series for the
+  // exponential function is the following:
+  //   e^x = \sum_{n=0}^{\infty} x^n / n!
+  ARITH_TRANS_EXP_APPROX_BELOW,
+
   //======== Sine is always between -1 and 1
   // Children: none
   // Arguments: (t)