From b7210ed60d517aebb25c23a2f407ee59562587dd Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 31 Mar 2021 21:16:05 +0200 Subject: [PATCH] Refactor SymFPU dependency (#6218) This PR refactors the contrib script to download SymFPU to a cmake external project. --- .github/workflows/ci.yml | 1 - cmake/FindSymFPU.cmake | 47 +++++++++++++++++++++++++++++++++++---- contrib/get-symfpu | 18 --------------- src/CMakeLists.txt | 25 ++++++++++----------- src/main/CMakeLists.txt | 12 ++++++++++ src/parser/CMakeLists.txt | 8 +++++++ test/api/CMakeLists.txt | 6 +++++ test/unit/CMakeLists.txt | 9 +++++++- 8 files changed, 89 insertions(+), 37 deletions(-) delete mode 100755 contrib/get-symfpu diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d18eefc35..5ebdc30b8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -119,7 +119,6 @@ jobs: if: steps.restore-deps.outputs.cache-hit != 'true' run: | ./contrib/get-poly - ./contrib/get-symfpu ./contrib/get-cadical ./contrib/get-cryptominisat ./contrib/get-lfsc-checker diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake index 47a047ce0..da8beac99 100644 --- a/cmake/FindSymFPU.cmake +++ b/cmake/FindSymFPU.cmake @@ -9,12 +9,51 @@ ## directory for licensing information. ## # Find SymFPU -# SymFPU_FOUND - system has SymFPU lib -# SymFPU_INCLUDE_DIR - the SymFPU include directory +# SymFPU_FOUND - should always be true +# SymFPU - interface target for the SymFPU headers find_path(SymFPU_INCLUDE_DIR NAMES symfpu/core/unpackedFloat.h) -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(SymFPU DEFAULT_MSG SymFPU_INCLUDE_DIR) +if(SymFPU_INCLUDE_DIR) + # Found SymFPU to be installed system-wide + set(SymFPU_FOUND_SYSTEM TRUE) +else() + set(SymFPU_FOUND_SYSTEM FALSE) + include(ExternalProject) + include(deps-helper) + set(SymFPU_COMMIT "8fbe139bf0071cbe0758d2f6690a546c69ff0053") + + ExternalProject_Add( + SymFPU-EP + PREFIX ${DEPS_PREFIX} + URL https://github.com/martin-cs/symfpu/archive/${SymFPU_COMMIT}.tar.gz + URL_HASH SHA1=9e00045130b93e3c2a46ce73a1b5b6451340dc46 + CONFIGURE_COMMAND "" + BUILD_COMMAND "" + INSTALL_COMMAND ${CMAKE_COMMAND} -E copy_directory /core + /include/symfpu/core + COMMAND ${CMAKE_COMMAND} -E copy_directory /utils + /include/symfpu/utils + ) + + set(SymFPU_INCLUDE_DIR "${DEPS_BASE}/include/") +endif() + +set(SymFPU_FOUND TRUE) + +add_library(SymFPU INTERFACE IMPORTED GLOBAL) +set_target_properties( + SymFPU PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${SymFPU_INCLUDE_DIR}" +) + +mark_as_advanced(SymFPU_FOUND) +mark_as_advanced(SymFPU_FOUND_SYSTEM) mark_as_advanced(SymFPU_INCLUDE_DIR) + +if(SymFPU_FOUND_SYSTEM) + message(STATUS "Found SymFPU: ${SymFPU_INCLUDE_DIR}") +else() + message(STATUS "Building SymFPU: ${SymFPU_INCLUDE_DIR}") + add_dependencies(SymFPU SymFPU-EP) +endif() diff --git a/contrib/get-symfpu b/contrib/get-symfpu deleted file mode 100755 index 383a620d9..000000000 --- a/contrib/get-symfpu +++ /dev/null @@ -1,18 +0,0 @@ -#!/usr/bin/env bash -# -source "$(dirname "$0")/get-script-header.sh" - -SYMFPU_DIR="$DEPS_DIR/symfpu-CVC4" -commit="8fbe139bf0071cbe0758d2f6690a546c69ff0053" - -setup_dep \ - "https://github.com/martin-cs/symfpu/archive/$commit.tar.gz" "$SYMFPU_DIR" -cd "$SYMFPU_DIR" -install_includes core symfpu -install_includes utils symfpu - -echo -echo "Using symfpu commit $commit" -echo -echo ===================== Now configure CVC4 with ===================== -echo ./configure.sh --symfpu diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4e2113c51..1a8c1964d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1127,47 +1127,46 @@ if(ENABLE_VALGRIND) target_include_directories(cvc4 PRIVATE ${Valgrind_INCLUDE_DIR}) endif() if(USE_ABC) - target_link_libraries(cvc4 ${ABC_LIBRARIES}) + target_link_libraries(cvc4 PRIVATE ${ABC_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${ABC_INCLUDE_DIR}) endif() if(USE_CADICAL) - target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES}) + target_link_libraries(cvc4 PRIVATE ${CaDiCaL_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${CaDiCaL_INCLUDE_DIR}) endif() if(USE_CLN) - target_link_libraries(cvc4 ${CLN_LIBRARIES}) - target_include_directories(cvc4 PUBLIC $) + target_link_libraries(cvc4 PRIVATE ${CLN_LIBRARIES}) + target_include_directories(cvc4 PRIVATE $) endif() if(USE_CRYPTOMINISAT) - target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES}) + target_link_libraries(cvc4 PRIVATE ${CryptoMiniSat_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${CryptoMiniSat_INCLUDE_DIR}) endif() if(USE_KISSAT) - target_link_libraries(cvc4 ${Kissat_LIBRARIES}) + target_link_libraries(cvc4 PRIVATE ${Kissat_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR}) endif() if(USE_GLPK) - target_link_libraries(cvc4 ${GLPK_LIBRARIES}) + target_link_libraries(cvc4 PRIVATE ${GLPK_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR}) endif() if(USE_POLY) - target_link_libraries(cvc4 ${POLY_LIBRARIES}) + target_link_libraries(cvc4 PRIVATE ${POLY_LIBRARIES}) target_include_directories(cvc4 PRIVATE ${POLY_INCLUDE_DIR}) endif() if(USE_SYMFPU) - target_include_directories(cvc4 - PUBLIC $) + target_link_libraries(cvc4 PRIVATE SymFPU) endif() # Note: When linked statically GMP needs to be linked after CLN since CLN # depends on GMP. -target_link_libraries(cvc4 ${GMP_LIBRARIES}) -target_include_directories(cvc4 PUBLIC $) +target_link_libraries(cvc4 PRIVATE ${GMP_LIBRARIES}) +target_include_directories(cvc4 PRIVATE $) # Add rt library # Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime). # RT_LIBRARIES should be empty for glibc >= 2.17 -target_link_libraries(cvc4 ${RT_LIBRARIES}) +target_link_libraries(cvc4 PRIVATE ${RT_LIBRARIES}) #-----------------------------------------------------------------------------# # Visit main subdirectory after creating target cvc4. For target main, we have diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 6a960a214..2e9757fc7 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -47,6 +47,12 @@ target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES}) add_library(main-test driver_unified.cpp $) target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER) target_link_libraries(main-test cvc4 cvc4parser) +if(USE_CLN) + target_link_libraries(main-test ${CLN_LIBRARIES}) + target_include_directories(main-test PRIVATE $) +endif() +target_link_libraries(main-test ${GMP_LIBRARIES}) +target_include_directories(main-test PRIVATE $) #-----------------------------------------------------------------------------# # cvc4 binary configuration @@ -58,6 +64,12 @@ set_target_properties(cvc4-bin OUTPUT_NAME cvc4 RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) target_link_libraries(cvc4-bin cvc4 cvc4parser) +if(USE_CLN) + target_link_libraries(cvc4-bin ${CLN_LIBRARIES}) + target_include_directories(cvc4-bin PRIVATE $) +endif() +target_link_libraries(cvc4-bin ${GMP_LIBRARIES}) +target_include_directories(cvc4-bin PRIVATE $) if(PROGRAM_PREFIX) install(PROGRAMS $ diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index fdf268dc6..236517b0c 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -103,6 +103,14 @@ set_target_properties(cvc4parser PROPERTIES SOVERSION ${CVC4_SOVERSION}) target_compile_definitions(cvc4parser PRIVATE -D__BUILDING_CVC4PARSERLIB) target_link_libraries(cvc4parser PUBLIC cvc4) target_link_libraries(cvc4parser PRIVATE ANTLR3) + +if(USE_CLN) + target_link_libraries(cvc4parser PRIVATE ${CLN_LIBRARIES}) + target_include_directories(cvc4parser PRIVATE $) +endif() +target_link_libraries(cvc4parser PRIVATE ${GMP_LIBRARIES}) +target_include_directories(cvc4parser PRIVATE $) + install(TARGETS cvc4parser EXPORT cvc4-targets DESTINATION ${CMAKE_INSTALL_LIBDIR}) diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index bc185140f..239c32c94 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -32,6 +32,12 @@ macro(cvc4_add_api_test name) add_executable(${name} ${name}.cpp) target_link_libraries(${name} main-test) target_compile_definitions(${name} PRIVATE ${CVC4_API_TEST_FLAGS}) + if(USE_CLN) + target_link_libraries(${name} ${CLN_LIBRARIES}) + target_include_directories(${name} PRIVATE $) + endif() + target_link_libraries(${name} ${GMP_LIBRARIES}) + target_include_directories(${name} PRIVATE $) 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 7163b5a12..c8c2b0d65 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -40,10 +40,17 @@ macro(cvc4_add_unit_test is_white name output_dir) target_link_libraries(${name} main-test) target_link_libraries(${name} GTest::Main) target_link_libraries(${name} GTest::GTest) + + if(USE_CLN) + target_link_libraries(${name} ${CLN_LIBRARIES}) + target_include_directories(${name} PRIVATE $) + endif() if(USE_POLY) - # We don't link against libpoly, because CVC4 is already linked against it. + target_link_libraries(${name} ${POLY_LIBRARIES}) target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR}) endif() + target_link_libraries(${name} ${GMP_LIBRARIES}) + target_include_directories(${name} PRIVATE ${GMP_INCLUDE_DIR}) if(${is_white}) target_compile_options(${name} PRIVATE -fno-access-control) endif() -- 2.30.2