cvc4_set_option(USE_READLINE ON)
endif()
-#-----------------------------------------------------------------------------#
-# Static libraries
+# Only enable unit testing if assertions are enabled. Otherwise, unit tests
+# that expect AssertionException to be thrown will fail.
+if(NOT ENABLE_ASSERTIONS)
+ set(ENABLE_UNIT_TESTING OFF)
+endif()
+
+# Never build unit tests as static binaries, otherwise we'll end up with
+# ~300MB per unit test.
+if(ENABLE_UNIT_TESTING)
+ set(ENABLE_SHARED ON)
+endif()
+#-----------------------------------------------------------------------------#
+# Shared/static libraries
+#
# This needs to be set before any find_package(...) command since we want to
# search for static libraries with suffix .a.
-if(NOT ENABLE_SHARED)
- set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
- set(CMAKE_EXE_LINKER_FLAGS "-static")
+
+if(ENABLE_SHARED)
+ set(BUILD_SHARED_LIBS ON)
+else()
+ set(CMAKE_FIND_LIBRARY_SUFFIXES ".a ${CMAKE_FIND_LIBRARY_SUFFIXES}")
set(BUILD_SHARED_LIBS OFF)
+ # This is required to force find_package(Boost) to use static libraries.
+ set(Boost_USE_STATIC_LIBS ON)
endif()
#-----------------------------------------------------------------------------#
set(GMP_HOME ${GMP_DIR})
find_package(GMP REQUIRED)
-libcvc4_link_libraries(${GMP_LIBRARIES})
-libcvc4_include_directories(${GMP_INCLUDE_DIR})
if(ENABLE_ASAN)
# -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
add_definitions(-DCVC4_ASSERTIONS)
else()
add_definitions(-DNDEBUG)
- # Only enable unit testing if assertions are enabled. Otherwise, unit tests
- # that expect AssertionException to be thrown will fail.
- set(ENABLE_UNIT_TESTING OFF)
endif()
if(ENABLE_COVERAGE)
if(ENABLE_UNIT_TESTING)
find_package(CxxTest REQUIRED)
- # Force shared libs for unit tests, static libs with unit tests are not
- # working right now.
- set(ENABLE_SHARED ON)
-endif()
-
-if(ENABLE_SHARED)
- set(BUILD_SHARED_LIBS ON)
endif()
if(ENABLE_STATISTICS)
if(ENABLE_VALGRIND)
find_package(Valgrind REQUIRED)
- libcvc4_include_directories(${Valgrind_INCLUDE_DIR})
add_definitions(-DCVC4_VALGRIND)
endif()
if(USE_ABC)
set(ABC_HOME "${ABC_DIR}")
find_package(ABC REQUIRED)
- libcvc4_link_libraries(${ABC_LIBRARIES})
- libcvc4_include_directories(${ABC_INCLUDE_DIR})
add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
endif()
if(USE_CADICAL)
set(CaDiCaL_HOME ${CADICAL_DIR})
find_package(CaDiCaL REQUIRED)
- libcvc4_link_libraries(${CaDiCaL_LIBRARIES})
- libcvc4_include_directories(${CaDiCaL_INCLUDE_DIR})
add_definitions(-DCVC4_USE_CADICAL)
endif()
if(USE_CLN)
set(GPL_LIBS "${GPL_LIBS} cln")
find_package(CLN 1.2.2 REQUIRED)
- libcvc4_link_libraries(${CLN_LIBRARIES})
- libcvc4_include_directories(${CLN_INCLUDE_DIR})
set(CVC4_USE_CLN_IMP 1)
set(CVC4_USE_GMP_IMP 0)
else()
endif()
set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
find_package(CryptoMiniSat REQUIRED)
- libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES})
- libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR})
add_definitions(-DCVC4_USE_CRYPTOMINISAT)
endif()
set(GPL_LIBS "${GPL_LIBS} glpk")
set(GLPK_HOME ${GLPK_DIR})
find_package(GLPK REQUIRED)
- libcvc4_link_libraries(${GLPK_LIBRARIES})
- libcvc4_include_directories(${GLPK_INCLUDE_DIR})
add_definitions(-DCVC4_USE_GLPK)
endif()
set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
set(LFSC_HOME ${LFSC_DIR})
find_package(LFSC REQUIRED)
- libcvc4_link_libraries(${LFSC_LIBRARIES})
- libcvc4_include_directories(${LFSC_INCLUDE_DIR})
add_definitions(-DCVC4_USE_LFSC)
endif()
if(USE_SYMFPU)
set(SymFPU_HOME ${SYMFPU_DIR})
find_package(SymFPU REQUIRED)
- libcvc4_include_directories(${SymFPU_INCLUDE_DIR})
add_definitions(-DCVC4_USE_SYMFPU)
set(CVC4_USE_SYMFPU 1)
else()
ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS)
mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS)
+if(ABC_LIBRARIES)
+ message(STATUS "Found ABC libs: ${ABC_LIBRARIES}")
+endif()
mark_as_advanced(ANTLR_BINARY ANTLR_INCLUDE_DIR ANTLR_LIBRARIES
HAVE_ANTLR3_FILE_STREAM_NEW)
+if(ANTLR_LIBRARIES)
+ message(STATUS "Found ANTLR libs: ${ANTLR_LIBRARIES}")
+endif()
VERSION_VAR CLN_VERSION)
mark_as_advanced(CLN_INCLUDE_DIR CLN_LIBRARIES)
endif()
+if(CLN_LIBRARIES)
+ message(STATUS "Found CLN libs: ${CLN_LIBRARIES}")
+endif()
CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES)
mark_as_advanced(CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES)
+if(CaDiCaL_LIBRARIES)
+ message(STATUS "Found CaDiCaL libs: ${CaDiCaL_LIBRARIES}")
+endif()
CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES)
mark_as_advanced(CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES)
+if(CryptoMiniSat_LIBRARIES)
+ message(STATUS "Found CryptoMiniSat libs: ${CryptoMiniSat_LIBRARIES}")
+endif()
GLPK_INCLUDE_DIR GLPK_LIBRARIES)
mark_as_advanced(GLPK_INCLUDE_DIR GLPK_LIBRARIES)
+if(GLPK_LIBRARIES)
+ message(STATUS "Found GLPK libs: ${GLPK_LIBRARIES}")
+endif()
find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIR GMP_LIBRARIES)
mark_as_advanced(GMP_INCLUDE_DIR GMP_LIBRARIES)
+if(GMP_LIBRARIES)
+ message(STATUS "Found GMP libs: ${GMP_LIBRARIES}")
+endif()
LFSC_INCLUDE_DIR LFSC_LIBRARIES)
mark_as_advanced(LFSC_INCLUDE_DIR LFSC_LIBRARIES)
+if(LFSC_LIBRARIES)
+ message(STATUS "Found LFSC libs: ${LFSC_LIBRARIES}")
+endif()
find_path(Readline_INCLUDE_DIR NAMES readline/readline.h)
find_library(Readline_LIBRARIES NAMES readline)
-# Check which standard of readline is installed on the system.
-# https://github.com/CVC4/CVC4/issues/702
+# Try to compile and link a simple program against readline. 'libs' can be
+# used to specify additional required libraries.
+function(try_compile_readline libs _result)
+ set(CMAKE_REQUIRED_QUIET TRUE)
+ set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES} ${libs})
+ check_cxx_source_compiles(
+ "
+ #include <stdio.h>
+ #include <readline/readline.h>
+ int main() { readline(\"\"); return 0; }
+ "
+ ${_result}
+ )
+ set(${_result} ${${_result}} PARENT_SCOPE)
+endfunction()
+
if(Readline_INCLUDE_DIR)
+ # We only need to figure out readline's additional libraries dependencies if
+ # we compile static.
+ # Note: It might be the case that we need to check for more/other libraries
+ # depending on what the installed version of readline is linked against
+ # (e.g., termcap, ncurses, ...).
+ find_library(TINFO_LIBRARY tinfo)
+ try_compile_readline(${TINFO_LIBRARY} OK)
+ if(OK)
+ list(APPEND Readline_LIBRARIES ${TINFO_LIBRARY})
+ else()
+ message(FATAL_ERROR
+ "Could not link against readline. "
+ "Check CMakeError.log for more details")
+ endif()
+
+ # Check which standard of readline is installed on the system.
+ # https://github.com/CVC4/CVC4/issues/702
include(CheckCXXSourceCompiles)
set(CMAKE_REQUIRED_QUIET TRUE)
- set(CMAKE_REQUIRED_LIBRARIES readline)
+ set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES})
check_cxx_source_compiles(
"#include <stdio.h>
#include <readline/readline.h>
Readline_LIBRARIES
Readline_COMPENTRY_FUNC_RETURNS_CHARPTR
)
+if(Readline_LIBRARIES)
+ message(STATUS "Found Readline libs: ${Readline_LIBRARIES}")
+endif()
endmacro()
-#-----------------------------------------------------------------------------#
-# libcvc4 helper macros
-
-# Collect all libraries that must be linked against libcvc4. These will be
-# actually linked in src/CMakeLists.txt with target_link_libaries(...).
-macro(libcvc4_link_libraries library)
- set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library})
-endmacro()
-
-# Collect all include directories that are required for libcvc4. These will be
-# actually included in src/CMakeLists.txt with target_include_directories(...).
-macro(libcvc4_include_directories dirs)
- set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs})
-endmacro()
-
# Collect all source files that are required to build libcvc4 in LIBCVC4_SRCS
# or LIBCVC4_GEN_SRCS. If GENERATED is the first argument the sources are
# added to LIBCVC4_GEN_SRCS. All sources are prepended with the absolute
add_subdirectory(base)
add_subdirectory(expr)
-add_subdirectory(main)
add_subdirectory(options)
add_subdirectory(parser)
add_subdirectory(theory)
set_source_files_properties(${LIBCVC4_GEN_SRCS} PROPERTIES GENERATED TRUE)
add_library(cvc4 ${LIBCVC4_SRCS} ${LIBCVC4_GEN_SRCS})
+install(TARGETS cvc4 DESTINATION lib)
set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC4_SOVERSION})
target_compile_definitions(cvc4
)
# Add libcvc4 dependencies for generated sources.
add_dependencies(cvc4 gen-expr gen-options gen-tags gen-theory)
-target_link_libraries(cvc4 ${LIBCVC4_LIBRARIES})
-target_include_directories(cvc4 PUBLIC ${LIBCVC4_INCLUDES})
-install(TARGETS cvc4 DESTINATION lib)
+# Add library/include dependencies
+if(ENABLE_VALGRIND)
+ target_include_directories(cvc4 PUBLIC ${Valgrind_INCLUDE_DIR})
+endif()
+if(USE_ABC)
+ target_link_libraries(cvc4 ${ABC_LIBRARIES})
+ target_include_directories(cvc4 PUBLIC ${ABC_INCLUDE_DIR})
+endif()
+if(USE_CADICAL)
+ target_link_libraries(cvc4 ${CaDiCaL_LIBRARIES})
+ target_include_directories(cvc4 PUBLIC ${CaDiCaL_INCLUDE_DIR})
+endif()
+if(USE_CLN)
+ target_link_libraries(cvc4 ${CLN_LIBRARIES})
+ target_include_directories(cvc4 PUBLIC ${CLN_INCLUDE_DIR})
+endif()
+if(USE_CRYPTOMINISAT)
+ target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
+ target_include_directories(cvc4 PUBLIC ${CryptoMiniSat_INCLUDE_DIR})
+endif()
+if(USE_GLPK)
+ target_link_libraries(cvc4 ${GLPK_LIBRARIES})
+ target_include_directories(cvc4 PUBLIC ${GLPK_INCLUDE_DIR})
+endif()
+if(USE_LFSC)
+ target_link_libraries(cvc4 ${LFSC_LIBRARIES})
+ target_include_directories(cvc4 PUBLIC ${LFSC_INCLUDE_DIR})
+endif()
+if(USE_SYMFPU)
+ target_include_directories(cvc4 PUBLIC ${SymFPU_INCLUDE_DIR})
+endif()
+
+# Note: When linked statically GMP needs to be linked after CLN since CLN
+# depends on GMP.
+target_link_libraries(cvc4 ${GMP_LIBRARIES})
+target_include_directories(cvc4 PUBLIC ${GMP_INCLUDE_DIR})
+
+#-----------------------------------------------------------------------------#
+# Visit main subdirectory after creating target cvc4. For target main, we have
+# to manually add library dependencies since we can't use
+# target_link_libraries(...) with object libraries for cmake versions <= 3.12.
+# Thus, we can only visit main as soon as all dependencies for cvc4 are set up.
+
+add_subdirectory(main)
+
+#-----------------------------------------------------------------------------#
# Note:
# We define all install commands for all public headers here in one
# place so that we can easily remove them as soon as we enforce the new
add_library(main OBJECT ${libmain_src_files})
target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER)
-if(BUILD_SHARED_LIBS)
- set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE 1)
+if(ENABLE_SHARED)
+ set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON)
endif()
# We can't use target_link_libraries(...) here since this is only supported for
# dependencies are not propagated and we need to manually add the include
# directories of libcvc4 to main.
add_dependencies(main cvc4 cvc4parser gen-tokens)
+get_target_property(LIBCVC4_INCLUDES cvc4 INCLUDE_DIRECTORIES)
target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES})
# main-test library is only used for linking against system and unit tests so
target_link_libraries(cvc4-bin cvc4 cvc4parser)
install(TARGETS cvc4-bin DESTINATION bin)
+# In order to get a fully static executable we have to make sure that we also
+# 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(NOT ENABLE_SHARED)
+ set_target_properties(cvc4-bin PROPERTIES LINK_FLAGS -static)
+ set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON)
+ set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
+endif()
+
if(ENABLE_PORTFOLIO)
set(pcvc4_src_files
main.cpp
target_link_libraries(pcvc4-bin cvc4 cvc4parser ${Boost_LIBRARIES})
target_include_directories(pcvc4-bin PRIVATE ${Boost_INCLUDE_DIRS})
install(TARGETS pcvc4-bin DESTINATION bin)
+
+ if(NOT ENABLE_SHARED)
+ set_target_properties(pcvc4-bin PROPERTIES LINK_FLAGS -static)
+ set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON)
+ set_target_properties(pcvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
+ endif()
endif()
if(USE_READLINE)
projects / cvc5.git / commitdiff