From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 31 Mar 2021 19:16:05 +0000 (+0200)
Subject: Refactor SymFPU dependency (#6218)
X-Git-Tag: cvc5-1.0.0~2000
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b7210ed60d517aebb25c23a2f407ee59562587dd;p=cvc5.git

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 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 <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
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 $<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 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_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 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 $<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 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 $<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 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 $<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()