diff options
| -rw-r--r-- | .github/workflows/ci.yml | 5 | ||||
| -rw-r--r-- | cmake/FindGMP.cmake | 72 | ||||
| -rw-r--r-- | cmake/FindPoly.cmake | 138 | ||||
| -rw-r--r-- | cmake/deps-helper.cmake | 32 | ||||
| -rwxr-xr-x | contrib/get-gmp-dev | 61 | ||||
| -rwxr-xr-x | contrib/get-poly | 30 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 6 | ||||
| -rw-r--r-- | src/main/CMakeLists.txt | 11 | ||||
| -rw-r--r-- | src/parser/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/api/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/unit/CMakeLists.txt | 6 |
11 files changed, 218 insertions, 149 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 21d8784ae..3930adbfa 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -118,13 +118,8 @@ jobs: - name: Setup Dependencies if: steps.restore-deps.outputs.cache-hit != 'true' run: | - ./contrib/get-poly ./contrib/get-lfsc-checker - - name: List dependencies - run: | - find deps/install -type f - # GitHub actions currently does not support modifying an already existing # cache. Hence, we create a new cache for each commit with key # cache-${{ runner.os }}-${{ matrix.cache-key }}-${{ github.sha }}. This diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index 1e1ca26c7..7e81dfd19 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -9,17 +9,73 @@ ## directory for licensing information. ## # Find GMP -# GMP_FOUND - system has GMP lib -# GMP_INCLUDE_DIR - the GMP include directory -# GMP_LIBRARIES - Libraries needed to use GMP +# GMP_FOUND - should always be true +# GMP - target for the GMP library + +include(deps-helper) find_path(GMP_INCLUDE_DIR NAMES gmp.h gmpxx.h) find_library(GMP_LIBRARIES NAMES gmp) -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES) +set(GMP_FOUND_SYSTEM FALSE) +if(GMP_INCLUDE_DIR AND GMP_LIBRARIES) + set(GMP_FOUND_SYSTEM TRUE) + + function(getversionpart OUTPUT FILENAME DESC) + file(STRINGS ${FILENAME} RES REGEX "^#define __GNU_MP_${DESC}[ \\t]+.*") + string(REGEX MATCH "[0-9]+" RES "${RES}") + set(${OUTPUT} + "${RES}" + PARENT_SCOPE + ) + endfunction() + getversionpart(MAJOR "${GMP_INCLUDE_DIR}/gmp.h" "VERSION") + getversionpart(MINOR "${GMP_INCLUDE_DIR}/gmp.h" "VERSION_MINOR") + getversionpart(PATCH "${GMP_INCLUDE_DIR}/gmp.h" "VERSION_PATCHLEVEL") + set(GMP_VERSION + "${MAJOR}.${MINOR}.${PATCH}" + PARENT_SCOPE + ) + + check_system_version("GMP") +endif() + +if(NOT GMP_FOUND_SYSTEM) + include(ExternalProject) + + set(GMP_VERSION "6.2.1") + + ExternalProject_Add( + GMP-EP + PREFIX ${DEPS_PREFIX} + URL https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2 + URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822 + CONFIGURE_COMMAND + <SOURCE_DIR>/configure --prefix=<INSTALL_DIR> --enable-cxx --with-pic + --disable-shared --enable-static --host=${TOOLCHAIN_PREFIX} + BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libgmp.a + ) + + set(GMP_INCLUDE_DIR "${DEPS_BASE}/include/") + set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp.a") +endif() + +set(GMP_FOUND TRUE) + +add_library(GMP STATIC IMPORTED GLOBAL) +set_target_properties(GMP PROPERTIES IMPORTED_LOCATION "${GMP_LIBRARIES}") +set_target_properties( + GMP PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${GMP_INCLUDE_DIR}" +) + +mark_as_advanced(GMP_FOUND) +mark_as_advanced(GMP_FOUND_SYSTEM) +mark_as_advanced(GMP_INCLUDE_DIR) +mark_as_advanced(GMP_LIBRARIES) -mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES) -if(GMP_LIBRARIES) - message(STATUS "Found GMP libs: ${GMP_LIBRARIES}") +if(GMP_FOUND_SYSTEM) + message(STATUS "Found GMP ${GMP_VERSION}: ${GMP_LIBRARIES}") +else() + message(STATUS "Building GMP ${GMP_VERSION}: ${GMP_LIBRARIES}") + add_dependencies(GMP GMP-EP) endif() diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake index ddcf9ddf5..3556a9d63 100644 --- a/cmake/FindPoly.cmake +++ b/cmake/FindPoly.cmake @@ -9,26 +9,120 @@ ## directory for licensing information. ## # 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}") +# Poly_FOUND - should always be true +# Poly - target for the libpoly library +# Polyxx - target for the C++ interface of libpoly, also links Poly + +include(deps-helper) + +find_path(Poly_INCLUDE_DIR NAMES poly/poly.h) +find_library(Poly_LIBRARIES NAMES poly) +find_library(PolyXX_LIBRARIES NAMES polyxx) + +set(Dummy_FOUND_SYSTEM FALSE) +if(Poly_INCLUDE_DIR + AND Poly_LIBRARIES + AND PolyXX_LIBRARIES +) + set(Poly_FOUND_SYSTEM TRUE) + + file(STRINGS ${Poly_INCLUDE_DIR}/poly/version.h Poly_VERSION + REGEX "^#define[\t ]+LIBPOLY_VERSION [0-9+]+" + ) + string(REGEX MATCH "[0-9.]+" Poly_VERSION "${Poly_VERSION}") + + check_system_version("Poly") +endif() + +if(NOT Poly_FOUND_SYSTEM) + include(ExternalProject) + + # TODO(#4706): Use proper release, after the next release + set(Poly_VERSION "bae67639726f63ed508a30845108bfdac4a77546") + + check_if_cross_compiling(CCWIN "Windows" "") + if(CCWIN) + # Roughly following https://stackoverflow.com/a/44383330/2375725 + set(patchcmd + PATCH_COMMAND + patch + <SOURCE_DIR>/src/CMakeLists.txt + ${CMAKE_CURRENT_LIST_DIR}/deps-utils/Poly-patch-cmake.patch + # Avoid %z and %llu format specifiers + COMMAND find <SOURCE_DIR>/ -type f -exec + sed -i.orig "s/%z[diu]/%\" PRIu64 \"/g" {} + + COMMAND find <SOURCE_DIR>/ -type f -exec + sed -i.orig "s/%ll[du]/%\" PRIu64 \"/g" {} + + # Make sure the new macros are available + COMMAND find <SOURCE_DIR>/ -type f -exec + sed -i.orig "s/#include <stdio.h>/#include <stdio.h>\\n#include <inttypes.h>/" {} + + COMMAND find <SOURCE_DIR>/ -type f -exec + sed -i.orig "s/#include <cstdio>/#include <cstdio>\\n#include <inttypes.h>/" {} + + ) + else() + unset(patchcmd) + endif() + + ExternalProject_Add( + Poly-EP + PREFIX ${DEPS_PREFIX} + URL https://github.com/SRI-CSL/libpoly/archive/${Poly_VERSION}.tar.gz + URL_HASH SHA1=2e79d5220d3ecbb40811463fcf12c5ddbd4b9f30 + DOWNLOAD_NAME libpoly.tar.gz + ${patchcmd} + CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release + -DCMAKE_INSTALL_PREFIX=<INSTALL_DIR> + -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} + -DLIBPOLY_BUILD_PYTHON_API=OFF + -DLIBPOLY_BUILD_STATIC=ON + -DLIBPOLY_BUILD_STATIC_PIC=ON + BUILD_COMMAND ${CMAKE_MAKE_PROGRAM} static_pic_poly static_pic_polyxx + INSTALL_COMMAND ${CMAKE_MAKE_PROGRAM} install + COMMAND ${CMAKE_COMMAND} -E copy src/libpicpoly.a + <INSTALL_DIR>/lib/libpicpoly.a + COMMAND ${CMAKE_COMMAND} -E copy src/libpicpolyxx.a + <INSTALL_DIR>/lib/libpicpolyxx.a + BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libpicpoly.a + <INSTALL_DIR>/lib/libpicpolyxx.a + ) + ExternalProject_Add_Step( + Poly-EP cleanup + DEPENDEES install + COMMAND ${CMAKE_COMMAND} -E remove_directory <SOURCE_DIR>/test/ + COMMAND ${CMAKE_COMMAND} -E remove_directory <BINARY_DIR>/test/ + ) + add_dependencies(Poly-EP GMP) + + set(Poly_INCLUDE_DIR "${DEPS_BASE}/include/") + set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpicpoly.a") + set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpicpolyxx.a") +endif() + +set(Poly_FOUND TRUE) + +add_library(Poly STATIC IMPORTED GLOBAL) +set_target_properties(Poly PROPERTIES IMPORTED_LOCATION "${Poly_LIBRARIES}") +set_target_properties( + Poly PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}" +) + +add_library(Polyxx STATIC IMPORTED GLOBAL) +set_target_properties(Polyxx PROPERTIES IMPORTED_LOCATION "${PolyXX_LIBRARIES}") +set_target_properties( + Polyxx PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}" +) +set_target_properties(Polyxx PROPERTIES INTERFACE_LINK_LIBRARIES Poly) + +mark_as_advanced(Poly_FOUND) +mark_as_advanced(Poly_FOUND_SYSTEM) +mark_as_advanced(Poly_INCLUDE_DIR) +mark_as_advanced(Poly_LIBRARIES) +mark_as_advanced(PolyXX_LIBRARIES) + +if(Poly_FOUND_SYSTEM) + message(STATUS "Found Poly ${Poly_VERSION}: ${Poly_LIBRARIES}") +else() + message(STATUS "Building Poly ${Poly_VERSION}: ${Poly_LIBRARIES}") + add_dependencies(Poly Poly-EP) + add_dependencies(Polyxx Poly-EP) endif() diff --git a/cmake/deps-helper.cmake b/cmake/deps-helper.cmake index bdc3e5de1..4b88d62ce 100644 --- a/cmake/deps-helper.cmake +++ b/cmake/deps-helper.cmake @@ -23,28 +23,46 @@ endmacro(check_system_version) # we are cross compiling if # - CMAKE_SYSTEM_NAME has been changed to ${name} # - CMAKE_SYSTEM_PROCESSOR has been changed to ${processor} -function(fail_if_cross_compiling name processor target error) - set(FAIL FALSE) +function(check_if_cross_compiling OUT name processor) if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "${CMAKE_HOST_SYSTEM_NAME}") if(NOT "${name}" STREQUAL "") if("${CMAKE_SYSTEM_NAME}" STREQUAL "${name}") - set(FAIL TRUE) + set(${OUT} TRUE PARENT_SCOPE) + return() endif() endif() endif() if(NOT "${CMAKE_SYSTEM_PROCESSOR}" STREQUAL "${CMAKE_HOST_SYSTEM_PROCESSOR}") if(NOT "${processor}" STREQUAL "") if("${CMAKE_SYSTEM_PROCESSOR}" STREQUAL "${processor}") - set(FAIL TRUE) + set(${OUT} TRUE PARENT_SCOPE) + return() endif() endif() endif() + set(${OUT} FALSE PARENT_SCOPE) +endfunction(check_if_cross_compiling) + +# fail if we are cross compiling as indicated by name and processor +# we are cross compiling if +# - CMAKE_SYSTEM_NAME has been changed to ${name} +# - CMAKE_SYSTEM_PROCESSOR has been changed to ${processor} +function(fail_if_cross_compiling name processor target error) + check_if_cross_compiling(FAIL "${name}" "${processor}") if(FAIL) message(SEND_ERROR - "We are cross compiling from \ + "We are cross compiling from \ ${CMAKE_HOST_SYSTEM_NAME}-${CMAKE_HOST_SYSTEM_PROCESSOR} to \ ${CMAKE_SYSTEM_NAME}-${CMAKE_SYSTEM_PROCESSOR}.\n" - "This is not supported by ${target}:\n" - "${error}") + "This is not supported by ${target}:\n" + "${error}") endif() endfunction(fail_if_cross_compiling) + +function(fail_if_include_missing include target) + include(CheckIncludeFileCXX) + check_include_file_cxx(${include} HAVE_INCLUDE) + if(NOT HAVE_INCLUDE) + message(SEND_ERROR "${target} requires ${include} header, but it is not available.") + endif() +endfunction(fail_if_include_missing) diff --git a/contrib/get-gmp-dev b/contrib/get-gmp-dev deleted file mode 100755 index 4baebc265..000000000 --- a/contrib/get-gmp-dev +++ /dev/null @@ -1,61 +0,0 @@ -#!/usr/bin/env bash -# -# This script should only be used if your distribution does not ship with the -# GMP configuration you need. For example, for cross-compiling GMP for Windows -# or Linux ARM platforms. You can also use the script if your -# distribution does not ship with static GMP libraries (e.g., Arch Linux) and -# you want to build CVC4 statically. -# In most of the cases the GMP version installed on your system is the one you -# want and should use. -# - -source "$(dirname "$0")/get-script-header.sh" - -CONFIG= -while :; do - case $1 in - --host=?*) - host=${1#*=} - CONFIG="--host=$host" - ;; - --host=) - echo "Error: empty --host=" - exit 1 - ;; - *) - break - esac - shift -done - -[ -z "${BUILD_TYPE}" ] && BUILD_TYPE="--disable-shared --enable-static" -[ -z "$GMPVERSION" ] && GMPVERSION=6.2.1 - -GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION" -rm -rf "$GMP_DIR" - -echo ============================================================================= -echo -echo "This script should only be used if your distribution does not ship with the" -echo "GMP configuration you need. For example, for cross-compiling GMP for" -echo "Windows or Linux ARM platforms. You can also use the script if your Linux" -echo "distribution does not ship with static GMP libraries (e.g., Arch Linux)" -echo "and you want to build CVC4 statically." -echo -echo "In most of the cases the GMP version installed on your system is the one you" -echo "want and should use." -echo -echo ============================================================================= -echo -echo "Setting up GMP $GMPVERSION..." -echo -setup_dep "https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2" "$GMP_DIR" -cd "$GMP_DIR" -./configure ${CONFIG} --prefix="$INSTALL_DIR" --enable-cxx ${BUILD_TYPE} -make \ - CFLAGS="${MAKE_CFLAGS}" \ - CXXFLAGS="${MAKE_CXXFLAGS}" \ - LDFLAGS="${MAKE_LDFLAGS}" \ - -j$(nproc) -make install -echo diff --git a/contrib/get-poly b/contrib/get-poly deleted file mode 100755 index d2e0935b6..000000000 --- a/contrib/get-poly +++ /dev/null @@ -1,30 +0,0 @@ -#!/usr/bin/env bash -# -source "$(dirname "$0")/get-script-header.sh" - -POLY_DIR="$DEPS_DIR/poly" -version="v0.1.8" - -setup_dep \ - "https://github.com/SRI-CSL/libpoly/archive/master.tar.gz" "$POLY_DIR" -# TODO(Gereon, #4706): Go back to fixed version with the next release - -pwd -cd "$POLY_DIR/build/" - -CMAKEFLAGS="\ - -DCMAKE_BUILD_TYPE=Release \ - -DLIBPOLY_BUILD_PYTHON_API=OFF \ - -DLIBPOLY_BUILD_STATIC=ON \ - -DLIBPOLY_BUILD_STATIC_PIC=ON \ -" - -echo "Installing to $INSTALL_DIR" - -cmake -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" $CMAKEFLAGS ../ && make -j${NPROC} install - -echo -echo "Using poly version $version" -echo -echo ===================== Now configure CVC4 with ===================== -echo ./configure.sh --poly diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 78236f989..2679f6072 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1148,8 +1148,7 @@ if(USE_GLPK) target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR}) endif() if(USE_POLY) - target_link_libraries(cvc4 PRIVATE ${POLY_LIBRARIES}) - target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR}) + target_link_libraries(cvc4 PRIVATE Polyxx) endif() if(USE_SYMFPU) target_link_libraries(cvc4 PRIVATE SymFPU) @@ -1157,8 +1156,7 @@ endif() # Note: When linked statically GMP needs to be linked after CLN since CLN # depends on GMP. -target_link_libraries(cvc4 PRIVATE ${GMP_LIBRARIES}) -target_include_directories(cvc4 PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>) +target_link_libraries(cvc4 PRIVATE GMP) # Add rt library # Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime). diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 2e9757fc7..2d2b08378 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -40,6 +40,11 @@ endif() add_dependencies(main cvc4 cvc4parser gen-tokens) get_target_property(LIBCVC4_INCLUDES cvc4 INCLUDE_DIRECTORIES) target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES}) +if(USE_CLN) + target_link_libraries(main ${CLN_LIBRARIES}) + target_include_directories(main PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>) +endif() +target_link_libraries(main GMP) # main-test library is only used for linking against api and unit tests so # that we don't have to include all object files of main into each api/unit @@ -51,8 +56,7 @@ if(USE_CLN) target_link_libraries(main-test ${CLN_LIBRARIES}) target_include_directories(main-test PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>) endif() -target_link_libraries(main-test ${GMP_LIBRARIES}) -target_include_directories(main-test PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>) +target_link_libraries(main-test GMP) #-----------------------------------------------------------------------------# # cvc4 binary configuration @@ -68,8 +72,7 @@ if(USE_CLN) target_link_libraries(cvc4-bin ${CLN_LIBRARIES}) target_include_directories(cvc4-bin PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>) endif() -target_link_libraries(cvc4-bin ${GMP_LIBRARIES}) -target_include_directories(cvc4-bin PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>) +target_link_libraries(cvc4-bin GMP) if(PROGRAM_PREFIX) install(PROGRAMS $<TARGET_FILE:cvc4-bin> diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 236517b0c..d131fa7b3 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -108,8 +108,7 @@ if(USE_CLN) target_link_libraries(cvc4parser PRIVATE ${CLN_LIBRARIES}) target_include_directories(cvc4parser PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>) endif() -target_link_libraries(cvc4parser PRIVATE ${GMP_LIBRARIES}) -target_include_directories(cvc4parser PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>) +target_link_libraries(cvc4parser PRIVATE GMP) install(TARGETS cvc4parser EXPORT cvc4-targets diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 239c32c94..1deea4a87 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -36,8 +36,7 @@ macro(cvc4_add_api_test name) target_link_libraries(${name} ${CLN_LIBRARIES}) target_include_directories(${name} PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>) endif() - target_link_libraries(${name} ${GMP_LIBRARIES}) - target_include_directories(${name} PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>) + target_link_libraries(${name} GMP) set_target_properties(${name} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) add_test(api/${name} ${test_bin_dir}/${name}) diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index c8c2b0d65..7b82f3346 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -46,11 +46,9 @@ macro(cvc4_add_unit_test is_white name output_dir) target_include_directories(${name} PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>) endif() if(USE_POLY) - target_link_libraries(${name} ${POLY_LIBRARIES}) - target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR}) + target_link_libraries(${name} Polyxx) endif() - target_link_libraries(${name} ${GMP_LIBRARIES}) - target_include_directories(${name} PRIVATE ${GMP_INCLUDE_DIR}) + target_link_libraries(${name} GMP) if(${is_white}) target_compile_options(${name} PRIVATE -fno-access-control) endif() |