Fix/Improve static and shared builds with CLN or Poly (#7306)

We already created two dependency targets `GMP_SHARED` and `GMP_STATIC`, as we could not use `libgmp.a` for shared linking (as it is built without `-fPIC`). This PR fixes our handling of CLN and Poly: they would always link with `GMP_STATIC`, leading to having both `GMP_SHARED` and `GMP_STATIC` in the linker command line in certain situations. We now also have `*_SHARED` and `*_STATIC` for both CLN and Poly.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 8e5a9c7e77b3394c1f2e21985dcd4616c4e087b5..07ff3c76f7180debe922bd8658a6050a927edfb7 100644 (file)
--- 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 f2a6d853e326271dd82dea279332e75e0729450a..11bf8ed98a8bc29013c9a3613256b143b6a62d74 100644 (file)
--- 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 6ddb918a92885e3217ddfa5a0d10b076319ef92f..ae236c6d9b6ea8549d4005d83805c9bd5922fb9d 100644 (file)
--- 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 f78e951d36ed0bdadcc475bd9e821620de721a1e..1dd005dd792d2f82462c81d8481e6d2c56be169f 100644 (file)
--- 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 1aedcb265c36e07311b60b24c9a6623edfd172d8..8cd96b3f19ba018dc97c1d4b70371874bed5ad62 100644 (file)
--- 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)