Refactor our static builds (#7251)

This PR does a major refactoring on how we organize our builds to allow both shared and static builds. We now build the libraries using object libraries to allow building the libraries both dynamically and statically in the same build folder, though the static library is optional (ENABLE_STATIC_LIBRARY). The binary is linked either dynamically or statically (depending on ENABLE_STATIC_BINARY).

18 files changed, 183 insertions, 140 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 054d4938c..aaad41e9f 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -102,7 +102,7 @@ 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_SHARED         "Build as shared library")
+cvc5_option(ENABLE_STATIC_LIBRARY "Enable building static library")
 cvc5_option(ENABLE_STATIC_BINARY
             "Build static binaries with statically linked system libraries")
 cvc5_option(ENABLE_AUTO_DOWNLOAD  "Enable automatic download of dependencies")
@@ -248,9 +248,8 @@ endif()
 # already set the option, which we don't want to overwrite.
 
 if(ENABLE_STATIC_BINARY)
-  cvc5_set_option(ENABLE_SHARED OFF)
-else()
-  cvc5_set_option(ENABLE_SHARED ON)
+  message(STATUS "Enable static library for static binary build.")
+  cvc5_set_option(ENABLE_STATIC_LIBRARY ON)
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -268,19 +267,7 @@ endif()
 # This needs to be set before any find_package(...) command since we want to
 # search for static libraries with suffix .a.
 
-if(ENABLE_SHARED)
-  set(BUILD_SHARED_LIBS ON)
-  if(ENABLE_STATIC_BINARY)
-    set(ENABLE_STATIC_BINARY OFF)
-    message(STATUS "Disabling static binary since shared build is enabled.")
-  endif()
-
-  # Set visibility to default if unit tests are enabled
-  if(ENABLE_UNIT_TESTING)
-    set(CMAKE_CXX_VISIBILITY_PRESET default)
-    set(CMAKE_VISIBILITY_INLINES_HIDDEN 0)
-  endif()
-
+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
@@ -298,27 +285,12 @@ if(ENABLE_SHARED)
   # 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")
-else()
-  # When building statically, we *only* want static archives/libraries
-  if (WIN32)
-      set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a)
-  else()
-      set(CMAKE_FIND_LIBRARY_SUFFIXES .a)
-  endif()
-  set(BUILD_SHARED_LIBS OFF)
-  cvc5_set_option(ENABLE_STATIC_BINARY ON)
-
-  # Never build unit tests as static binaries, otherwise we'll end up with
-  # ~300MB per unit test.
-  if(ENABLE_UNIT_TESTING)
-    message(STATUS "Disabling unit tests since static build is enabled.")
-    set(ENABLE_UNIT_TESTING OFF)
-  endif()
+endif()
 
-  if (BUILD_BINDINGS_PYTHON)
-    message(FATAL_ERROR "Building Python bindings is not possible "
-                        "when building statically")
-  endif()
+# Set visibility to default if unit tests are enabled
+if(ENABLE_UNIT_TESTING)
+  set(CMAKE_CXX_VISIBILITY_PRESET default)
+  set(CMAKE_VISIBILITY_INLINES_HIDDEN 0)
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -512,7 +484,7 @@ include(IWYU)
 #-----------------------------------------------------------------------------#
 
 include(ConfigureCvc5)
-if(NOT ENABLE_SHARED)
+if(ENABLE_STATIC_BINARY)
   set(CVC5_STATIC_BUILD ON)
 endif()
 
@@ -553,7 +525,7 @@ include(CMakePackageConfigHelpers)
 # time anyway). Also, we print a big warning with further instructions.
 if(NOT ENABLE_STATIC_BINARY)
   # Get the libraries that cvc5 links against
-  get_target_property(libs cvc5 INTERFACE_LINK_LIBRARIES)
+  get_target_property(libs cvc5-shared INTERFACE_LINK_LIBRARIES)
   set(LIBS_SHARED_FROM_DEPS "")
   foreach(lib ${libs})
     # Filter out those that are linked dynamically and come from deps/install
