From: Mathias Preiner Date: Fri, 31 Aug 2018 16:11:23 +0000 (-0700) Subject: cmake: Use target specific includes for libcvc4. X-Git-Tag: cvc5-1.0.0~4578 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c255e8d8a39ca904ba6f99589fa06123c728d784;p=cvc5.git cmake: Use target specific includes for libcvc4. Further, print definitions added with add_definitions(...). --- diff --git a/CMakeLists.txt b/CMakeLists.txt index aa91a631f..47934d05f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -49,12 +49,20 @@ include(CheckCCompilerFlag) include(CheckCXXCompilerFlag) macro(add_c_flag flag) - set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}") + if(CMAKE_C_FLAGS) + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}") + else() + set(CMAKE_C_FLAGS "${flag}") + endif() message(STATUS "Configuring with C flag '${flag}'") endmacro() macro(add_cxx_flag flag) - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}") + if(CMAKE_CXX_FLAGS) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}") + else() + set(CMAKE_CXX_FLAGS "${flag}") + endif() message(STATUS "Configuring with CXX flag '${flag}'") endmacro() @@ -107,16 +115,31 @@ macro(add_required_c_cxx_flag flag) add_required_cxx_flag(${flag}) endmacro() -macro(cvc4_link_library library) - set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${library}) +# 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() +# CVC4 Boolean options are three-valued to detect if an option was set by the +# user. The available values are: IGNORE (default), ON, OFF +# Default options do not override options that were set by the user, i.e., +# cvc4_set_option only sets an option if it's value is still IGNORE. +# This e.g., allows the user to disable proofs for debug builds (where proofs +# are enabled by default). macro(cvc4_option var description) set(${var} IGNORE CACHE STRING "${description}") # Provide drop down menu options in cmake-gui set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF) endmacro() +# Only set option if the user did not set an option. macro(cvc4_set_option var value) if(${var} STREQUAL "IGNORE") set(${var} ${value}) @@ -263,8 +286,8 @@ find_package(ANTLR REQUIRED) set(GMP_HOME ${GMP_DIR}) find_package(GMP REQUIRED) -cvc4_link_library(${GMP_LIBRARIES}) -include_directories(${GMP_INCLUDE_DIR}) +libcvc4_link_libraries(${GMP_LIBRARIES}) +libcvc4_include_directories(${GMP_INCLUDE_DIR}) #-----------------------------------------------------------------------------# @@ -336,6 +359,7 @@ if(ENABLE_PROOFS) set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof) add_definitions(-DCVC4_PROOF) set(CVC4_PROOF 1) + libcvc4_link_libraries(signatures) endif() if(ENABLE_REPLAY) @@ -370,24 +394,24 @@ endif() if(USE_ABC) set(ABC_HOME "${ABC_DIR}") find_package(ABC REQUIRED) - cvc4_link_library(${ABC_LIBRARIES}) - include_directories(${ABC_INCLUDE_DIR}) + 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) - cvc4_link_library(${CaDiCaL_LIBRARIES}) - include_directories(${CaDiCaL_INCLUDE_DIR}) + 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) - cvc4_link_library(${CLN_LIBRARIES}) - include_directories(${CLN_INCLUDE_DIR}) + libcvc4_link_libraries(${CLN_LIBRARIES}) + libcvc4_include_directories(${CLN_INCLUDE_DIR}) set(CVC4_USE_CLN_IMP 1) set(CVC4_USE_GMP_IMP 0) else() @@ -404,8 +428,8 @@ if(USE_CRYPTOMINISAT) endif() set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR}) find_package(CryptoMiniSat REQUIRED) - cvc4_link_library(${CryptoMiniSat_LIBRARIES}) - include_directories(${CryptoMiniSat_INCLUDE_DIR}) + libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES}) + libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR}) add_definitions(-DCVC4_USE_CRYPTOMINISAT) endif() @@ -413,8 +437,8 @@ if(USE_GLPK) set(GPL_LIBS "${GPL_LIBS} glpk") set(GLPK_HOME ${GLPK_DIR}) find_package(GLPK REQUIRED) - cvc4_link_library(${GLPK_LIBRARIES}) - include_directories(${GLPK_INCLUDE_DIR}) + libcvc4_link_libraries(${GLPK_LIBRARIES}) + libcvc4_include_directories(${GLPK_INCLUDE_DIR}) add_definitions(-DCVC4_USE_GLPK) endif() @@ -422,7 +446,8 @@ if(USE_LFSC) set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc) set(LFSC_HOME ${LFSC_DIR}) find_package(LFSC REQUIRED) - include_directories(${LFSC_INCLUDE_DIR}) + libcvc4_link_libraries(${LFSC_LIBRARIES}) + libcvc4_include_directories(${LFSC_INCLUDE_DIR}) add_definitions(-DCVC4_USE_LFSC) set(CVC4_USE_LFSC 1) else() @@ -444,7 +469,7 @@ endif() if(USE_SYMFPU) set(SymFPU_HOME ${SYMFPU_DIR}) find_package(SymFPU REQUIRED) - include_directories(${SymFPU_INCLUDE_DIR}) + libcvc4_include_directories(${SymFPU_INCLUDE_DIR}) add_definitions(-DCVC4_USE_SYMFPU) set(CVC4_USE_SYMFPU 1) else() @@ -575,10 +600,10 @@ endif() if(ENABLE_PROOFS) add_subdirectory(proofs/signatures) - cvc4_link_library(signatures) endif() #-----------------------------------------------------------------------------# +# Print build configuration if(CVC4_BUILD_PROFILE_PRODUCTION) set(CVC4_BUILD_PROFILE_STRING "production") @@ -590,6 +615,10 @@ elseif(CVC4_BUILD_PROFILE_COMPETITION) set(CVC4_BUILD_PROFILE_STRING "competition") endif() +# Get all definitions added via add_definitions to print it below +get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS) +string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}") + message("CVC4 ${CVC4_RELEASE_STRING}") message("") message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") @@ -608,12 +637,7 @@ message("Unit tests : ${ENABLE_UNIT_TESTING}") message("Coverage (gcov) : ${ENABLE_COVERAGE}") message("Profiling (gprof) : ${ENABLE_PROFILING}") message("") -#message("Static libs : ${enable_static}") -if(BUILD_SHARED_LIBS) - message("Shared libs : ON") -else() - message("Shared libs : OFF") -endif() +message("Shared libs : ${ENABLE_SHARED}") #message("Static binary: ${enable_static_binary}") #message("Compat lib : ${CVC4_BUILD_LIBCOMPAT}") #message("Bindings : ${bindings_to_be_built}") @@ -626,11 +650,15 @@ message("CaDiCaL : ${USE_CADICAL}") message("CryptoMiniSat : ${USE_CRYPTOMINISAT}") message("GLPK : ${USE_GLPK}") message("LFSC : ${USE_LFSC}") -#message("MP library : ${mplibrary}") +if(CVC4_USE_CLN_IMP) + message("MP library : cln") +else() + message("MP library : gmp") +endif() message("Readline : ${USE_READLINE}") message("SymFPU : ${USE_SYMFPU}") message("") -#message("CPPFLAGS : ${CPPFLAGS}") +message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}") message("CXXFLAGS : ${CMAKE_CXX_FLAGS}") message("CFLAGS : ${CMAKE_C_FLAGS}") #message("LIBS : ${LIBS}") @@ -641,7 +669,7 @@ message("CFLAGS : ${CMAKE_C_FLAGS}") #message("libcvc4compat version : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}") #message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}") #message("") -#message("Install into : ${prefix}") +message("Install prefix : ${CMAKE_INSTALL_PREFIX}") message("") if(GPL_LIBS) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0a8db038f..22513d47e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -570,8 +570,9 @@ target_compile_definitions(cvc4 add_dependencies(cvc4 gen-theory-files) target_link_libraries(cvc4 base bvminisat expr minisat options smtutil util replacements - ${CVC4_LIBRARIES} + ${LIBCVC4_LIBRARIES} ) +target_include_directories(cvc4 PRIVATE ${LIBCVC4_INCLUDES}) include_directories(include) include_directories(. ${CMAKE_CURRENT_BINARY_DIR})