From e1f69a43e9ee7e4a63f3c4a1881001bc650c9df7 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 4 Nov 2021 11:43:42 -0700 Subject: [PATCH] Refactor cmake to build either static or shared (#7534) This PR simplifies the cmake setup to only build either shared or statically. It also attempts to fix windows builds, both shared and static. --- .../actions/configure-and-build/action.yml | 2 +- .github/actions/run-tests/action.yml | 8 +- .github/workflows/ci.yml | 15 ++- CMakeLists.txt | 30 ++++- cmake/ConfigCompetition.cmake | 2 +- cmake/FindANTLR3.cmake | 2 +- cmake/FindCLN.cmake | 41 +++---- cmake/FindGMP.cmake | 115 +++++------------- cmake/FindPoly.cmake | 85 +++++-------- cmake/cvc5Config.cmake.in | 2 +- configure.sh | 10 +- examples/CMakeLists.txt | 3 +- src/CMakeLists.txt | 85 ++++--------- src/api/java/CMakeLists.txt | 6 +- src/api/python/CMakeLists.txt | 8 +- src/main/CMakeLists.txt | 16 ++- src/parser/CMakeLists.txt | 26 ++-- test/unit/CMakeLists.txt | 2 +- 18 files changed, 178 insertions(+), 280 deletions(-) diff --git a/.github/actions/configure-and-build/action.yml b/.github/actions/configure-and-build/action.yml index 4e2bea7a1..ace887be1 100644 --- a/.github/actions/configure-and-build/action.yml +++ b/.github/actions/configure-and-build/action.yml @@ -44,7 +44,7 @@ runs: echo "::group::Static build" if [[ "${{ inputs.build-static }}" != "true" ]]; then exit 0; fi ${{ inputs.configure-env }} ./configure.sh ${{ inputs.configure-config }} \ - --prefix=$(pwd)/build-static/install --werror --static --name=build-static + --prefix=$(pwd)/build-static/install --werror --static --name=build-static --no-java-bindings cd build-static/ && pwd=$(pwd) $SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir = $pwd" $CCACHE_CONFIGPATH diff --git a/.github/actions/run-tests/action.yml b/.github/actions/run-tests/action.yml index bc3936d47..ba4502b95 100644 --- a/.github/actions/run-tests/action.yml +++ b/.github/actions/run-tests/action.yml @@ -5,12 +5,14 @@ inputs: default: build/ check-examples: default: true + check-install: + default: true check-python-bindings: default: false check-unit-tests: default: true regressions-args: - default: "--no-check-unsat-cores --no-check-proofs" + default: "" regressions-exclude: default: "3-4" runs: @@ -36,6 +38,7 @@ runs: - name: Install Check shell: bash run: | + if [[ "${{ inputs.check-install }}" != "true" ]]; then exit 0; fi make -j${{ env.num_proc }} install echo -e "#include \nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp g++ -std=c++17 /tmp/test.cpp -I install/include -L install/lib -lcvc5 @@ -52,8 +55,7 @@ runs: shell: bash run: | if [[ "${{ inputs.check-examples }}" != "true" ]]; then exit 0; fi - mkdir build - cd build + mkdir -p build && cd build cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake make -j${{ env.num_proc }} ctest -j${{ env.num_proc }} --output-on-failure diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fedcb9bb4..f8faab276 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -8,7 +8,7 @@ jobs: include: - name: ubuntu:production os: ubuntu-latest - config: production --auto-download --all-bindings --editline --docs --static + config: production --auto-download --all-bindings --editline --docs cache-key: production python-bindings: true build-documentation: true @@ -19,7 +19,7 @@ jobs: - name: macos:production os: macos-11 - config: production --auto-download --all-bindings --editline --static + config: production --auto-download --all-bindings --editline cache-key: production python-bindings: true check-examples: true @@ -89,6 +89,17 @@ jobs: check-unit-tests: ${{ matrix.check-units }} regressions-args: ${{ matrix.run_regression_args }} regressions-exclude: ${{ matrix.exclude_regress }} + + - name: Run tests + uses: ./.github/actions/run-tests + with: + build-dir: ${{ steps.configure-and-build.outputs.static-build-dir }} + check-examples: false + check-install: false + check-python-bindings: false + check-unit-tests: ${{ matrix.check-units }} + regressions-args: ${{ matrix.run_regression_args }} + regressions-exclude: 1-4 - name: Build documentation if: matrix.build-documentation diff --git a/CMakeLists.txt b/CMakeLists.txt index ef3b7636e..11e12d89a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -70,6 +70,7 @@ option(ENABLE_GPL "Enable GPL dependencies") # >> 3-valued: IGNORE ON OFF # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for build types +option(BUILD_SHARED_LIBS "Build shared libraries and binary") cvc5_option(ENABLE_ASAN "Enable ASAN build") cvc5_option(ENABLE_UBSAN "Enable UBSan build") cvc5_option(ENABLE_TSAN "Enable TSan build") @@ -83,7 +84,6 @@ cvc5_option(ENABLE_STATISTICS "Enable statistics") cvc5_option(ENABLE_TRACING "Enable tracing") cvc5_option(ENABLE_UNIT_TESTING "Enable unit testing") cvc5_option(ENABLE_VALGRIND "Enable valgrind instrumentation") -cvc5_option(ENABLE_STATIC_BUILD "Enable building static libraries and binary") cvc5_option(ENABLE_AUTO_DOWNLOAD "Enable automatic download of dependencies") cvc5_option(ENABLE_IPO "Enable interprocedural optimization") # >> 2-valued: ON OFF @@ -263,6 +263,20 @@ enable_testing() #-----------------------------------------------------------------------------# # Check options, find packages and configure build. +if(BUILD_SHARED_LIBS) + if (WIN32) + set(CMAKE_FIND_LIBRARY_SUFFIXES .dll .lib .a) + else() + set(CMAKE_FIND_LIBRARY_SUFFIXES .so .dylib .a) + endif() +else() + if (WIN32) + set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a .dll) + else() + set(CMAKE_FIND_LIBRARY_SUFFIXES .a .so .dylib) + endif() +endif() + if(USE_PYTHON2) find_package(PythonInterp 2.7 REQUIRED) else() @@ -440,7 +454,9 @@ include(fuzzing-murxla) #-----------------------------------------------------------------------------# include(ConfigureCvc5) -if(ENABLE_STATIC_BUILD) +if(BUILD_SHARED_LIBS) + set(CVC5_STATIC_BUILD OFF) +else() set(CVC5_STATIC_BUILD ON) endif() @@ -449,6 +465,10 @@ endif() add_subdirectory(src) +if(BUILD_BINDINGS_PYTHON AND NOT BUILD_SHARED_LIBS) + message(STATUS "Python bindings can only be built in a shared build.") + set(BUILD_BINDINGS_PYTHON OFF) +endif() if(BUILD_BINDINGS_PYTHON) set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR}) add_subdirectory(src/api/python) @@ -481,9 +501,9 @@ include(CMakePackageConfigHelpers) # (in the assumption that only reasonably experienced users use this and # also that custom installation prefixes are not used for longer periods of # time anyway). Also, we print a big warning with further instructions. -if(NOT ENABLE_STATIC_BUILD) +if(BUILD_SHARED_LIBS) # Get the libraries that cvc5 links against - get_target_property(libs cvc5-shared INTERFACE_LINK_LIBRARIES) + get_target_property(libs cvc5 INTERFACE_LINK_LIBRARIES) set(LIBS_SHARED_FROM_DEPS "") foreach(lib ${libs}) # Filter out those that are linked dynamically and come from deps/install @@ -592,7 +612,7 @@ print_config("Profiling (gprof) " ${ENABLE_PROFILING}) print_config("Unit tests " ${ENABLE_UNIT_TESTING}) print_config("Valgrind " ${ENABLE_VALGRIND}) message("") -print_config("Static build " ${ENABLE_STATIC_BUILD}) +print_config("Shared build " ${BUILD_SHARED_LIBS}) print_config("Python bindings " ${BUILD_BINDINGS_PYTHON}) print_config("Java bindings " ${BUILD_BINDINGS_JAVA}) print_config("Python2 " ${USE_PYTHON2}) diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake index e479c15d0..04b377b12 100644 --- a/cmake/ConfigCompetition.cmake +++ b/cmake/ConfigCompetition.cmake @@ -32,7 +32,7 @@ cvc5_set_option(ENABLE_DUMPING OFF) # enable_muzzle=yes cvc5_set_option(ENABLE_MUZZLE ON) # enable_valgrind=no -cvc5_set_option(ENABLE_STATIC_BUILD ON) +cvc5_set_option(BUILD_SHARED_LIBS OFF) cvc5_set_option(ENABLE_UNIT_TESTING OFF) # By default, we include all dependencies in our competition build that are diff --git a/cmake/FindANTLR3.cmake b/cmake/FindANTLR3.cmake index bc4afda23..dc8a63255 100644 --- a/cmake/FindANTLR3.cmake +++ b/cmake/FindANTLR3.cmake @@ -33,7 +33,7 @@ if(ANTLR3_JAR AND ANTLR3_INCLUDE_DIR AND ANTLR3_LIBRARIES) check_system_version("ANTLR3") endif() -if(ENABLE_STATIC_BUILD AND ANTLR3_FOUND_SYSTEM) +if(NOT BUILD_SHARED_LIBS AND ANTLR3_FOUND_SYSTEM) force_static_library() find_library(ANTLR3_STATIC_LIBRARIES NAMES antlr3c) if(NOT ANTLR3_STATIC_LIBRARIES) diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake index 3f83b61e2..025514189 100644 --- a/cmake/FindCLN.cmake +++ b/cmake/FindCLN.cmake @@ -33,15 +33,6 @@ if(CLN_INCLUDE_DIR AND CLN_LIBRARIES) check_system_version("CLN") endif() -if(ENABLE_STATIC_BUILD 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) @@ -77,31 +68,28 @@ if(NOT CLN_FOUND_SYSTEM) /lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX} ) - add_dependencies(CLN-EP GMP_SHARED) + add_dependencies(CLN-EP GMP) set(CLN_INCLUDE_DIR "${DEPS_BASE}/include/") - set(CLN_LIBRARIES "${DEPS_BASE}/lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}") - set(CLN_STATIC_LIBRARIES "${DEPS_BASE}/lib/libcln.a") + if(BUILD_SHARED_LIBS) + set(CLN_LIBRARIES "${DEPS_BASE}/lib/libcln${CMAKE_SHARED_LIBRARY_SUFFIX}") + else() + set(CLN_STATIC_LIBRARIES "${DEPS_BASE}/lib/libcln.a") + endif() endif() set(CLN_FOUND TRUE) -add_library(CLN_SHARED SHARED IMPORTED GLOBAL) -set_target_properties(CLN_SHARED PROPERTIES +if(BUILD_SHARED_LIBS) + add_library(CLN SHARED IMPORTED GLOBAL) +else() + add_library(CLN STATIC IMPORTED GLOBAL) +endif() +set_target_properties(CLN PROPERTIES IMPORTED_LOCATION "${CLN_LIBRARIES}" INTERFACE_INCLUDE_DIRECTORIES "${CLN_INCLUDE_DIR}" ) -target_link_libraries(CLN_SHARED INTERFACE GMP_SHARED) - - -if(ENABLE_STATIC_BUILD) - 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() +target_link_libraries(CLN INTERFACE GMP) mark_as_advanced(AUTORECONF) mark_as_advanced(CLN_FOUND) @@ -113,6 +101,5 @@ if(CLN_FOUND_SYSTEM) message(STATUS "Found CLN ${CLN_VERSION}: ${CLN_LIBRARIES}") else() message(STATUS "Building CLN ${CLN_VERSION}: ${CLN_LIBRARIES}") - add_dependencies(CLN_SHARED CLN-EP) - add_dependencies(CLN_STATIC CLN-EP) + add_dependencies(CLN CLN-EP) endif() diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index bea0e1bf1..b6db90054 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -42,16 +42,6 @@ if(GMP_INCLUDE_DIR AND GMP_LIBRARIES) check_system_version("GMP") endif() -if(ENABLE_STATIC_BUILD AND GMP_FOUND_SYSTEM) - force_static_library() - find_library(GMP_STATIC_LIBRARIES NAMES gmp) - if(NOT GMP_STATIC_LIBRARIES) - set(GMP_FOUND_SYSTEM FALSE) - endif() - set(GMP_STATIC_INCLUDE_DIR "${GMP_INCLUDE_DIR}") - reset_force_static_library() -endif() - if(NOT GMP_FOUND_SYSTEM) check_ep_downloaded("GMP-EP") if(NOT GMP-EP_DOWNLOADED) @@ -62,83 +52,47 @@ if(NOT GMP_FOUND_SYSTEM) set(GMP_VERSION "6.2.1") - if(CMAKE_SYSTEM_NAME STREQUAL "Windows") - # on windows, the gmp.h is different for shared and static builds. - # we thus need two separate builds. as the configure script taints the - # source folder, we even need two source folders. - ExternalProject_Add( - GMP-EP-shared - ${COMMON_EP_CONFIG} - URL https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2 - URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822 - DOWNLOAD_NAME gmp-${GMP_VERSION}-shared.tar.bz2 - CONFIGURE_COMMAND - /configure --enable-shared --disable-static - --prefix=/gmp-shared - --enable-cxx --with-pic --host=${TOOLCHAIN_PREFIX} - BUILD_BYPRODUCTS /gmp-shared/lib/libgmp.dll.a - ) - ExternalProject_Add( - GMP-EP-static - ${COMMON_EP_CONFIG} - URL https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2 - URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822 - DOWNLOAD_NAME gmp-${GMP_VERSION}-static.tar.bz2 - CONFIGURE_COMMAND - /configure --disable-shared --enable-static - --prefix=/gmp-static - --enable-cxx --with-pic --host=${TOOLCHAIN_PREFIX} - BUILD_BYPRODUCTS /gmp-static/lib/libgmp.a - ) - - add_custom_target(GMP-EP DEPENDS GMP-EP-shared GMP-EP-static) - - set(GMP_INCLUDE_DIR "${DEPS_BASE}/gmp-shared/include/") - set(GMP_STATIC_INCLUDE_DIR "${DEPS_BASE}/gmp-static/include/") - set(GMP_LIBRARIES "${DEPS_BASE}/gmp-shared/lib/libgmp.dll.a") - set(GMP_STATIC_LIBRARIES "${DEPS_BASE}/gmp-static/lib/libgmp.a") - - file(MAKE_DIRECTORY "${GMP_INCLUDE_DIR}") - file(MAKE_DIRECTORY "${GMP_STATIC_INCLUDE_DIR}") + set(GMP_INCLUDE_DIR "${DEPS_BASE}/include/") + if(BUILD_SHARED_LIBS) + set(LINK_OPTS --enable-shared --disable-static) + if(CMAKE_SYSTEM_NAME STREQUAL "Windows") + set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp.dll.a") + else() + set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp${CMAKE_SHARED_LIBRARY_SUFFIX}") + endif() else() - ExternalProject_Add( - GMP-EP - ${COMMON_EP_CONFIG} - URL https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2 - URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822 - CONFIGURE_COMMAND - /configure --enable-shared --enable-static - --prefix= - --enable-cxx --with-pic --host=${TOOLCHAIN_PREFIX} - BUILD_BYPRODUCTS /lib/libgmp.a - /lib/libgmp${CMAKE_SHARED_LIBRARY_SUFFIX} - ) - - set(GMP_INCLUDE_DIR "${DEPS_BASE}/include/") - set(GMP_STATIC_INCLUDE_DIR "${DEPS_BASE}/include/") - set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp${CMAKE_SHARED_LIBRARY_SUFFIX}") - set(GMP_STATIC_LIBRARIES "${DEPS_BASE}/lib/libgmp.a") + set(LINK_OPTS --disable-shared --enable-static) + set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp.a") endif() + + + ExternalProject_Add( + GMP-EP + ${COMMON_EP_CONFIG} + URL https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2 + URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822 + CONFIGURE_COMMAND + /configure ${LINK_OPTS} --prefix= + --with-pic --enable-cxx --host=${TOOLCHAIN_PREFIX} + BUILD_BYPRODUCTS ${GMP_LIBRARIES} + ) endif() set(GMP_FOUND TRUE) -add_library(GMP_SHARED SHARED IMPORTED GLOBAL) -set_target_properties(GMP_SHARED PROPERTIES + +if(BUILD_SHARED_LIBS) + add_library(GMP SHARED IMPORTED GLOBAL) + if(CMAKE_SYSTEM_NAME STREQUAL "Windows") + set_target_properties(GMP PROPERTIES IMPORTED_IMPLIB "${GMP_LIBRARIES}") + endif() +else() + add_library(GMP STATIC IMPORTED GLOBAL) +endif() +set_target_properties(GMP PROPERTIES IMPORTED_LOCATION "${GMP_LIBRARIES}" INTERFACE_INCLUDE_DIRECTORIES "${GMP_INCLUDE_DIR}" ) -if(CMAKE_SYSTEM_NAME STREQUAL "Windows") - set_target_properties(GMP_SHARED PROPERTIES IMPORTED_IMPLIB "${GMP_LIBRARIES}") -endif() - -if(ENABLE_STATIC_BUILD) - add_library(GMP_STATIC STATIC IMPORTED GLOBAL) - set_target_properties(GMP_STATIC PROPERTIES - IMPORTED_LOCATION "${GMP_STATIC_LIBRARIES}" - INTERFACE_INCLUDE_DIRECTORIES "${GMP_STATIC_INCLUDE_DIR}" - ) -endif() mark_as_advanced(GMP_FOUND) mark_as_advanced(GMP_FOUND_SYSTEM) @@ -149,8 +103,5 @@ if(GMP_FOUND_SYSTEM) message(STATUS "Found GMP ${GMP_VERSION}: ${GMP_LIBRARIES}") else() message(STATUS "Building GMP ${GMP_VERSION}: ${GMP_LIBRARIES}") - add_dependencies(GMP_SHARED GMP-EP) - if(ENABLE_STATIC_BUILD) - add_dependencies(GMP_STATIC GMP-EP) - endif() + add_dependencies(GMP GMP-EP) endif() diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake index e19e1c57d..1bfb2f7cc 100644 --- a/cmake/FindPoly.cmake +++ b/cmake/FindPoly.cmake @@ -37,16 +37,6 @@ if(Poly_INCLUDE_DIR check_system_version("Poly") endif() -if(ENABLE_STATIC_BUILD 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) @@ -66,8 +56,8 @@ if(NOT Poly_FOUND_SYSTEM) unset(patchcmd) endif() - get_target_property(GMP_INCLUDE_DIR GMP_SHARED INTERFACE_INCLUDE_DIRECTORIES) - get_target_property(GMP_LIBRARY GMP_SHARED IMPORTED_LOCATION) + get_target_property(GMP_INCLUDE_DIR GMP INTERFACE_INCLUDE_DIRECTORIES) + get_target_property(GMP_LIBRARY GMP IMPORTED_LOCATION) get_filename_component(GMP_LIB_PATH "${GMP_LIBRARY}" DIRECTORY) set(POLY_BYPRODUCTS @@ -109,7 +99,8 @@ if(NOT Poly_FOUND_SYSTEM) -DLIBPOLY_BUILD_STATIC_PIC=ON -DCMAKE_INCLUDE_PATH=${GMP_INCLUDE_DIR} -DCMAKE_LIBRARY_PATH=${GMP_LIB_PATH} - BUILD_COMMAND ${CMAKE_MAKE_PROGRAM} static_pic_poly static_pic_polyxx + BUILD_COMMAND ${CMAKE_MAKE_PROGRAM} + COMMAND ${CMAKE_MAKE_PROGRAM} static_pic_poly static_pic_polyxx INSTALL_COMMAND ${CMAKE_MAKE_PROGRAM} install COMMAND ${CMAKE_COMMAND} -E copy src/libpicpoly.a /lib/libpicpoly.a @@ -122,13 +113,16 @@ if(NOT Poly_FOUND_SYSTEM) DEPENDEES install COMMAND ${CMAKE_COMMAND} -E remove_directory /test/ ) - add_dependencies(Poly-EP GMP_SHARED) + add_dependencies(Poly-EP GMP) set(Poly_INCLUDE_DIR "${DEPS_BASE}/include/") - 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") + if(BUILD_SHARED_LIBS) + set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}") + set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpolyxx${CMAKE_SHARED_LIBRARY_SUFFIX}") + else() + set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpicpoly.a") + set(PolyXX_LIBRARIES "${DEPS_BASE}/lib/libpicpolyxx.a") + endif() if(CMAKE_SYSTEM_NAME STREQUAL "Windows") set(Poly_LIBRARIES "${DEPS_BASE}/bin/libpoly${CMAKE_SHARED_LIBRARY_SUFFIX}") @@ -138,41 +132,29 @@ endif() set(Poly_FOUND TRUE) -add_library(Poly_SHARED SHARED IMPORTED GLOBAL) -set_target_properties(Poly_SHARED PROPERTIES + +if(BUILD_SHARED_LIBS) + add_library(Poly SHARED IMPORTED GLOBAL) + add_library(Polyxx SHARED IMPORTED GLOBAL) + if(CMAKE_SYSTEM_NAME STREQUAL "Windows") + set_target_properties(Poly PROPERTIES IMPORTED_IMPLIB "${Poly_LIBRARIES}") + set_target_properties(Polyxx PROPERTIES IMPORTED_IMPLIB "${PolyXX_LIBRARIES}") + endif() +else() + add_library(Poly STATIC IMPORTED GLOBAL) + add_library(Polyxx STATIC IMPORTED GLOBAL) +endif() + +set_target_properties(Poly PROPERTIES IMPORTED_LOCATION "${Poly_LIBRARIES}" INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}" ) -if(CMAKE_SYSTEM_NAME STREQUAL "Windows") - set_target_properties(Poly_SHARED PROPERTIES IMPORTED_IMPLIB "${Poly_LIBRARIES}") -endif() -target_link_libraries(Poly_SHARED INTERFACE GMP_SHARED) - -add_library(Polyxx_SHARED SHARED IMPORTED GLOBAL) -set_target_properties(Polyxx_SHARED PROPERTIES +target_link_libraries(Poly INTERFACE GMP) +set_target_properties(Polyxx PROPERTIES IMPORTED_LOCATION "${PolyXX_LIBRARIES}" INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}" - INTERFACE_LINK_LIBRARIES Poly_SHARED + INTERFACE_LINK_LIBRARIES Poly ) -if(CMAKE_SYSTEM_NAME STREQUAL "Windows") - set_target_properties(Polyxx_SHARED PROPERTIES IMPORTED_IMPLIB "${PolyXX_LIBRARIES}") -endif() - -if(ENABLE_STATIC_BUILD) - 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) @@ -184,8 +166,8 @@ if(Poly_FOUND_SYSTEM) message(STATUS "Found Poly ${Poly_VERSION}: ${Poly_LIBRARIES}") else() message(STATUS "Building Poly ${Poly_VERSION}: ${Poly_LIBRARIES}") - add_dependencies(Poly_SHARED Poly-EP) - add_dependencies(Polyxx_SHARED Poly-EP) + add_dependencies(Poly Poly-EP) + add_dependencies(Polyxx Poly-EP) ExternalProject_Get_Property(Poly-EP BUILD_BYPRODUCTS INSTALL_DIR) string(REPLACE "" "${INSTALL_DIR}" BUILD_BYPRODUCTS "${BUILD_BYPRODUCTS}") @@ -193,9 +175,4 @@ else() ${BUILD_BYPRODUCTS} DESTINATION ${CMAKE_INSTALL_LIBDIR} ) - - if(ENABLE_STATIC_BUILD) - add_dependencies(Poly_STATIC Poly-EP) - add_dependencies(Polyxx_STATIC Poly-EP) - endif() endif() diff --git a/cmake/cvc5Config.cmake.in b/cmake/cvc5Config.cmake.in index 5275c620f..6b238fb38 100644 --- a/cmake/cvc5Config.cmake.in +++ b/cmake/cvc5Config.cmake.in @@ -17,7 +17,7 @@ set(CVC5_BINDINGS_JAVA @BUILD_BINDINGS_JAVA@) set(CVC5_BINDINGS_PYTHON @BUILD_BINDINGS_PYTHON@) set(CVC5_BINDINGS_PYTHON_VERSION @BUILD_BINDINGS_PYTHON_VERSION@) -if(NOT TARGET cvc5::cvc5-shared) +if(NOT TARGET cvc5::cvc5) include(${CMAKE_CURRENT_LIST_DIR}/cvc5Targets.cmake) endif() diff --git a/configure.sh b/configure.sh index b7a2ca280..319af54c5 100755 --- a/configure.sh +++ b/configure.sh @@ -126,7 +126,7 @@ python2=default python_bindings=default java_bindings=default editline=default -static=default +build_shared=ON statistics=default tracing=default tsan=default @@ -238,8 +238,8 @@ do --muzzle) muzzle=ON;; --no-muzzle) muzzle=OFF;; - --static) static=ON;; - --no-static) static=OFF;; + --static) build_shared=OFF;; + --no-static) build_shared=ON;; --auto-download) auto_download=ON;; --no-auto-download) auto_download=OFF;; @@ -339,8 +339,8 @@ fi [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja" [ $muzzle != default ] \ && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" -[ $static != default ] \ - && cmake_opts="$cmake_opts -DENABLE_STATIC_BUILD=$static" +[ $build_shared != default ] \ + && cmake_opts="$cmake_opts -DBUILD_SHARED_LIBS=$build_shared" [ $statistics != default ] \ && cmake_opts="$cmake_opts -DENABLE_STATISTICS=$statistics" [ $tracing != default ] \ diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 99c9ea311..d08e63e0f 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -54,7 +54,7 @@ macro(cvc5_add_example name src_files output_dir) endif() add_executable(${name} ${src_files_list}) - target_link_libraries(${name} cvc5::cvc5-shared cvc5::cvc5parser-shared) + target_link_libraries(${name} cvc5::cvc5 cvc5::cvc5parser) # The test target is prefixed with the path, # e.g., for '/myexample.cpp' @@ -105,6 +105,7 @@ if(TARGET cvc5::cvc5jar) endif() if(CVC5_BINDINGS_PYTHON) + message(STATUS "with Python examples") # If legacy Python API has been built add_subdirectory(api/python) endif() diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5f77128a4..268668dfd 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1276,53 +1276,38 @@ add_dependencies(cvc5-obj cvc5base cvc5context) # Add libcvc5 dependencies for generated sources. add_dependencies(cvc5-obj gen-expr gen-versioninfo gen-options gen-tags gen-theory) +add_library(cvc5 $ $ $) + +set_target_properties(cvc5 PROPERTIES OUTPUT_NAME cvc5) + # Link the shared library -add_library(cvc5-shared SHARED $ $ $) -set_target_properties(cvc5-shared PROPERTIES SOVERSION ${CVC5_SOVERSION}) -set_target_properties(cvc5-shared PROPERTIES OUTPUT_NAME cvc5) -target_include_directories(cvc5-shared +target_include_directories(cvc5 PUBLIC $ $ ) -install(TARGETS cvc5-shared +install(TARGETS cvc5 EXPORT cvc5-targets LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR} ) -if(ENABLE_STATIC_BUILD) - add_library(cvc5-static STATIC $ $ $) - set_target_properties(cvc5-static PROPERTIES OUTPUT_NAME cvc5) - target_include_directories(cvc5-static - PUBLIC - $ - $ - ) - install(TARGETS cvc5-static - EXPORT cvc5-targets - LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} - ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}) -endif() - include(GenerateExportHeader) generate_export_header(cvc5-obj BASE_NAME cvc5) # Add library/include dependencies -add_dependencies(cvc5-obj GMP_SHARED) +add_dependencies(cvc5-obj GMP) target_include_directories(cvc5-obj PRIVATE ${GMP_INCLUDE_DIR}) -target_link_libraries(cvc5-shared PRIVATE GMP_SHARED) -if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC GMP_STATIC) +if(BUILD_SHARED_LIBS) + target_link_libraries(cvc5 PRIVATE GMP) +else() + target_link_libraries(cvc5 PUBLIC GMP) endif() # 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(cvc5-shared PRIVATE ${RT_LIBRARIES}) -if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PRIVATE ${RT_LIBRARIES}) -endif() +target_link_libraries(cvc5 PRIVATE ${RT_LIBRARIES}) if(ENABLE_VALGRIND) target_include_directories(cvc5-obj PUBLIC ${Valgrind_INCLUDE_DIR}) @@ -1330,65 +1315,45 @@ endif() add_dependencies(cvc5-obj CaDiCaL) target_include_directories(cvc5-obj PRIVATE ${CaDiCaL_INCLUDE_DIR}) -target_link_libraries(cvc5-shared PRIVATE CaDiCaL) -if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC CaDiCaL) -endif() +target_link_libraries(cvc5 PRIVATE CaDiCaL) if(USE_CLN) - add_dependencies(cvc5-obj CLN_SHARED) + add_dependencies(cvc5-obj CLN) target_include_directories(cvc5-obj PRIVATE ${CLN_INCLUDE_DIR}) - target_link_libraries(cvc5-shared PRIVATE CLN_SHARED) - if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC CLN_STATIC) - endif() + target_link_libraries(cvc5 PRIVATE CLN) endif() if(USE_CRYPTOMINISAT) add_dependencies(cvc5-obj CryptoMiniSat) target_include_directories(cvc5-obj PRIVATE ${CryptoMiniSat_INCLUDE_DIR}) - target_link_libraries(cvc5-shared PRIVATE CryptoMiniSat) - if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC CryptoMiniSat) - endif() + target_link_libraries(cvc5 PRIVATE CryptoMiniSat) endif() if(USE_KISSAT) add_dependencies(cvc5-obj Kissat) target_include_directories(cvc5-obj PRIVATE ${Kissat_INCLUDE_DIR}) - target_link_libraries(cvc5-shared PRIVATE Kissat) - if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC Kissat) - endif() + target_link_libraries(cvc5 PRIVATE Kissat) endif() if(USE_GLPK) target_include_directories(cvc5-obj PRIVATE ${GLPK_INCLUDE_DIR}) - target_link_libraries(cvc5-shared PRIVATE ${GLPK_LIBRARIES}) - if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC ${GLPK_LIBRARIES}) - endif() + target_link_libraries(cvc5 PRIVATE ${GLPK_LIBRARIES}) endif() if(USE_POLY) - add_dependencies(cvc5-obj Polyxx_SHARED) + add_dependencies(cvc5-obj Polyxx) target_include_directories(cvc5-obj PRIVATE ${Poly_INCLUDE_DIR}) - target_link_libraries(cvc5-shared PRIVATE Polyxx_SHARED) - if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC Polyxx_STATIC) + if(BUILD_SHARED_LIBS) + target_link_libraries(cvc5 PRIVATE Polyxx) + else() + target_link_libraries(cvc5 PUBLIC Polyxx) endif() endif() if(USE_COCOA) add_dependencies(cvc5-obj CoCoA) target_include_directories(cvc5-obj PRIVATE ${CoCoA_INCLUDE_DIR}) - target_link_libraries(cvc5-shared PRIVATE CoCoA) - if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC CoCoA) - endif() + target_link_libraries(cvc5 PRIVATE CoCoA) endif() add_dependencies(cvc5-obj SymFPU) target_include_directories(cvc5-obj PRIVATE ${SymFPU_INCLUDE_DIR}) -target_link_libraries(cvc5-shared PRIVATE SymFPU) -if(ENABLE_STATIC_BUILD) - target_link_libraries(cvc5-static PUBLIC SymFPU) -endif() +target_link_libraries(cvc5 PRIVATE SymFPU) #-----------------------------------------------------------------------------# # Visit main subdirectory after creating target cvc5. For target main, we have diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 5f522f4d1..ad4183f25 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -109,7 +109,7 @@ message(STATUS "JAVA_INCLUDE_PATH : ${JAVA_INCLUDE_PATH}") message(STATUS "JAVA_INCLUDE_PATH2 : ${JAVA_INCLUDE_PATH2}") message(STATUS "JAVA_AWT_INCLUDE_PATH: ${JAVA_AWT_INCLUDE_PATH}") -add_library(cvc5jni SHARED +add_library(cvc5jni jni/api_utilities.cpp jni/datatype.cpp jni/datatype_constructor.cpp @@ -133,7 +133,7 @@ target_include_directories(cvc5jni PUBLIC ${PROJECT_SOURCE_DIR}/src) target_include_directories(cvc5jni PUBLIC ${CMAKE_BINARY_DIR}/src/) target_include_directories(cvc5jni PUBLIC ${JNI_DIR}) target_link_libraries(cvc5jni PRIVATE ${JNI_LIBRARIES}) -target_link_libraries(cvc5jni PRIVATE cvc5-shared) +target_link_libraries(cvc5jni PRIVATE cvc5) set(CVC5_JAR "cvc5-${CVC5_VERSION}.jar") @@ -146,4 +146,4 @@ add_jar(cvc5jar ) set_target_properties(cvc5jar PROPERTIES SOURCES "${JAVA_FILES}") -add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5-shared) +add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5) diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 96fcd67a0..235e28100 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -13,12 +13,6 @@ # The build system configuration. ## -if(POLICY CMP0057) - # For cmake >= 3.3 this policy changed the behavior of IN_LIST - # if the policy exists, we use the NEW behavior - cmake_policy(SET CMP0057 NEW) -endif() - # Check that scikit-build is installed # Provides CMake files for Python bindings check_python_module("skbuild" "scikit-build") @@ -92,7 +86,7 @@ target_include_directories(pycvc5 ${CMAKE_BINARY_DIR}/src # for cvc5_export.h ) -target_link_libraries(pycvc5 cvc5-shared) +target_link_libraries(pycvc5 cvc5) # Disable -Werror and other warnings for code generated by Cython. set(PY_SRC_FLAGS "") diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index cb83413f9..51809975c 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -35,7 +35,7 @@ set_source_files_properties(${libmain_gen_src_files} PROPERTIES GENERATED TRUE) # main-test library. add_library(main OBJECT ${libmain_src_files} ${libmain_gen_src_files}) -target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER) +target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER -Dcvc5_obj_EXPORTS) set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON) add_dependencies(main gen-tokens cvc5-obj) @@ -45,19 +45,19 @@ add_dependencies(main gen-tokens cvc5-obj) # test. Do not link against main-test in any other case. add_library(main-test driver_unified.cpp $) target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC5DRIVER) -target_link_libraries(main-test PUBLIC cvc5-shared cvc5parser-shared) +target_link_libraries(main-test PUBLIC cvc5 cvc5parser) if(USE_CLN) - target_link_libraries(main-test PUBLIC CLN_SHARED) + target_link_libraries(main-test PUBLIC CLN) endif() if(USE_POLY) - target_link_libraries(main-test PUBLIC Polyxx_SHARED) + target_link_libraries(main-test PUBLIC Polyxx) endif() #-----------------------------------------------------------------------------# # cvc5 binary configuration add_executable(cvc5-bin driver_unified.cpp main.cpp $) -target_compile_definitions(cvc5-bin PRIVATE -D__BUILDING_CVC5DRIVER) +target_compile_definitions(cvc5-bin PRIVATE -D__BUILDING_CVC5DRIVER -Dcvc5_obj_EXPORTS) set_target_properties(cvc5-bin PROPERTIES OUTPUT_NAME cvc5 @@ -76,17 +76,15 @@ endif() # use the static system libraries. # https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_START_STATIC.html # https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_END_STATIC.html -if(ENABLE_STATIC_BUILD) +if(NOT BUILD_SHARED_LIBS) if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin") set_target_properties(cvc5-bin PROPERTIES LINK_FLAGS -static) 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 "") - target_link_libraries(cvc5-bin PUBLIC cvc5-static cvc5parser-static) -else() - target_link_libraries(cvc5-bin PUBLIC cvc5-shared cvc5parser-shared) endif() +target_link_libraries(cvc5-bin PUBLIC cvc5 cvc5parser) if(USE_EDITLINE) target_link_libraries(cvc5-bin PUBLIC ${Editline_LIBRARIES}) diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index d012851d7..4fd2993ed 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -114,27 +114,19 @@ target_compile_definitions(cvc5parser-objs PUBLIC -D__BUILDING_CVC5PARSERLIB -Dc add_dependencies(cvc5parser-objs ANTLR3) target_include_directories(cvc5parser-objs PRIVATE ${ANTLR3_INCLUDE_DIR}) -add_library(cvc5parser-shared SHARED $) -set_target_properties(cvc5parser-shared PROPERTIES SOVERSION ${CVC5_SOVERSION}) -set_target_properties(cvc5parser-shared PROPERTIES OUTPUT_NAME cvc5parser) -target_link_libraries(cvc5parser-shared PRIVATE cvc5-shared) -target_link_libraries(cvc5parser-shared PRIVATE ANTLR3) +add_library(cvc5parser $) +if(BUILD_SHARED_LIBS) + set_target_properties(cvc5parser PROPERTIES SOVERSION ${CVC5_SOVERSION}) +endif() + +set_target_properties(cvc5parser PROPERTIES OUTPUT_NAME cvc5parser) +target_link_libraries(cvc5parser PRIVATE cvc5) +target_link_libraries(cvc5parser PRIVATE ANTLR3) -install(TARGETS cvc5parser-shared +install(TARGETS cvc5parser-objs cvc5parser EXPORT cvc5-targets DESTINATION ${CMAKE_INSTALL_LIBDIR}) -if(ENABLE_STATIC_BUILD) - add_library(cvc5parser-static STATIC $) - set_target_properties(cvc5parser-static PROPERTIES OUTPUT_NAME cvc5parser) - target_link_libraries(cvc5parser-static PRIVATE cvc5-static) - target_link_libraries(cvc5parser-static PRIVATE ANTLR3) - - install(TARGETS cvc5parser-objs cvc5parser-static - EXPORT cvc5-targets - DESTINATION ${CMAKE_INSTALL_LIBDIR}) -endif() - # The generated lexer/parser files define some functions as # __declspec(dllexport) via the ANTLR3_API macro, which leads to lots of # unresolved symbols when linking against libcvc5parser. diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index bbfc2a74b..24158e00b 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -41,7 +41,7 @@ macro(cvc5_add_unit_test is_white name output_dir) add_executable(${name} ${test_src}) target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK}) gtest_add_tests(TARGET ${name}) - target_link_libraries(${name} PUBLIC main-test GMP_SHARED) + target_link_libraries(${name} PUBLIC main-test GMP) target_link_libraries(${name} PUBLIC GTest::Main) target_link_libraries(${name} PUBLIC GTest::GTest) -- 2.30.2