projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4711be9) | patch
Add trans secant proofs. (#5957)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 23 Feb 2021 04:35:46 +0000 (05:35 +0100)
committerGitHub <noreply@github.com>
Tue, 23 Feb 2021 04:35:46 +0000 (22:35 -0600)
commitf1c384dff82bffa56b9cf9ba18ec1f35aa529b12
tree5049b8dda3ad679e6b164c50daa458649d0515aftree
parent4711be9f5f65d5ea61321bc80d31e030536de81bcommit | 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.
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/arith/nl/transcendental/proof_checker.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.cpp diff | blob | history