projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: de14432) | patch
Fix transcendental secant plane lemmas (#5525)
authorGereon Kremer <gkremer@stanford.edu>
Wed, 25 Nov 2020 18:07:54 +0000 (19:07 +0100)
committerGitHub <noreply@github.com>
Wed, 25 Nov 2020 18:07:54 +0000 (12:07 -0600)
commit192c6c7667f74c91f4769b009cf8acc131292098
treead619f5170c87c889ae979bcfb651d8aaedaae5btree
parentde14432ebd850dab001bb860db102e86ec734f97commit | diff
Fix transcendental secant plane lemmas (#5525)

The refactoring of the transcendental solver introduced a subtle issue that lead to incorrect secant plane lemmas.
This PR fixes this issue, so that we now produce the correct lemmas again.
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/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
src/theory/arith/nl/transcendental/transcendental_state.cpp diff | blob | history
src/theory/arith/nl/transcendental/transcendental_state.h diff | blob | history