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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 11 Apr 2020 00:15:18 +0000 (19:15 -0500)
committer	GitHub <noreply@github.com>
	Sat, 11 Apr 2020 00:15:18 +0000 (19:15 -0500)
commit	04a8bf833bad57329a4e83b3c5aafb7537de885d
tree	07d3e46c8da90c8b23475712deb93b39765dc047	tree
parent	6b599f87b18186b811f187789e48c1e8c0774534	commit \| diff

Split the non-linear solver (#4219)

This splits the "non-linear solver" from "NonlinearExtension". The non-linear solver is the module that implements the inference schemas whereas NonlinearExtension is the glue code that manages the solver(s) for non-linear.

This also involves moving utilities from the non-linear solver to their own file.

src/CMakeLists.txt		diff \| blob \| history
src/theory/arith/nl_constraint.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl_constraint.h	[new file with mode: 0644]	blob
src/theory/arith/nl_lemma_utils.h		diff \| blob \| history
src/theory/arith/nl_monomial.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl_monomial.h	[new file with mode: 0644]	blob
src/theory/arith/nl_solver.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl_solver.h	[new file with mode: 0644]	blob
src/theory/arith/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/transcendental_solver.h		diff \| blob \| history

RSS Atom