@@ -662,7 +634,7 @@ print_config("Profiling (gprof)         " ${ENABLE_PROFILING})
 print_config("Unit tests                " ${ENABLE_UNIT_TESTING})
 print_config("Valgrind                  " ${ENABLE_VALGRIND})
 message("")
-print_config("Shared libs               " ${ENABLE_SHARED})
+print_config("Static library            " ${ENABLE_STATIC_LIBRARY})
 print_config("Static binary             " ${ENABLE_STATIC_BINARY})
 print_config("Python bindings           " ${BUILD_BINDINGS_PYTHON})
 print_config("Java bindings             " ${BUILD_BINDINGS_JAVA})
diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake
index 785f792d4..2b17d8073 100644
--- a/cmake/ConfigCompetition.cmake
+++ b/cmake/ConfigCompetition.cmake
@@ -32,8 +32,7 @@ cvc5_set_option(ENABLE_DUMPING OFF)
 # enable_muzzle=yes
 cvc5_set_option(ENABLE_MUZZLE ON)
 # enable_valgrind=no
-# enable_shared=no
-cvc5_set_option(ENABLE_SHARED OFF)
+cvc5_set_option(ENABLE_STATIC_BINARY ON)
 cvc5_set_option(ENABLE_UNIT_TESTING OFF)
 
 # By default, we include all dependencies in our competition build that are
diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake
index e802da2ef..f2a6d853e 100644
--- a/cmake/FindCLN.cmake
+++ b/cmake/FindCLN.cmake
@@ -67,7 +67,7 @@ if(NOT CLN_FOUND_SYSTEM)
     BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libcln.a
   )
 
-  add_dependencies(CLN-EP GMP)
+  add_dependencies(CLN-EP GMP_SHARED)
 
   set(CLN_INCLUDE_DIR "${DEPS_BASE}/include/")
   set(CLN_LIBRARIES "${DEPS_BASE}/lib/libcln.a")
@@ -76,10 +76,15 @@ endif()
 set(CLN_FOUND TRUE)
 
 add_library(CLN STATIC IMPORTED GLOBAL)
