projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 39e82b2) | patch
(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Mon, 22 Feb 2021 16:25:38 +0000 (17:25 +0100)
committerGitHub <noreply@github.com>
Mon, 22 Feb 2021 16:25:38 +0000 (17:25 +0100)
commitce710ed0e88bc62a470ff7043ba3ebcc1d7ebc6e
tree3abb14d74f9f03a55eb3b0780499e619af9602d0tree
parent39e82b212bd2f957805884c24e6414289a7ec987commit | diff
(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)

This PR adds proofs for the lemmas related to the sine function in the transcendental solver.
It introduces several new proof rules with corresponding proof checkers and produces proofs in the sine solver.
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
src/theory/arith/nl/transcendental/sine_solver.h diff | blob | history
src/theory/arith/nl/transcendental/transcendental_solver.cpp diff | blob | history