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.

diff --git a/.github/actions/configure-and-build/action.yml b/.github/actions/configure-and-build/action.yml
index 4e2bea7a19646492fa7d51ef416a408518258b8d..ace887be17b486f9b378011f07b34c54a8e8b77e 100644 (file)
--- 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 bc3936d477e219524486d195a4f4d49dccd73737..ba4502b954f0f91c8b954130cd8702cbe7ac13f4 100644 (file)
--- 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 <cvc5/cvc5.h>\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 fedcb9bb4cea39c8b2d533818fa695935b399b18..f8faab276ca0d732a1eea555ad4520b02535cd91 100644 (file)
--- 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 ef3b7636ed86f697da2abc17ac42d850b6f70971..11e12d89a5783d16846f0dabf39979fdf5664ff8 100644 (file)
--- 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 e479c15d05f622126eac9aaf6cb951a878065e4f..04b377b123a7a5c15621d5cf8ab103eb3b3a2959 100644 (file)
--- 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 bc4afda235a6c384ccb5d9e87b3242d2372ec014..dc8a63255a4e2ba74734e4fa8b85169ec049dcbd 100644 (file)
--- 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 3f83b61e26343810ede30780bb5e83c265f71f3b..0255141899ee4220f76f5837e4c69a24dd205a66 100644 (file)
--- 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)
                      <INSTALL_DIR>/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 bea0e1bf169d12357b4642505496842f178d3157..b6db900547a51dd1e0862e4b69dbf75834329c47 100644 (file)
--- 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
-        <SOURCE_DIR>/configure --enable-shared --disable-static
-        --prefix=<INSTALL_DIR>/gmp-shared
-        --enable-cxx --with-pic --host=${TOOLCHAIN_PREFIX}
-      BUILD_BYPRODUCTS <INSTALL_DIR>/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
-        <SOURCE_DIR>/configure --disable-shared --enable-static
-        --prefix=<INSTALL_DIR>/gmp-static
-        --enable-cxx --with-pic --host=${TOOLCHAIN_PREFIX}
-      BUILD_BYPRODUCTS <INSTALL_DIR>/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
-        <SOURCE_DIR>/configure --enable-shared --enable-static
-        --prefix=<INSTALL_DIR>
-        --enable-cxx --with-pic --host=${TOOLCHAIN_PREFIX}
-      BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libgmp.a
-                       <INSTALL_DIR>/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
+      <SOURCE_DIR>/configure ${LINK_OPTS} --prefix=<INSTALL_DIR>
+      --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 e19e1c57d05badbee22f7363759dd80c5c6a826b..1bfb2f7ccc40aa55a3f64c37e0a835121be545b1 100644 (file)
--- 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
             <INSTALL_DIR>/lib/libpicpoly.a
@@ -122,13 +113,16 @@ if(NOT Poly_FOUND_SYSTEM)
     DEPENDEES install
     COMMAND ${CMAKE_COMMAND} -E remove_directory <BINARY_DIR>/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>" "${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 5275c620fe1b5ec65dc66004cb5cc1409908dc85..6b238fb38ae52b92fbb20818312e16eaf1f056f3 100644 (file)
--- 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 b7a2ca280525935167def093a8a70c08f4f60b0f..319af54c5ee4218a77f74868efbde7205f20e869 100755 (executable)
--- 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 99c9ea3113a67cba98c10176409e3f9bfc09fda9..d08e63e0f99fa721f0fd5b9998b4edc69bef4d69 100644 (file)
--- 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 '<output_dir>/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 5f77128a4fccb10ef6d5f96460d2753235e971a3..268668dfd7500043f5ef43ed9786814e57aa8924 100644 (file)
--- 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 $<TARGET_OBJECTS:cvc5-obj> $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
+
+set_target_properties(cvc5 PROPERTIES OUTPUT_NAME cvc5)
+
 # Link the shared library
-add_library(cvc5-shared SHARED $<TARGET_OBJECTS:cvc5-obj> $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
-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
     $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
     $<INSTALL_INTERFACE:include>
 )
-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 $<TARGET_OBJECTS:cvc5-obj> $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
-  set_target_properties(cvc5-static PROPERTIES OUTPUT_NAME cvc5)
-  target_include_directories(cvc5-static
-    PUBLIC
-      $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
-      $<INSTALL_INTERFACE:include>
-  )
-  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 5f522f4d10703da74c516d50166e90ca44964df7..ad4183f25e9e87e765274c6b506ebc2272729541 100644 (file)
--- 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 96fcd67a01079bbe31977029345774aa2866eb28..235e28100dc093f29df61ef15172957377888661 100644 (file)
--- 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 cb83413f9a43831cfe71d2b71bbe675a7441bf75..51809975c677aa17a9aea2fdb5e008a9a45a15c9 100644 (file)
--- 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_OBJECTS:main>)
 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_OBJECTS:main>)
-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 d012851d7c84984dc9dfa45337b6035e54e0a8f4..4fd2993ed5922c2b1d5f3af5ad7257a59b9ca7b7 100644 (file)
--- 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 $<TARGET_OBJECTS:cvc5parser-objs>)
-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 $<TARGET_OBJECTS:cvc5parser-objs>)
+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 $<TARGET_OBJECTS:cvc5parser-objs>)
-  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 bbfc2a74b9fa6543a8d5134238e16d9ce8dbe46e..24158e00b0ce8bb8e6fb82d294d36e016cd1f6a3 100644 (file)
--- 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)