-set_target_properties(CLN PROPERTIES IMPORTED_LOCATION "${CLN_LIBRARIES}")
-set_target_properties(
-  CLN PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${CLN_INCLUDE_DIR}"
+set_target_properties(CLN PROPERTIES
+  IMPORTED_LOCATION "${CLN_LIBRARIES}"
+  INTERFACE_INCLUDE_DIRECTORIES "${CLN_INCLUDE_DIR}"
 )
+if(ENABLE_STATIC_LIBRARY)
+  target_link_libraries(CLN INTERFACE GMP_STATIC)
+else()
+  target_link_libraries(CLN INTERFACE GMP_SHARED)
+endif()
 
 mark_as_advanced(AUTORECONF)
 mark_as_advanced(CLN_FOUND)
diff --git a/cmake/FindEditline.cmake b/cmake/FindEditline.cmake
index 4fa2f892b..1038424a3 100644
--- a/cmake/FindEditline.cmake
+++ b/cmake/FindEditline.cmake
@@ -40,6 +40,12 @@ if(Editline_INCLUDE_DIRS)
   unset(CMAKE_REQUIRED_QUIET)
   unset(CMAKE_REQUIRED_LIBRARIES)
   unset(CMAKE_REQUIRED_INCLUDES)
+
+  if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+    set(Editline_LIBRARIES ${Editline_LIBRARIES})
+  else()
+    set(Editline_LIBRARIES ${Editline_LIBRARIES} bsd tinfo)
+  endif()
 endif()
 
 include(FindPackageHandleStandardArgs)
diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake
index c554197b9..d6780ed24 100644
--- a/cmake/FindGMP.cmake
+++ b/cmake/FindGMP.cmake
@@ -42,6 +42,15 @@ if(GMP_INCLUDE_DIR AND GMP_LIBRARIES)
   check_system_version("GMP")
 endif()
 
+if(ENABLE_STATIC_LIBRARY 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()
+  reset_force_static_library()
+endif()
+
 if(NOT GMP_FOUND_SYSTEM)
   check_ep_downloaded("GMP-EP")
   if(NOT GMP-EP_DOWNLOADED)
@@ -59,22 +68,31 @@ if(NOT GMP_FOUND_SYSTEM)
     URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822
     CONFIGURE_COMMAND
       <SOURCE_DIR>/configure --prefix=<INSTALL_DIR> --enable-cxx --with-pic
-      --disable-shared --enable-static --host=${TOOLCHAIN_PREFIX}
-    BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libgmp.a
+      --enable-shared --enable-static --host=${TOOLCHAIN_PREFIX}
+    BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libgmp.a <INSTALL_DIR>/lib/libgmp.so
   )
 
   set(GMP_INCLUDE_DIR "${DEPS_BASE}/include/")
-  set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp.a")
+  set(GMP_LIBRARIES "${DEPS_BASE}/lib/libgmp.so")
+  set(GMP_STATIC_LIBRARIES "${DEPS_BASE}/lib/libgmp.a")
 endif()
 
 set(GMP_FOUND TRUE)
 
-add_library(GMP STATIC IMPORTED GLOBAL)
-set_target_properties(GMP PROPERTIES IMPORTED_LOCATION "${GMP_LIBRARIES}")
-set_target_properties(
-  GMP PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${GMP_INCLUDE_DIR}"
+add_library(GMP_SHARED SHARED IMPORTED GLOBAL)
+set_target_properties(GMP_SHARED PROPERTIES
+  IMPORTED_LOCATION "${GMP_LIBRARIES}"
+  INTERFACE_INCLUDE_DIRECTORIES "${GMP_INCLUDE_DIR}"
 )
 
+if(ENABLE_STATIC_LIBRARY)
+  add_library(GMP_STATIC STATIC IMPORTED GLOBAL)
+  set_target_properties(GMP_STATIC PROPERTIES
+    IMPORTED_LOCATION "${GMP_STATIC_LIBRARIES}"
+    INTERFACE_INCLUDE_DIRECTORIES "${GMP_INCLUDE_DIR}"
+  )
+endif()
+
 mark_as_advanced(GMP_FOUND)
 mark_as_advanced(GMP_FOUND_SYSTEM)
 mark_as_advanced(GMP_INCLUDE_DIR)
@@ -84,5 +102,8 @@ if(GMP_FOUND_SYSTEM)
   message(STATUS "Found GMP ${GMP_VERSION}: ${GMP_LIBRARIES}")
 else()
   message(STATUS "Building GMP ${GMP_VERSION}: ${GMP_LIBRARIES}")
-  add_dependencies(GMP GMP-EP)
+  add_dependencies(GMP_SHARED GMP-EP)
+  if(ENABLE_STATIC_LIBRARY)
+    add_dependencies(GMP_STATIC GMP-EP)
+  endif()
 endif()
diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake
index e11d85c3f..6ddb918a9 100644
--- a/cmake/FindPoly.cmake
+++ b/cmake/FindPoly.cmake
@@ -66,8 +66,8 @@ if(NOT Poly_FOUND_SYSTEM)
     unset(patchcmd)
   endif()
 
-  get_target_property(GMP_INCLUDE_DIR GMP INTERFACE_INCLUDE_DIRECTORIES)
-  get_target_property(GMP_LIBRARY GMP IMPORTED_LOCATION)
+  get_target_property(GMP_INCLUDE_DIR GMP_SHARED INTERFACE_INCLUDE_DIRECTORIES)
+  get_target_property(GMP_LIBRARY GMP_SHARED IMPORTED_LOCATION)
   get_filename_component(GMP_LIB_PATH "${GMP_LIBRARY}" DIRECTORY)
 
   ExternalProject_Add(
@@ -101,7 +101,7 @@ if(NOT Poly_FOUND_SYSTEM)
     DEPENDEES install
     COMMAND ${CMAKE_COMMAND} -E remove_directory <BINARY_DIR>/test/
   )
-  add_dependencies(Poly-EP GMP)
+  add_dependencies(Poly-EP GMP_SHARED)
 
   set(Poly_INCLUDE_DIR "${DEPS_BASE}/include/")
   set(Poly_LIBRARIES "${DEPS_BASE}/lib/libpicpoly.a")
@@ -115,7 +115,11 @@ set_target_properties(Poly PROPERTIES IMPORTED_LOCATION "${Poly_LIBRARIES}")
 set_target_properties(
   Poly PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${Poly_INCLUDE_DIR}"
 )
-target_link_libraries(Poly INTERFACE GMP)
+if(ENABLE_STATIC_LIBRARY)
+  target_link_libraries(Poly INTERFACE GMP_STATIC)
+else()
+  target_link_libraries(Poly INTERFACE GMP_SHARED)
+endif()
 
 add_library(Polyxx STATIC IMPORTED GLOBAL)
 set_target_properties(Polyxx PROPERTIES IMPORTED_LOCATION "${PolyXX_LIBRARIES}")
diff --git a/cmake/cvc5Config.cmake.in b/cmake/cvc5Config.cmake.in
index 6b238fb38..5275c620f 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)
+if(NOT TARGET cvc5::cvc5-shared)
   include(${CMAKE_CURRENT_LIST_DIR}/cvc5Targets.cmake)
 endif()
 
diff --git a/cmake/deps-helper.cmake b/cmake/deps-helper.cmake
index f37ccb1f2..f2a43c028 100644
--- a/cmake/deps-helper.cmake
+++ b/cmake/deps-helper.cmake
@@ -39,6 +39,23 @@ if(CMAKE_VERSION VERSION_GREATER_EQUAL "3.14")
     )
 endif()
 
