From f1c384dff82bffa56b9cf9ba18ec1f35aa529b12 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 23 Feb 2021 05:35:46 +0100 Subject: 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. --- src/expr/proof_rule.cpp | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/expr/proof_rule.cpp') diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 110d9467e..85463d2d9 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -167,6 +167,10 @@ const char* toString(PfRule id) 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_ABOVE_NEG: + return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG"; + case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS: + return "ARITH_TRANS_EXP_APPROX_ABOVE_POS"; case PfRule::ARITH_TRANS_EXP_APPROX_BELOW: return "ARITH_TRANS_EXP_APPROX_BELOW"; case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS"; -- cgit v1.2.3