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).

1 files changed, 10 insertions, 30 deletions

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>