+macro(force_static_library)
+    message(STATUS "before: ${CMAKE_FIND_LIBRARY_SUFFIXES}")
+    if (WIN32)
+        set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a)
+    else()
+        set(CMAKE_FIND_LIBRARY_SUFFIXES .a)
+    endif()
+endmacro(force_static_library)
+
+macro(reset_force_static_library)
+    if (WIN32)
+        set(CMAKE_FIND_LIBRARY_SUFFIXES .dll)
+    else()
+        set(CMAKE_FIND_LIBRARY_SUFFIXES .so .dylib)
+    endif()
+endmacro(reset_force_static_library)
+
 macro(check_auto_download name disable_option)
     if(NOT ENABLE_AUTO_DOWNLOAD)
         if (${name}_FIND_VERSION)
diff --git a/configure.sh b/configure.sh
index 07c1cc4ae..4fc274612 100755
--- a/configure.sh
+++ b/configure.sh
@@ -131,7 +131,7 @@ python2=default
 python_bindings=default
 java_bindings=default
 editline=default
-shared=default
+static_library=default
 static_binary=default
 statistics=default
 tracing=default
@@ -249,8 +249,8 @@ do
     --muzzle) muzzle=ON;;
     --no-muzzle) muzzle=OFF;;
 
-    --static) shared=OFF; static_binary=ON;;
-    --no-static) shared=ON;;
+    --static) static_library=ON; static_binary=ON;;
+    --no-static) static_library=OFF;;
 
     --static-binary) static_binary=ON;;
     --no-static-binary) static_binary=OFF;;
