Refactor SymFPU dependency (#6218)

This PR refactors the contrib script to download SymFPU to a cmake external project.

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d18eefc35f785e3ed1759fd5c2fbb7ee0e77b025..5ebdc30b8397229ee848f4cc6dba7795043e0f5c 100644 (file)
--- 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 47a047ce0d852bdbe407459c0f196278cd34c5cf..da8beac994a77fe570d7ab8737f4fee1cbf2854b 100644 (file)
--- 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 <SOURCE_DIR>/core
+                    <INSTALL_DIR>/include/symfpu/core
+    COMMAND ${CMAKE_COMMAND} -E copy_directory <SOURCE_DIR>/utils
+            <INSTALL_DIR>/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 (executable)
index 383a620..0000000
--- 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 4e2113c51424503f1ee2b3f39228c6cebcb6cc9d..1a8c1964d9bab5f9e91a9747f5f67071f4fe3ac7 100644 (file)
--- 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 $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
+  target_link_libraries(cvc4 PRIVATE ${CLN_LIBRARIES})
+  target_include_directories(cvc4 PRIVATE $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
 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 $<BUILD_INTERFACE:${SymFPU_INCLUDE_DIR}>)
+  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 $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
+target_link_libraries(cvc4 PRIVATE ${GMP_LIBRARIES})
+target_include_directories(cvc4 PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
 
 # 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 6a960a214a3ca24241e101bf8f2792183f29a99e..2e9757fc7c72d73a686028801c9a533895e87b1f 100644 (file)
--- 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_OBJECTS:main>)
 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 $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
+endif()
+target_link_libraries(main-test ${GMP_LIBRARIES})
+target_include_directories(main-test PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
 
 #-----------------------------------------------------------------------------#
 # 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 $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
+endif()
+target_link_libraries(cvc4-bin ${GMP_LIBRARIES})
+target_include_directories(cvc4-bin PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
 if(PROGRAM_PREFIX)
   install(PROGRAMS
     $<TARGET_FILE:cvc4-bin>

diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index fdf268dc6587d5b9473b84540749fc7ccf045377..236517b0c934e6f858b216655d685d91da58a813 100644 (file)
--- 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 $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
+endif()
+target_link_libraries(cvc4parser PRIVATE ${GMP_LIBRARIES})
+target_include_directories(cvc4parser PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
+
 install(TARGETS cvc4parser
   EXPORT cvc4-targets
   DESTINATION ${CMAKE_INSTALL_LIBDIR})

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index bc185140f31cad345d824ab67b3300ce7a69bd8d..239c32c94fe0fd68035ad41bdc37384300f79609 100644 (file)
--- 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 $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
+  endif()
+  target_link_libraries(${name} ${GMP_LIBRARIES})
+  target_include_directories(${name} PRIVATE $<BUILD_INTERFACE:${GMP_INCLUDE_DIR}>)
   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 7163b5a12e7a2454acf3fccedeb12e62149c348a..c8c2b0d650b51608f1bc8a6ed43d41fd5dec87c0 100644 (file)
--- 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 $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
+  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()