projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3d65b80) | patch
Add proof for pi bound lemma (#5709)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 21 Dec 2020 19:49:24 +0000 (20:49 +0100)
committerGitHub <noreply@github.com>
Mon, 21 Dec 2020 19:49:24 +0000 (20:49 +0100)
commitc9747ae3a0577498073a04de97a978e1d9464d5d
tree647c65e55b3b363747a13547b187f62ed029b3d5tree
parent3d65b80f9e19739554ddc4263757d9b98111d14ecommit | diff
Add proof for pi bound lemma (#5709)

This PR adds proofs for lemmas that introduce bounds on the constant representing pi.
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_state.cpp diff | blob | history