@@ -356,8 +356,8 @@ fi
 [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja"
 [ $muzzle != default ] \
   && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle"
-[ $shared != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared"
+[ $static_library != default ] \
+  && cmake_opts="$cmake_opts -ENABLE_STATIC_LIBRARY=$static_library"
 [ $static_binary != default ] \
   && cmake_opts="$cmake_opts -DENABLE_STATIC_BINARY=$static_binary"
 [ $statistics != default ] \
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 86634bc0c..99c9ea311 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 cvc5::cvc5parser)
+  target_link_libraries(${name} cvc5::cvc5-shared cvc5::cvc5parser-shared)
 
   # The test target is prefixed with the path,
   # e.g., for '<output_dir>/myexample.cpp'
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6c03db7e7..18312f7c0 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1295,63 +1295,89 @@ add_subdirectory(util)
 # LIBCVC5_GEN_SRCS (via libcvc5_add_sources). We can now build libcvc5.
 
 set_source_files_properties(${LIBCVC5_GEN_SRCS} PROPERTIES GENERATED TRUE)
-add_library(cvc5 ${LIBCVC5_SRCS} ${LIBCVC5_GEN_SRCS}
-  $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
-target_include_directories(cvc5
+
+# First build the object library
+add_library(cvc5-obj OBJECT ${LIBCVC5_SRCS} ${LIBCVC5_GEN_SRCS})
+target_compile_definitions(cvc5-obj PRIVATE -D__BUILDING_CVC5LIB)
+set_target_properties(cvc5-obj PROPERTIES POSITION_INDEPENDENT_CODE ON)
+target_link_libraries(cvc5-obj PUBLIC $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>)
+# add_dependencies() is necessary for cmake versions before 3.21
+add_dependencies(cvc5-obj cvc5base cvc5context)
+# Add libcvc5 dependencies for generated sources.
+add_dependencies(cvc5-obj gen-expr gen-gitinfo gen-options gen-tags gen-theory)
+
+# Link the shared library
+add_library(cvc5-shared SHARED)
+target_link_libraries(cvc5-shared PRIVATE cvc5-obj)
+set_target_properties(cvc5-shared PROPERTIES SOVERSION ${CVC5_SOVERSION})
+set_target_properties(cvc5-shared PROPERTIES OUTPUT_NAME cvc5)
+target_include_directories(cvc5-shared
   PUBLIC
     $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}>
     $<INSTALL_INTERFACE:include>
 )
-
-include(GenerateExportHeader)
-generate_export_header(cvc5)
-
-install(TARGETS cvc5
+install(TARGETS cvc5-shared
   EXPORT cvc5-targets
   LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
-  ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR})
+  ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}
+)
 
-set_target_properties(cvc5 PROPERTIES SOVERSION ${CVC5_SOVERSION})
-target_compile_definitions(cvc5 PRIVATE -D__BUILDING_CVC5LIB)
-# Add libcvc5 dependencies for generated sources.
-add_dependencies(cvc5 gen-expr gen-gitinfo gen-options gen-tags gen-theory)
+if(ENABLE_STATIC_LIBRARY)
+  add_library(cvc5-static STATIC)
+  target_link_libraries(cvc5-static PRIVATE cvc5-obj)
+  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-obj 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
+target_include_directories(cvc5-obj PRIVATE ${GMP_INCLUDE_DIR})
+target_link_libraries(cvc5-shared PRIVATE GMP_SHARED)
+if(ENABLE_STATIC_LIBRARY)
+  target_link_libraries(cvc5-static PUBLIC GMP_STATIC)
+endif()
+
 if(ENABLE_VALGRIND)
-  target_include_directories(cvc5 PRIVATE ${Valgrind_INCLUDE_DIR})
+  target_include_directories(cvc5-obj PUBLIC ${Valgrind_INCLUDE_DIR})
 endif()
 if(USE_ABC)
-  target_link_libraries(cvc5 PRIVATE ${ABC_LIBRARIES})
-  target_include_directories(cvc5 PRIVATE ${ABC_INCLUDE_DIR})
+  target_include_directories(cvc5-obj PUBLIC ${ABC_INCLUDE_DIR})
+  target_link_libraries(cvc5-obj PUBLIC ${ABC_LIBRARIES})
 endif()
 
-target_link_libraries(cvc5 PRIVATE CaDiCaL)
+target_link_libraries(cvc5-obj PUBLIC CaDiCaL)
 
 if(USE_CLN)
-  target_link_libraries(cvc5 PRIVATE CLN)
+  target_link_libraries(cvc5-obj PUBLIC CLN)
 endif()
 if(USE_CRYPTOMINISAT)
-  target_link_libraries(cvc5 PRIVATE CryptoMiniSat)
+  target_link_libraries(cvc5-obj PUBLIC CryptoMiniSat)
 endif()
 if(USE_KISSAT)
-  target_link_libraries(cvc5 PRIVATE Kissat)
+  target_link_libraries(cvc5-obj PUBLIC Kissat)
 endif()
 if(USE_GLPK)
