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 | |
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')
-rw-r--r-- | src/base/configuration.cpp | 13 | ||||
-rw-r--r-- | src/base/configuration.h | 2 | ||||
-rw-r--r-- | src/base/configuration_private.h | 6 |
3 files changed, 20 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() { diff --git a/src/base/configuration.h b/src/base/configuration.h index de060fa00..40914e531 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -107,6 +107,8 @@ public: static bool isBuiltWithLfsc(); + static bool isBuiltWithPoly(); + static bool isBuiltWithSymFPU(); /* Return the number of debug tags */ diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index 9c58e7898..906cf831d 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -138,6 +138,12 @@ namespace CVC4 { #define IS_LFSC_BUILD false #endif /* CVC4_USE_LFSC */ +#if CVC4_USE_POLY +#define IS_POLY_BUILD true +#else /* CVC4_USE_POLY */ +#define IS_POLY_BUILD false +#endif /* CVC4_USE_POLY */ + #if HAVE_LIBREADLINE # define IS_READLINE_BUILD true #else /* HAVE_LIBREADLINE */ |