diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-07-17 09:06:31 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-17 00:06:31 -0700 |
| commit | 0a7e733a5cee4733ca8ca9fff1f6eab6fc22a549 (patch) | |
| tree | 8df7919ddfa7e3d3b6207f61edddfac6ed204305 /src/base/configuration.cpp | |
| parent | 2ee5a2bcf5fd7aaf72d44553ebb85edd76fd06c8 (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.
Diffstat (limited to 'src/base/configuration.cpp')
| -rw-r--r-- | src/base/configuration.cpp | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index 5fcc5170b..c50311840 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -179,7 +179,7 @@ std::string Configuration::copyright() { } } - if (Configuration::isBuiltWithGmp()) + if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly()) { ss << "This version of CVC4 is linked against the following third party\n" << "libraries covered by the LGPLv3 license.\n" @@ -188,6 +188,12 @@ std::string Configuration::copyright() { ss << " GMP - Gnu Multi Precision Arithmetic Library\n" << " See http://gmplib.org for copyright information.\n\n"; } + if (Configuration::isBuiltWithPoly()) + { + ss << " LibPoly polynomial library\n" + << " See https://github.com/SRI-CSL/libpoly for copyright and\n" + << " licensing information.\n\n"; + } } if (Configuration::isBuiltWithCln() @@ -269,6 +275,11 @@ bool Configuration::isBuiltWithLfsc() { return IS_LFSC_BUILD; } +bool Configuration::isBuiltWithPoly() +{ + return IS_POLY_BUILD; +} + bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; } unsigned Configuration::getNumDebugTags() { |