projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ddf6479) | patch
(proof-new) Add proofs for exponential functions (#5956)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 22 Feb 2021 21:27:30 +0000 (22:27 +0100)
committerGitHub <noreply@github.com>
Mon, 22 Feb 2021 21:27:30 +0000 (15:27 -0600)
commit580f3e93c2cc4564e6fa87d07426dc1ff87224e4
tree344bdfaa5a9dfbe96131b7379f7fccd7533b8b36tree
parentddf647904de838e8e6ee266ad13de8a6a90250c8commit | diff
(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.
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/arith/nl/transcendental/exponential_solver.cpp diff | blob | history
src/theory/arith/nl/transcendental/exponential_solver.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