projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 75359f1) | patch
Refactor transcendental solver (#5539)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 1 Dec 2020 15:44:32 +0000 (16:44 +0100)
committerGitHub <noreply@github.com>
Tue, 1 Dec 2020 15:44:32 +0000 (09:44 -0600)
commit9cbf861d698aaa44d79ca7bd4714064a55f31fba
tree4e8b2ba9b88b7bf3dd7f5a5cb5dd6423d0b5ee51tree
parent75359f120b1cdfa77add48ef11c776f530783c31commit | diff
Refactor transcendental solver (#5539)

This PR does another round of refactoring on the transcendental solver. It cleans up some variable names, introduces an enum type for Convexity and passes both the intended taylor degree and the actual taylor degree (which will be needed for proofs).
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/taylor_generator.cpp diff | blob | history
src/theory/arith/nl/transcendental/taylor_generator.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