summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/workflows/ci.yml1
-rw-r--r--cmake/FindSymFPU.cmake47
-rwxr-xr-xcontrib/get-symfpu18
-rw-r--r--src/CMakeLists.txt25
-rw-r--r--src/main/CMakeLists.txt12
-rw-r--r--src/parser/CMakeLists.txt8
-rw-r--r--test/api/CMakeLists.txt6
-rw-r--r--test/unit/CMakeLists.txt9
8 files changed, 89 insertions, 37 deletions
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()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback