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).
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")
# 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()
#-----------------------------------------------------------------------------#
# 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
# 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()
#-----------------------------------------------------------------------------#
#-----------------------------------------------------------------------------#
include(ConfigureCvc5)
-if(NOT ENABLE_SHARED)
+if(ENABLE_STATIC_BINARY)
set(CVC5_STATIC_BUILD ON)
endif()
# 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
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})
# 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
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")
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)
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)
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)
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)
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()
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(
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")
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}")
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()
)
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)
python_bindings=default
java_bindings=default
editline=default
-shared=default
+static_library=default
static_binary=default
statistics=default
tracing=default
--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;;
[ $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 ] \
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'
# 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
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")
OUTPUT_NAME cvc5
)
-add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5)
+add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5-shared)
${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_...
)
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)
)
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)
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>
#-----------------------------------------------------------------------------#
# 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.
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)
projects / cvc5.git / commitdiff