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 /cmake | |
| 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 'cmake')
| -rw-r--r-- | cmake/FindPoly.cmake | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake new file mode 100644 index 000000000..5f4383732 --- /dev/null +++ b/cmake/FindPoly.cmake @@ -0,0 +1,24 @@ +# Find LibPoly +# POLY_FOUND - system has LibPoly +# POLY_INCLUDE_DIR - the LibPoly include directory +# POLY_LIBRARIES - Libraries needed to use LibPoly + +# Note: contrib/get-poly copies header files to deps/install/include/poly. +# However, includes in LibPoly headers are not prefixed with "poly/" and therefore +# we have to look for headers in include/poly instead of include/. +find_path(POLY_INCLUDE_DIR NAMES poly/poly.h PATH_SUFFIXES poly) +find_library(POLY_LIB NAMES poly) +find_library(POLY_LIBXX NAMES polyxx) +set(POLY_LIBRARIES "${POLY_LIBXX};${POLY_LIB}") +unset(POLY_LIB CACHE) +unset(POLY_LIBXX CACHE) + +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(Poly + DEFAULT_MSG + POLY_INCLUDE_DIR POLY_LIBRARIES) + +mark_as_advanced(POLY_INCLUDE_DIR POLY_LIBRARIES) +if(POLY_LIBRARIES) + message(STATUS "Found LibPoly: ${POLY_LIBRARIES}") +endif() |