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 /COPYING | |
| 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 'COPYING')
| -rw-r--r-- | COPYING | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -79,6 +79,7 @@ CVC4 optionally links against the following libraries: CaDiCaL (https://github.com/arminbiere/cadical) CryptoMiniSat (https://github.com/msoos/cryptominisat) LFSC checker (https://github.com/CVC4/LFSC) + LibPoly (https://github.com/SRI-CSL/libpoly) Linking CVC4 against these libraries does not affect the license terms of the CVC4 code. See the respective projects for copyright and licensing @@ -111,4 +112,3 @@ CVC4 can be optionally configured to link against GNU Readline for improved text-editing support in interactive mode. GNU Readline is available here: http://cnswww.cns.cwru.edu/php/chet/readline/rltop.html - |