diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-23 05:35:46 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-22 22:35:46 -0600 |
| commit | f1c384dff82bffa56b9cf9ba18ec1f35aa529b12 (patch) | |
| tree | 5049b8dda3ad679e6b164c50daa458649d0515af /src/expr/proof_rule.cpp | |
| parent | 4711be9f5f65d5ea61321bc80d31e030536de81b (diff) | |
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.
Diffstat (limited to 'src/expr/proof_rule.cpp')
| -rw-r--r-- | src/expr/proof_rule.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
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"; |