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

author	Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
	Fri, 17 Jul 2020 07:06:31 +0000 (09:06 +0200)
committer	GitHub <noreply@github.com>
	Fri, 17 Jul 2020 07:06:31 +0000 (00:06 -0700)
commit	0a7e733a5cee4733ca8ca9fff1f6eab6fc22a549
tree	8df7919ddfa7e3d3b6207f61edddfac6ed204305	tree
parent	2ee5a2bcf5fd7aaf72d44553ebb85edd76fd06c8	commit \| diff

Integration of libpoly (#4679)

This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration.
Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities.

21 files changed:

.github/workflows/ci.yml		diff \| blob \| history
CMakeLists.txt		diff \| blob \| history
COPYING		diff \| blob \| history
INSTALL.md		diff \| blob \| history
cmake/FindPoly.cmake	[new file with mode: 0644]	blob
configure.sh		diff \| blob \| history
contrib/get-poly	[new file with mode: 0755]	blob
src/CMakeLists.txt		diff \| blob \| history
src/base/configuration.cpp		diff \| blob \| history
src/base/configuration.h		diff \| blob \| history
src/base/configuration_private.h		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/util/CMakeLists.txt		diff \| blob \| history
src/util/poly_util.cpp	[new file with mode: 0644]	blob
src/util/poly_util.h	[new file with mode: 0644]	blob
src/util/real_algebraic_number.h.in	[new file with mode: 0644]	blob
src/util/real_algebraic_number_poly_imp.cpp	[new file with mode: 0644]	blob
src/util/real_algebraic_number_poly_imp.h	[new file with mode: 0644]	blob
test/unit/CMakeLists.txt		diff \| blob \| history
test/unit/util/CMakeLists.txt		diff \| blob \| history
test/unit/util/real_algebraic_number_black.h	[new file with mode: 0644]	blob

RSS Atom