projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 708c5a1) | patch
Add proof for sine shift lemmas. (#5710)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 21 Dec 2020 17:16:53 +0000 (18:16 +0100)
committerGitHub <noreply@github.com>
Mon, 21 Dec 2020 17:16:53 +0000 (11:16 -0600)
commit0c2a43ab616c3670f3077758defcaa1f61cbe291
tree83cf86aa5cdd2ea0af07a980ebca0cd4af072f83tree
parent708c5a14bca031100b05000ddae65a9828d76da0commit | diff
Add proof for sine shift lemmas. (#5710)

This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and 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/sine_solver.cpp diff | blob | history