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

author	Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
	Thu, 30 Jul 2020 16:16:25 +0000 (18:16 +0200)
committer	GitHub <noreply@github.com>
	Thu, 30 Jul 2020 16:16:25 +0000 (09:16 -0700)
commit	9f57f4613dd273b0ef1a531cc72fc418cf4b1af0
tree	3f7ab1a2b1f2a59927de109c51b4d146d2610a45	tree
parent	e142a47195faba468d523660710bedc05f6591dd	commit \| diff

Adds the interface for the CAD-based arithmetic solver. (#4773)

This PR adds some utilities and, most importantly, the interface of the new
CAD-based solver.
The approach is based on https://arxiv.org/pdf/2003.05633.pdf and the code
structure follows the paper rather closely.

13 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/theory/arith/nl/cad/cdcac.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl/cad/cdcac.h	[new file with mode: 0644]	blob
src/theory/arith/nl/cad/cdcac_utils.cpp	[new file with mode: 0644]	blob
src/theory/arith/nl/cad/cdcac_utils.h	[new file with mode: 0644]	blob
src/theory/arith/nl/cad/constraints.cpp		diff \| blob \| history
src/theory/arith/nl/cad/constraints.h		diff \| blob \| history
src/theory/arith/nl/cad/projections.cpp		diff \| blob \| history
src/theory/arith/nl/cad/projections.h		diff \| blob \| history
src/theory/arith/nl/cad/variable_ordering.cpp		diff \| blob \| history
src/theory/arith/nl/cad/variable_ordering.h		diff \| blob \| history
src/theory/arith/nl/poly_conversion.cpp		diff \| blob \| history
src/theory/arith/nl/poly_conversion.h		diff \| blob \| history

RSS Atom