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

author	Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
	Wed, 25 Nov 2020 00:07:42 +0000 (01:07 +0100)
committer	GitHub <noreply@github.com>
	Wed, 25 Nov 2020 00:07:42 +0000 (18:07 -0600)
commit	2576297452114b9bc916c84a748a5337e595a323
tree	8261a6df31098c4b1963b45f542bdcb85d71def1	tree
parent	07c7b873c5c2ee81cb2672428ca1de0d75bb1ae8	commit \| diff

Refactor transcendental solver (#5514)

The transcendental solver has grown over time, and a refactoring was due.
This PR splits the transcendental solver into five components:

a utility to compute taylor approximations
a common state for transcendental solvers
a solver for exponential function
a solver for sine function
a solver that wraps everything to a transcendental solver.

15 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/theory/arith/nl/nl_lemma_utils.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/exponential_solver.h	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/sine_solver.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/sine_solver.h	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/taylor_generator.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/taylor_generator.h	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/transcendental_solver.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/transcendental_solver.h	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/transcendental_state.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental/transcendental_state.h	[new file with mode: 0644]	blob
src/theory/arith/nl/transcendental_solver.cpp	[deleted file]	blob \| history
src/theory/arith/nl/transcendental_solver.h	[deleted file]	blob \| history

RSS Atom