-  target_link_libraries(cvc5 PRIVATE ${GLPK_LIBRARIES})
-  target_include_directories(cvc5 PRIVATE ${GLPK_INCLUDE_DIR})
+  target_link_libraries(cvc5-obj PUBLIC ${GLPK_LIBRARIES})
+  target_include_directories(cvc5-obj PUBLIC ${GLPK_INCLUDE_DIR})
 endif()
 if(USE_POLY)
-  target_link_libraries(cvc5 PRIVATE Polyxx)
+  target_link_libraries(cvc5-obj PUBLIC Polyxx)
 endif()
 if(USE_COCOA)
-  target_link_libraries(cvc5 PRIVATE CoCoA)
+  target_link_libraries(cvc5-obj PUBLIC CoCoA)
 endif()
 
-target_link_libraries(cvc5 PRIVATE SymFPU)
-
-# Note: When linked statically GMP needs to be linked after CLN since CLN
-# depends on GMP.
-target_link_libraries(cvc5 PRIVATE GMP)
+target_link_libraries(cvc5-obj PUBLIC 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 69605c06a..a2fc1dba9 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -127,7 +127,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)
+target_link_libraries(cvc5jni PRIVATE cvc5-shared)
 
 set(CVC5_JAR "cvc5-${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}.jar")
 
@@ -139,4 +139,4 @@ add_jar(cvc5jar
   OUTPUT_NAME cvc5
 )
 
-add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5)
+add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5-shared)
diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index 7ee559a6a..dce0208cb 100644
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -92,7 +92,7 @@ target_include_directories(pycvc5
   ${CMAKE_BINARY_DIR}/src         # for cvc5_export.h
 )
 
-target_link_libraries(pycvc5 cvc5)
+target_link_libraries(pycvc5 cvc5-shared)
 
 # Disable -Werror and other warnings for code generated by Cython.
 # Note: Visibility is reset to default here since otherwise the PyInit_...
diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index 8d79fb764..78f6cd069 100644
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -84,8 +84,6 @@ set_source_files_properties(
 )
 
 add_library(cvc5base OBJECT ${LIBBASE_SOURCES})
-if(ENABLE_SHARED)
-  set_target_properties(cvc5base PROPERTIES POSITION_INDEPENDENT_CODE ON)
-endif()
+set_target_properties(cvc5base PROPERTIES POSITION_INDEPENDENT_CODE ON)
 target_compile_definitions(cvc5base PRIVATE -D__BUILDING_CVC5LIB)
 add_dependencies(cvc5base gen-gitinfo gen-tags)
diff --git a/src/context/CMakeLists.txt b/src/context/CMakeLists.txt
index 6cc066235..00b4d91ee 100644
--- a/src/context/CMakeLists.txt
+++ b/src/context/CMakeLists.txt
@@ -34,7 +34,5 @@ set(LIBCONTEXT_SOURCES
 )
 
 add_library(cvc5context OBJECT ${LIBCONTEXT_SOURCES})
-if(ENABLE_SHARED)
-  set_target_properties(cvc5context PROPERTIES POSITION_INDEPENDENT_CODE ON)
-endif()
+set_target_properties(cvc5context PROPERTIES POSITION_INDEPENDENT_CODE ON)
 target_compile_definitions(cvc5context PRIVATE -D__BUILDING_CVC5LIB)
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 8ce0ba754..4d528312e 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -36,53 +36,33 @@ set_source_files_properties(${libmain_gen_src_files} PROPERTIES GENERATED TRUE)
 
 add_library(main OBJECT ${libmain_src_files} ${libmain_gen_src_files})
 target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER)
-if(ENABLE_SHARED)
-  set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON)
-endif()
-
-# We can't use target_link_libraries(main ...) here since this is only
-# supported for cmake version >= 3.12. Hence, we have to manually add the
-# library dependencies for main. As a consequence, include directories from
-# dependencies are not propagated and we need to manually add the include
-# directories of libcvc5 to main.
-add_dependencies(main cvc5 cvc5parser gen-tokens)
+set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON)
 
