git.libre-soc.org Git - cvc5.git/commit

author	Gereon Kremer <nafur42@gmail.com>
	Mon, 7 Dec 2020 19:59:10 +0000 (20:59 +0100)
committer	GitHub <noreply@github.com>
	Mon, 7 Dec 2020 19:59:10 +0000 (20:59 +0100)
commit	5cc5bc2eafa90c763e727868c6149b5c370e63f7
tree	044cd426f035d5449920b5e3140562a3346dc443	tree
parent	a062043b187afe410f0de3568f57594e74eb8d25	commit \| diff

Refactor initial phase of transcendental solver (#5599)

This PR refactors the initialization of the transcendental solver, decoupling the setup of generic caches from initial lemmas for exponential and sine functions.

RSS Atom

src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
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_solver.h		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