diff options
| -rw-r--r-- | CMakeLists.txt | 36 | ||||
| -rw-r--r-- | cmake/FindCLN.cmake | 34 | ||||
| -rw-r--r-- | cmake/FindPoly.cmake | 72 | ||||
| -rw-r--r-- | src/CMakeLists.txt | 14 | ||||
| -rw-r--r-- | src/main/CMakeLists.txt | 7 |
5 files changed, 115 insertions, 48 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 8e5a9c7e7..07ff3c76f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -267,25 +267,23 @@ endif() # This needs to be set before any find_package(...) command since we want to # search for static libraries with suffix .a. -if(NOT ENABLE_STATIC_BINARY) - # Embed the installation prefix as an RPATH in the executable such that the - # linker can find our libraries (such as libcvc5parser) when executing the - # cvc5 binary. This is for example useful when installing cvc5 with a custom - # prefix on macOS (e.g. when using homebrew in a non-standard directory). If - # we do not set this option, then the linker will not be able to find the - # required libraries when trying to run cvc5. - # - # Also embed the installation prefix of the installed contrib libraries as an - # RPATH. This allows to install a dynamically linked binary that depends on - # dynamically linked libraries. This is dangerous, as the installed binary - # breaks if the contrib library is removed or changes in other ways, we thus - # print a big warning and only allow if installing to a custom installation - # prefix. - # - # More information on RPATH in CMake: - # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling - set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib") -endif() +# Embed the installation prefix as an RPATH in the executable such that the +# linker can find our libraries (such as libcvc5parser) when executing the +# cvc5 binary. This is for example useful when installing cvc5 with a custom +# prefix on macOS (e.g. when using homebrew in a non-standard directory). If +# we do not set this option, then the linker will not be able to find the +# required libraries when trying to run cvc5. +# +# Also embed the installation prefix of the installed contrib libraries as an +# RPATH. This allows to install a dynamically linked binary that depends on +# dynamically linked libraries. This is dangerous, as the installed binary +# breaks if the contrib library is removed or changes in other ways, we thus +# print a big warning and only allow if installing to a custom installation +# prefix. +# +# More information on RPATH in CMake: +# https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling +set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib") # Set visibility to default if unit tests are enabled if(ENABLE_UNIT_TESTING) diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake index f2a6d853e..11bf8ed98 100644 --- a/cmake/FindCLN.cmake +++ b/cmake/FindCLN.cmake @@ -33,6 +33,15 @@ if(CLN_INCLUDE_DIR AND CLN_LIBRARIES) check_system_version("CLN") endif() +if(ENABLE_STATIC_LIBRARY AND CLN_FOUND_SYSTEM) + force_static_library() + find_library(CLN_STATIC_LIBRARIES NAMES cln) + if(NOT CLN_STATIC_LIBRARIES) + set(CLN_FOUND_SYSTEM FALSE) + endif() + reset_force_static_library() +endif() + if(NOT CLN_FOUND_SYSTEM) check_ep_downloaded("CLN-EP") if(NOT CLN-EP_DOWNLOADED) @@ -62,28 +71,36 @@ if(NOT CLN_FOUND_SYSTEM) ${CMAKE_COMMAND} -E chdir <SOURCE_DIR> ./autogen.sh COMMAND ${CMAKE_COMMAND} -E chdir <SOURCE_DIR> autoreconf -iv - COMMAND <SOURCE_DIR>/configure --prefix=<INSTALL_DIR> --disable-shared + COMMAND <SOURCE_DIR>/configure --prefix=<INSTALL_DIR> --enable-shared --enable-static --with-pic BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libcln.a + <INSTALL_DIR>/lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX} ) add_dependencies(CLN-EP GMP_SHARED) set(CLN_INCLUDE_DIR "${DEPS_BASE}/include/") - set(CLN_LIBRARIES "${DEPS_BASE}/lib/libcln.a") + set(CLN_LIBRARIES "${DEPS_BASE}/lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}") + set(CLN_STATIC_LIBRARIES "${DEPS_BASE}/lib/libcln.a") endif() set(CLN_FOUND TRUE) -add_library(CLN STATIC IMPORTED GLOBAL) -set_target_properties(CLN PROPERTIES +add_library(CLN_SHARED SHARED IMPORTED GLOBAL) +set_target_properties(CLN_SHARED PROPERTIES IMPORTED_LOCATION "${CLN_LIBRARIES}" INTERFACE_INCLUDE_DIRECTORIES "${CLN_INCLUDE_DIR}" ) +target_link_libraries(CLN_SHARED INTERFACE GMP_SHARED) + + if(ENABLE_STATIC_LIBRARY) - target_link_libraries(CLN INTERFACE GMP_STATIC) -else() - target_link_libraries(CLN INTERFACE GMP_SHARED) + add_library(CLN_STATIC STATIC IMPORTED GLOBAL) + set_target_properties(CLN_STATIC PROPERTIES + IMPORTED_LOCATION "${CLN_STATIC_LIBRARIES}" + INTERFACE_INCLUDE_DIRECTORIES "${CLN_INCLUDE_DIR}" + ) + target_link_libraries(CLN_STATIC INTERFACE GMP_STATIC) endif() mark_as_advanced(AUTORECONF) @@ -96,5 +113,6 @@ if(CLN_FOUND_SYSTEM) message(STATUS "Found CLN ${CLN_VERSION}: ${CLN_LIBRARIES}") else() message(STATUS "Building CLN ${CLN_VERSION}: ${CLN_LIBRARIES}") - add_dependencies(CLN CLN-EP) + add_dependencies(CLN_SHARED CLN-EP) + add_dependencies(CLN_STATIC CLN-EP) endif() diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake index 6ddb918a9..ae236c6d9 100644 --- a/cmake/FindPoly.cmake +++ b/cmake/FindPoly.cmake @@ -37,6 +37,16 @@ if(Poly_INCLUDE_DIR check_system_version("Poly") endif() +if(ENABLE_STATIC_LIBRARY AND Poly_FOUND_SYSTEM) + force_static_library() + find_library(Poly_STATIC_LIBRARIES NAMES poly) + find_library(PolyXX_STATIC_LIBRARIES NAMES polyxx) + if(NOT Poly_STATIC_LIBRARIES OR NOT PolyXX_STATIC_LIBRARIES) + set(Poly_FOUND_SYSTEM FALSE) + endif() + reset_force_static_library() +endif() + if(NOT Poly_FOUND_SYSTEM) check_ep_downloaded("Poly-EP") if(NOT Poly-EP_DOWNLOADED) @@ -95,6 +105,8 @@ if(NOT Poly_FOUND_SYSTEM) <INSTALL_DIR>/lib/libpicpolyxx.a BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libpicpoly.a <INSTALL_DIR>/lib/libpicpolyxx.a + <INSTALL_DIR>/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX} + <INSTALL_DIR>/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX} ) ExternalProject_Add_Step( Poly-EP cleanup @@ -104,29 +116,43 @@ if(NOT Poly_FOUND_SYSTEM) add_dependencies(Poly-EP GMP_SHARED) set(Poly_INCLUDE_DIR "${DEPS_BASE}/include/") - set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpicpoly.a") - set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpicpolyxx.a") + set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}") + set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}") + set(Poly_STATIC_LIBRARIES "${DEPS_BASE}/lib/libpicpoly.a") + set(PolyXX_STATIC_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(Poly_SHARED SHARED IMPORTED GLOBAL) +set_target_properties(Poly_SHARED PROPERTIES + IMPORTED_LOCATION "${Poly_LIBRARIES}" + INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}" ) -if(ENABLE_STATIC_LIBRARY) - target_link_libraries(Poly INTERFACE GMP_STATIC) -else() - target_link_libraries(Poly INTERFACE GMP_SHARED) -endif() +target_link_libraries(Poly_SHARED INTERFACE GMP_SHARED) -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}" +add_library(Polyxx_SHARED SHARED IMPORTED GLOBAL) +set_target_properties(Polyxx_SHARED PROPERTIES + IMPORTED_LOCATION "${PolyXX_LIBRARIES}" + INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}" + INTERFACE_LINK_LIBRARIES Poly_SHARED ) -set_target_properties(Polyxx PROPERTIES INTERFACE_LINK_LIBRARIES Poly) + +if(ENABLE_STATIC_LIBRARY) + add_library(Poly_STATIC STATIC IMPORTED GLOBAL) + set_target_properties(Poly_STATIC PROPERTIES + IMPORTED_LOCATION "${Poly_STATIC_LIBRARIES}" + INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}" + ) + target_link_libraries(Poly_STATIC INTERFACE GMP_STATIC) + + add_library(Polyxx_STATIC STATIC IMPORTED GLOBAL) + set_target_properties(Polyxx_STATIC PROPERTIES + IMPORTED_LOCATION "${PolyXX_STATIC_LIBRARIES}" + INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}" + INTERFACE_LINK_LIBRARIES Poly_STATIC + ) +endif() mark_as_advanced(Poly_FOUND) mark_as_advanced(Poly_FOUND_SYSTEM) @@ -138,6 +164,16 @@ 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) + add_dependencies(Poly_SHARED Poly-EP) + add_dependencies(Polyxx_SHARED Poly-EP) + + install(FILES + $<TARGET_SONAME_FILE:Poly_SHARED> $<TARGET_SONAME_FILE:Polyxx_SHARED> + DESTINATION ${CMAKE_INSTALL_LIBDIR} + ) + + if(ENABLE_STATIC_LIBRARY) + add_dependencies(Poly_STATIC Poly-EP) + add_dependencies(Polyxx_STATIC Poly-EP) + endif() endif() diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f78e951d3..1dd005dd7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1355,14 +1355,18 @@ if(ENABLE_VALGRIND) target_include_directories(cvc5-obj PUBLIC ${Valgrind_INCLUDE_DIR}) endif() if(USE_ABC) - target_include_directories(cvc5-obj PUBLIC ${ABC_INCLUDE_DIR}) + target_include_directories(cvc5-obj PRIVATE ${ABC_INCLUDE_DIR}) target_link_libraries(cvc5-obj PUBLIC ${ABC_LIBRARIES}) endif() target_link_libraries(cvc5-obj PUBLIC CaDiCaL) if(USE_CLN) - target_link_libraries(cvc5-obj PUBLIC CLN) + target_include_directories(cvc5-obj PRIVATE ${CLN_INCLUDE_DIR}) + target_link_libraries(cvc5-shared PRIVATE CLN_SHARED) + if(ENABLE_STATIC_LIBRARY) + target_link_libraries(cvc5-static PUBLIC CLN_STATIC) + endif() endif() if(USE_CRYPTOMINISAT) target_link_libraries(cvc5-obj PUBLIC CryptoMiniSat) @@ -1375,7 +1379,11 @@ if(USE_GLPK) target_include_directories(cvc5-obj PUBLIC ${GLPK_INCLUDE_DIR}) endif() if(USE_POLY) - target_link_libraries(cvc5-obj PUBLIC Polyxx) + target_include_directories(cvc5-obj PRIVATE ${Poly_INCLUDE_DIR}) + target_link_libraries(cvc5-shared PRIVATE Polyxx_SHARED) + if(ENABLE_STATIC_LIBRARY) + target_link_libraries(cvc5-static PUBLIC Polyxx_STATIC) + endif() endif() if(USE_COCOA) target_link_libraries(cvc5-obj PUBLIC CoCoA) diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 1aedcb265..8cd96b3f1 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -52,6 +52,12 @@ add_dependencies(main gen-tokens) add_library(main-test driver_unified.cpp $<TARGET_OBJECTS:main>) target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC5DRIVER) target_link_libraries(main-test PUBLIC cvc5-shared cvc5parser-shared) +if(USE_CLN) + target_link_libraries(main-test PUBLIC CLN_SHARED) +endif() +if(USE_POLY) + target_link_libraries(main-test PUBLIC Polyxx_SHARED) +endif() #-----------------------------------------------------------------------------# # cvc5 binary configuration @@ -83,6 +89,7 @@ if(ENABLE_STATIC_BINARY) set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_START_STATIC ON) set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_END_STATIC ON) endif() + set_target_properties(cvc5-bin PROPERTIES INSTALL_RPATH "") endif() if(USE_EDITLINE) |