-# Note: This should not be required anymore as soon as we get rid of the
-#       smt_engine.h include in src/main. smt_engine.h has transitive includes
-#       of GMP and CLN via sexpr.h and therefore needs GMP/CLN headers.
-if(USE_CLN)
-  get_target_property(CLN_INCLUDES CLN INTERFACE_INCLUDE_DIRECTORIES)
-  target_include_directories(main PRIVATE ${CLN_INCLUDES})
+if(ENABLE_STATIC_BINARY)
+  target_link_libraries(main PUBLIC cvc5-static cvc5parser-static)
+else()
+  target_link_libraries(main PUBLIC cvc5-shared cvc5parser-shared)
 endif()
-get_target_property(GMP_INCLUDES GMP INTERFACE_INCLUDE_DIRECTORIES)
-target_include_directories(main PRIVATE ${GMP_INCLUDES})
+
+add_dependencies(main gen-tokens)
 
 # main-test library is only used for linking against api and unit tests so
 # that we don't have to include all object files of main into each api/unit
 # 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 cvc5parser)
-if(USE_CLN)
-  target_link_libraries(main-test PUBLIC CLN)
-endif()
-target_link_libraries(main-test PUBLIC GMP)
+target_link_libraries(main-test PUBLIC cvc5-shared cvc5parser-shared)
 
 #-----------------------------------------------------------------------------#
 # cvc5 binary configuration
 
-add_executable(cvc5-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>)
+add_executable(cvc5-bin driver_unified.cpp main.cpp)
+target_link_libraries(cvc5-bin PRIVATE main)
 target_compile_definitions(cvc5-bin PRIVATE -D__BUILDING_CVC5DRIVER)
 set_target_properties(cvc5-bin
   PROPERTIES
     OUTPUT_NAME cvc5
     RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
-target_link_libraries(cvc5-bin PUBLIC cvc5 cvc5parser)
-if(USE_CLN)
-  target_link_libraries(cvc5-bin PUBLIC CLN)
-endif()
-target_link_libraries(cvc5-bin PUBLIC GMP)
-
 if(PROGRAM_PREFIX)
   install(PROGRAMS
     $<TARGET_FILE:cvc5-bin>
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 589bfad1f..32ddfee52 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -98,16 +98,33 @@ endforeach()
 #-----------------------------------------------------------------------------#
 # libcvc5parser configuration
 
-add_library(cvc5parser ${libcvc5parser_src_files})
-set_target_properties(cvc5parser PROPERTIES SOVERSION ${CVC5_SOVERSION})
-target_compile_definitions(cvc5parser PRIVATE -D__BUILDING_CVC5PARSERLIB)
-target_link_libraries(cvc5parser PUBLIC cvc5)
-target_link_libraries(cvc5parser PRIVATE ANTLR3)
+add_library(cvc5parser-objs OBJECT ${libcvc5parser_src_files})
+set_target_properties(cvc5parser-objs PROPERTIES POSITION_INDEPENDENT_CODE ON)
+target_compile_definitions(cvc5parser-objs PUBLIC -D__BUILDING_CVC5PARSERLIB)
+target_link_libraries(cvc5parser-objs PRIVATE ANTLR3)
 
-install(TARGETS cvc5parser
+
+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 cvc5parser-objs)
+
+install(TARGETS cvc5parser-shared
   EXPORT cvc5-targets
   DESTINATION ${CMAKE_INSTALL_LIBDIR})
 
+if(ENABLE_STATIC_LIBRARY)
+  add_library(cvc5parser-static STATIC)
+  set_target_properties(cvc5parser-static PROPERTIES OUTPUT_NAME cvc5parser)
+  target_link_libraries(cvc5parser-static PRIVATE cvc5parser-objs)
+  target_link_libraries(cvc5parser-static PRIVATE cvc5-static)
+
+  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 7196cc915..2e15cff4b 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)
+  target_link_libraries(${name} PUBLIC main-test GMP_SHARED)
   target_link_libraries(${name} PUBLIC GTest::Main)
   target_link_libraries(${name} PUBLIC GTest::GTest)