X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=CMakeLists.txt;h=ac654957ad86cdf83282e132cc98c54882f4a689;hb=51d731ec403becd8a46e02933112ff2fc6b310e9;hp=b0a8444919c09397e4c24f14c7080f4d78752bbc;hpb=c422f03d3169d4dc8d5b333de12be14e9121bc93;p=cvc5.git diff --git a/CMakeLists.txt b/CMakeLists.txt index b0a844491..ac654957a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -18,29 +18,14 @@ cmake_minimum_required(VERSION 3.9) #-----------------------------------------------------------------------------# # Project configuration -project(cvc4) +project(cvc5) +include(CheckIPOSupported) include(GNUInstallDirs) +set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) -set(CVC5_MAJOR 1) # Major component of the version of CVC4. -set(CVC5_MINOR 9) # Minor component of the version of CVC4. -set(CVC5_RELEASE 0) # Release component of the version of CVC4. - -# Extraversion component of the version of CVC4. -set(CVC5_EXTRAVERSION "-prerelease") - -# Shared library versioning. Increment SOVERSION for every new CVC4 release. -set(CVC5_SOVERSION 7) +include(version) -# Full release string for CVC4. -if(CVC5_RELEASE) - set(CVC5_RELEASE_STRING - "${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}${CVC5_EXTRAVERSION}") -else() - set(CVC5_RELEASE_STRING "${CVC5_MAJOR}.${CVC5_MINOR}${CVC5_EXTRAVERSION}") -endif() - -set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake) set(CMAKE_C_STANDARD 99) set(CMAKE_CXX_STANDARD 17) set(CMAKE_CXX_EXTENSIONS OFF) @@ -63,9 +48,6 @@ endif() #-----------------------------------------------------------------------------# # Tell CMake where to find our dependencies -if(ABC_DIR) - list(APPEND CMAKE_PREFIX_PATH "${ABC_DIR}") -endif() if(GLPK_DIR) list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}") endif() @@ -88,22 +70,21 @@ option(ENABLE_GPL "Enable GPL dependencies") # >> 3-valued: IGNORE ON OFF # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for build types -cvc4_option(ENABLE_ASAN "Enable ASAN build") -cvc4_option(ENABLE_UBSAN "Enable UBSan build") -cvc4_option(ENABLE_TSAN "Enable TSan build") -cvc4_option(ENABLE_ASSERTIONS "Enable assertions") -cvc4_option(ENABLE_COMP_INC_TRACK +option(BUILD_SHARED_LIBS "Build shared libraries and binary") +cvc5_option(ENABLE_ASAN "Enable ASAN build") +cvc5_option(ENABLE_UBSAN "Enable UBSan build") +cvc5_option(ENABLE_TSAN "Enable TSan build") +cvc5_option(ENABLE_ASSERTIONS "Enable assertions") +cvc5_option(ENABLE_COMP_INC_TRACK "Enable optimizations for incremental SMT-COMP tracks") -cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") -cvc4_option(ENABLE_DUMPING "Enable dumping") -cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output") -cvc4_option(ENABLE_STATISTICS "Enable statistics") -cvc4_option(ENABLE_TRACING "Enable tracing") -cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing") -cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation") -cvc4_option(ENABLE_SHARED "Build as shared library") -cvc4_option(ENABLE_STATIC_BINARY - "Build static binaries with statically linked system libraries") +cvc5_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") +cvc5_option(ENABLE_MUZZLE "Suppress ALL non-result output") +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_AUTO_DOWNLOAD "Enable automatic download of dependencies") +cvc5_option(ENABLE_IPO "Enable interprocedural optimization") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) option(ENABLE_BEST "Enable dependencies known to give best performance") @@ -116,17 +97,15 @@ option(ENABLE_PROFILING "Enable support for gprof profiling") # >> 3-valued: IGNORE ON OFF # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for ENABLE_BEST -cvc4_option(USE_ABC "Use ABC for AIG bit-blasting") -cvc4_option(USE_CADICAL "Use CaDiCaL SAT solver") -cvc4_option(USE_CLN "Use CLN instead of GMP") -cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") -cvc4_option(USE_GLPK "Use GLPK simplex solver") -cvc4_option(USE_KISSAT "Use Kissat SAT solver") -cvc4_option(USE_EDITLINE "Use Editline for better interactive support") +cvc5_option(USE_CLN "Use CLN instead of GMP") +cvc5_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver") +cvc5_option(USE_GLPK "Use GLPK simplex solver") +cvc5_option(USE_KISSAT "Use Kissat SAT solver") +cvc5_option(USE_EDITLINE "Use Editline for better interactive support") # >> 2-valued: ON OFF # > for options where we don't need to detect if set by user (default: OFF) option(USE_POLY "Use LibPoly for polynomial arithmetic") -option(USE_SYMFPU "Use SymFPU for floating point support") +option(USE_COCOA "Use CoCoALib for further polynomial operations") option(USE_PYTHON2 "Force Python 2 (deprecated)") # Custom install directories for dependencies @@ -134,7 +113,6 @@ option(USE_PYTHON2 "Force Python 2 (deprecated)") # installed via the corresponding contrib/get-* script and if not found, we # check the intalled system version. If the user provides a directory we # immediately fail if the dependency was not found at the specified location. -set(ABC_DIR "" CACHE STRING "Set ABC install directory") set(GLPK_DIR "" CACHE STRING "Set GLPK install directory") # Prepend binaries with prefix on make install @@ -144,11 +122,12 @@ set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install") option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ") option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ") -# Build limitations -option(BUILD_LIB_ONLY "Only build the library") - # Api documentation -cvc4_option(BUILD_DOCS "Build Api documentation") +option(BUILD_DOCS "Build Api documentation") + +# Link against static system libraries +cvc5_option(STATIC_BINARY "Link against static system libraries \ +(enabled by default for static builds)") #-----------------------------------------------------------------------------# # Internal cmake variables @@ -201,16 +180,21 @@ include(Config${CMAKE_BUILD_TYPE}) add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}") add_check_c_cxx_flag("-Wall") -add_check_c_cxx_flag("-Wno-unused-private-field") +add_check_c_cxx_supression_flag("-Wno-unused-private-field") add_check_c_flag("-fexceptions") add_check_cxx_flag("-Wsuggest-override") add_check_cxx_flag("-Wnon-virtual-dtor") add_check_c_cxx_flag("-Wimplicit-fallthrough") add_check_c_cxx_flag("-Wshadow") +# Assume no dynamic initialization of thread-local variables in non-defining +# translation units. This option should result in better performance and works +# around crashing issues with our Windows build. +add_check_cxx_flag("-fno-extern-tls-init") + # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment' # cdlist.h warnings. Remove when fixed. -add_check_cxx_flag("-Wno-class-memaccess") +add_check_cxx_supression_flag("-Wno-class-memaccess") if (WIN32) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000") @@ -230,15 +214,10 @@ if ("${LD_VERSION}" MATCHES "GNU gold") endif () #-----------------------------------------------------------------------------# -# Option defaults (three-valued options (cvc4_option(...))) -# -# These options are only set if their value is IGNORE. Otherwise, the user -# already set the option, which we don't want to overwrite. +# Use interprocedural optimization if requested -if(ENABLE_STATIC_BINARY) - cvc4_set_option(ENABLE_SHARED OFF) -else() - cvc4_set_option(ENABLE_SHARED ON) +if(ENABLE_IPO) + set(CMAKE_INTERPROCEDURAL_OPTIMIZATION TRUE) endif() #-----------------------------------------------------------------------------# @@ -246,66 +225,46 @@ endif() # Only enable unit testing if assertions are enabled. Otherwise, unit tests # that expect AssertionException to be thrown will fail. if(NOT ENABLE_ASSERTIONS) - message(WARNING "Disabling unit tests since assertions are disabled.") + message(STATUS "Disabling unit tests since assertions are disabled.") set(ENABLE_UNIT_TESTING OFF) 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(ENABLE_SHARED) - set(BUILD_SHARED_LIBS ON) - if(ENABLE_STATIC_BINARY) - set(ENABLE_STATIC_BINARY OFF) - message(WARNING "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() - # Embed the installation prefix as an RPATH in the executable such that the - # linker can find our libraries (such as libcvc4parser) when executing the - # cvc4 binary. This is for example useful when installing CVC4 with a custom - # prefix on macOS (e.g. when using homebrew in a non-standard directory). If - # we do not set this option, then the linker will not be able to find the - # required libraries when trying to run CVC4. - # - # Also embed the installation prefix of the installed contrib libraries as an - # RPATH. This allows to install a dynamically linked binary that depends on - # dynamically linked libraries. This is dangerous, as the installed binary - # breaks if the contrib library is removed or changes in other ways, we thus - # print a big warning and only allow if installing to a custom installation - # prefix. - # - # 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) - cvc4_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(WARNING "Disabling unit tests since static build is enabled.") - set(ENABLE_UNIT_TESTING OFF) - endif() - - if (BUILD_BINDINGS_PYTHON) - message(FATAL_ERROR "Building Python bindings is not possible " - "when building statically") +# 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 +# prefix on macOS (e.g. when using homebrew in a non-standard directory). If +# we do not set this option, then the linker will not be able to find the +# required libraries when trying to run cvc5. +# +# Also embed the installation prefix of the installed contrib libraries as an +# RPATH. This allows to install a dynamically linked binary that depends on +# dynamically linked libraries. This is dangerous, as the installed binary +# breaks if the contrib library is removed or changes in other ways, we thus +# print a big warning and only allow if installing to a custom installation +# prefix. +# +# 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") + +# Set visibility to default if unit tests are enabled. If unit tests are +# enabled, we also check if we can execute white box unit tests (some versions +# of Clang have issues with the required flag). +set(ENABLE_WHITEBOX_UNIT_TESTING OFF) +if(ENABLE_UNIT_TESTING) + set(CMAKE_CXX_VISIBILITY_PRESET default) + set(CMAKE_VISIBILITY_INLINES_HIDDEN 0) + + # Check if Clang version has the bug that was fixed in + # https://reviews.llvm.org/D93104 + set(ENABLE_WHITEBOX_UNIT_TESTING ON) + check_cxx_compiler_flag("-faccess-control" HAVE_CXX_FLAGfaccess_control) + if(NOT HAVE_CXX_FLAGfaccess_control) + set(ENABLE_WHITEBOX_UNIT_TESTING OFF) + message(STATUS "Disabling white box unit tests") endif() endif() @@ -319,6 +278,20 @@ enable_testing() #-----------------------------------------------------------------------------# # Check options, find packages and configure build. +if(BUILD_SHARED_LIBS) + if (WIN32) + set(CMAKE_FIND_LIBRARY_SUFFIXES .dll .lib .a) + else() + set(CMAKE_FIND_LIBRARY_SUFFIXES .so .dylib .a) + endif() +else() + if (WIN32) + set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a .dll) + else() + set(CMAKE_FIND_LIBRARY_SUFFIXES .a .so .dylib) + endif() +endif() + if(USE_PYTHON2) find_package(PythonInterp 2.7 REQUIRED) else() @@ -358,19 +331,14 @@ endif() if(ENABLE_COVERAGE) include(CodeCoverage) - APPEND_COVERAGE_COMPILER_FLAGS() + append_coverage_compiler_flags() add_definitions(-DCVC5_COVERAGE) - # Note: The ctest command returns a non-zero exit code if tests fail or run - # into a timeout. As a consequence, the coverage report is not generated. To - # prevent this we always return with exit code 0 after the ctest command has - # finished. - setup_target_for_coverage_gcovr_html( + setup_code_coverage_fastcov( NAME coverage - EXECUTABLE - ctest -j${CTEST_NTHREADS} -LE "example" - --output-on-failure $$ARGS || exit 0 - DEPENDS - build-tests) + PATH "${PROJECT_SOURCE_DIR}" + EXCLUDE "${CMAKE_BINARY_DIR}/deps/*" + DEPENDENCIES cvc5-bin + ) endif() if(ENABLE_DEBUG_CONTEXT_MM) @@ -389,10 +357,6 @@ if(ENABLE_MUZZLE) add_definitions(-DCVC5_MUZZLE) endif() -if(ENABLE_DUMPING) - add_definitions(-DCVC5_DUMPING) -endif() - if(ENABLE_PROFILING) add_definitions(-DCVC5_PROFILING) add_check_c_cxx_flag("-pg") @@ -411,15 +375,7 @@ if(ENABLE_VALGRIND) add_definitions(-DCVC5_VALGRIND) endif() -if(USE_ABC) - find_package(ABC REQUIRED) - add_definitions(-DCVC5_USE_ABC ${ABC_ARCH_FLAGS}) -endif() - -if(USE_CADICAL) - find_package(CaDiCaL REQUIRED) - add_definitions(-DCVC5_USE_CADICAL) -endif() +find_package(CaDiCaL REQUIRED) if(USE_CLN) set(GPL_LIBS "${GPL_LIBS} cln") @@ -438,7 +394,7 @@ if(USE_CRYPTOMINISAT) if(THREADS_HAVE_PTHREAD_ARG) add_c_cxx_flag(-pthread) endif() - find_package(CryptoMiniSat REQUIRED) + find_package(CryptoMiniSat 5.8 REQUIRED) add_definitions(-DCVC5_USE_CRYPTOMINISAT) endif() @@ -461,6 +417,11 @@ else() set(CVC5_USE_POLY_IMP 0) endif() +if(USE_COCOA) + find_package(CoCoA REQUIRED 0.99711) + add_definitions(-DCVC5_USE_COCOA) +endif() + if(USE_EDITLINE) find_package(Editline REQUIRED) set(HAVE_LIBEDITLINE 1) @@ -469,13 +430,7 @@ if(USE_EDITLINE) endif() endif() -if(USE_SYMFPU) - find_package(SymFPU REQUIRED) - add_definitions(-DCVC5_USE_SYMFPU) - set(CVC5_USE_SYMFPU 1) -else() - set(CVC5_USE_SYMFPU 0) -endif() +find_package(SymFPU REQUIRED) if(GPL_LIBS) if(NOT ENABLE_GPL) @@ -490,25 +445,29 @@ endif() # Provide targets to inspect iwyu suggestions include(IWYU) +include(fuzzing-murxla) #-----------------------------------------------------------------------------# -# Generate CVC4's cvc4autoconfig.h header -include(ConfigureCVC4) -if(NOT ENABLE_SHARED) +include(ConfigureCvc5) +if(BUILD_SHARED_LIBS) + set(CVC5_STATIC_BUILD OFF) +else() set(CVC5_STATIC_BUILD ON) + if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin") + cvc5_set_option(STATIC_BINARY ON) + endif() endif() -configure_file(cvc4autoconfig.h.in cvc4autoconfig.h) -unset(CVC5_STATIC_BUILD) -include_directories(${CMAKE_CURRENT_BINARY_DIR}) #-----------------------------------------------------------------------------# # Add subdirectories -add_subdirectory(doc) add_subdirectory(src) -add_subdirectory(test) +if(BUILD_BINDINGS_PYTHON AND NOT BUILD_SHARED_LIBS) + message(STATUS "Python bindings can only be built in a shared build.") + set(BUILD_BINDINGS_PYTHON OFF) +endif() if(BUILD_BINDINGS_PYTHON) set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR}) add_subdirectory(src/api/python) @@ -516,17 +475,20 @@ endif() if(BUILD_BINDINGS_JAVA) add_subdirectory(src/api/java) - message(WARNING "Java API is currently under development.") endif() if(BUILD_DOCS) add_subdirectory(docs) endif() +add_subdirectory(test) + +include(target-graphs) + #-----------------------------------------------------------------------------# # Package configuration # -# Export CVC4 targets to support find_package(CVC4) in other cmake projects. +# Export cvc5 targets to support find_package(cvc5) in other cmake projects. include(CMakePackageConfigHelpers) @@ -537,9 +499,9 @@ include(CMakePackageConfigHelpers) # (in the assumption that only reasonably experienced users use this and # also that custom installation prefixes are not used for longer periods of # time anyway). Also, we print a big warning with further instructions. -if(NOT ENABLE_STATIC_BINARY) - # Get the libraries that cvc4 links against - get_target_property(libs cvc4 INTERFACE_LINK_LIBRARIES) +if(BUILD_SHARED_LIBS) + # Get the libraries that cvc5 links against + get_target_property(libs cvc5 INTERFACE_LINK_LIBRARIES) set(LIBS_SHARED_FROM_DEPS "") foreach(lib ${libs}) # Filter out those that are linked dynamically and come from deps/install @@ -552,16 +514,16 @@ if(NOT ENABLE_STATIC_BINARY) if(list_len GREATER 0) # Print a generic warning install(CODE "message(WARNING \"You are installing a dynamically linked \ - binary of CVC4 which may be a problem if you are using any dynamically \ + binary of cvc5 which may be a problem if you are using any dynamically \ linked third-party library that you obtained through one of the \ contrib/get-xxx scripts. The binary uses the rpath mechanism to find these \ locally, hence executing such a contrib script removing the \ \\\"deps/install\\\" folder most probably breaks the installed binary! \ Consider installing the dynamically linked dependencies on your system \ - manually or link cvc4 statically.\")") + manually or link cvc5 statically.\")") # Print the libraries in question foreach(lib ${LIBS_SHARED_FROM_DEPS}) - install(CODE "message(WARNING \"The following library is used by the cvc4 binary: ${lib}\")") + install(CODE "message(WARNING \"The following library is used by the cvc5 binary: ${lib}\")") endforeach() # Check if we use a custom installation prefix if(CMAKE_INSTALL_PREFIX STREQUAL "/usr/local") @@ -576,28 +538,28 @@ if(NOT ENABLE_STATIC_BINARY) endif() endif() -install(EXPORT cvc4-targets - FILE CVC4Targets.cmake - NAMESPACE CVC4:: - DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4) +install(EXPORT cvc5-targets + FILE cvc5Targets.cmake + NAMESPACE cvc5:: + DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5) configure_package_config_file( - ${CMAKE_SOURCE_DIR}/cmake/CVC4Config.cmake.in - ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake - INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4 + ${CMAKE_SOURCE_DIR}/cmake/cvc5Config.cmake.in + ${CMAKE_BINARY_DIR}/cmake/cvc5Config.cmake + INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5 PATH_VARS CMAKE_INSTALL_LIBDIR ) write_basic_package_version_file( - ${CMAKE_CURRENT_BINARY_DIR}/CVC4ConfigVersion.cmake - VERSION ${CVC5_RELEASE_STRING} + ${CMAKE_CURRENT_BINARY_DIR}/cvc5ConfigVersion.cmake + VERSION ${CVC5_VERSION} COMPATIBILITY ExactVersion ) install(FILES - ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake - ${CMAKE_BINARY_DIR}/CVC4ConfigVersion.cmake - DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4 + ${CMAKE_BINARY_DIR}/cmake/cvc5Config.cmake + ${CMAKE_BINARY_DIR}/cvc5ConfigVersion.cmake + DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5 ) @@ -620,7 +582,7 @@ get_directory_property(CVC5_DEFINITIONS COMPILE_DEFINITIONS) string(REPLACE ";" " " CVC5_DEFINITIONS "${CVC5_DEFINITIONS}") message("") -print_info("CVC4 ${CVC5_RELEASE_STRING}") +print_info("cvc5 ${CVC5_VERSION}") message("") if(ENABLE_COMP_INC_TRACK) print_config("Build profile " "${CVC5_BUILD_PROFILE_STRING} (incremental)") @@ -635,7 +597,6 @@ print_config("Assertions " ${ENABLE_ASSERTIONS}) print_config("Debug symbols " ${ENABLE_DEBUG_SYMBOLS}) print_config("Debug context mem mgr " ${ENABLE_DEBUG_CONTEXT_MM}) message("") -print_config("Dumping " ${ENABLE_DUMPING}) print_config("Muzzle " ${ENABLE_MUZZLE}) print_config("Statistics " ${ENABLE_STATISTICS}) print_config("Tracing " ${ENABLE_TRACING}) @@ -648,34 +609,27 @@ 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 binary " ${ENABLE_STATIC_BINARY}) +print_config("Shared build " ${BUILD_SHARED_LIBS}) print_config("Python bindings " ${BUILD_BINDINGS_PYTHON}) print_config("Java bindings " ${BUILD_BINDINGS_JAVA}) print_config("Python2 " ${USE_PYTHON2}) +print_config("Interprocedural opt. " ${ENABLE_IPO}) message("") -print_config("ABC " ${USE_ABC}) -print_config("CaDiCaL " ${USE_CADICAL}) -print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT}) +print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT} FOUND_SYSTEM ${CryptoMiniSat_FOUND_SYSTEM}) print_config("GLPK " ${USE_GLPK}) -print_config("Kissat " ${USE_KISSAT}) -print_config("LibPoly " ${USE_POLY}) -message("") -print_config("Build libcvc4 only " ${BUILD_LIB_ONLY}) +print_config("Kissat " ${USE_KISSAT} FOUND_SYSTEM ${Kissat_FOUND_SYSTEM}) +print_config("LibPoly " ${USE_POLY} FOUND_SYSTEM ${Poly_FOUND_SYSTEM}) +print_config("CoCoALib " ${USE_COCOA} FOUND_SYSTEM ${CoCoA_FOUND_SYSTEM}) if(CVC5_USE_CLN_IMP) - print_config("MP library " "cln") + print_config("MP library " "cln" FOUND_SYSTEM ${CLN_FOUND_SYSTEM}) else() - print_config("MP library " "gmp") + print_config("MP library " "gmp" FOUND_SYSTEM ${GMP_FOUND_SYSTEM}) endif() print_config("Editline " ${USE_EDITLINE}) -print_config("SymFPU " ${USE_SYMFPU}) message("") print_config("Api docs " ${BUILD_DOCS}) message("") -if(ABC_DIR) - print_config("ABC dir " ${ABC_DIR}) -endif() if(GLPK_DIR) print_config("GLPK dir " ${GLPK_DIR}) endif() @@ -690,34 +644,34 @@ message("") if(GPL_LIBS) message( - "${Blue}CVC4 license: " + "${Blue}cvc5 license: " "${Yellow}GPLv3 (due to optional libraries; see below)${ResetColor}" "\n" "\n" - "Please note that CVC4 will be built against the following GPLed libraries:" + "Please note that cvc5 will be built against the following GPLed libraries:" "\n" "${GPL_LIBS}" "\n" - "As these libraries are covered under the GPLv3, so is this build of CVC4." + "As these libraries are covered under the GPLv3, so is this build of cvc5." "\n" - "CVC4 is also available to you under the terms of the (modified) BSD license." + "cvc5 is also available to you under the terms of the (modified) BSD license." "\n" - "If you prefer to license CVC4 under those terms, please configure CVC4 to" + "If you prefer to license cvc5 under those terms, please configure cvc5 to" "\n" "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)." ) else() message( - "${Blue}CVC4 license:${ResetColor} modified BSD" + "${Blue}cvc5 license:${ResetColor} modified BSD" "\n" "\n" "Note that this configuration is NOT built against any GPL'ed libraries, so" "\n" - "it is covered by the (modified) BSD license. This is, however, not the best" + "it is covered by the (modified) BSD license. To build against GPL'ed" "\n" - "performing configuration of CVC4. To build against GPL'ed libraries which" + "libraries which can improve cvc5's performance on arithmetic and bitvector" "\n" - "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'." + "logics, re-configure with '-DENABLE_GPL -DENABLE_BEST'." ) endif()