CMakeLists.txt

   1 ###############################################################################
   2 # Top contributors (to current version):
   3 #   Aina Niemetz, Mathias Preiner, Gereon Kremer
   4 #
   5 # This file is part of the cvc5 project.
   6 #
   7 # Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8 # in the top-level source directory and their institutional affiliations.
   9 # All rights reserved.  See the file COPYING in the top-level source
  10 # directory for licensing information.
  11 # #############################################################################
  12 #
  13 # The build system configuration.
  14 ##
  15
  16 cmake_minimum_required(VERSION 3.9)
  17
  18 #-----------------------------------------------------------------------------#
  19 # Project configuration
  20
  21 project(cvc5)
  22
  23 include(CheckIPOSupported)
  24 include(GNUInstallDirs)
  25 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
  26
  27 include(version)
  28
  29 set(CMAKE_C_STANDARD 99)
  30 set(CMAKE_CXX_STANDARD 17)
  31 set(CMAKE_CXX_EXTENSIONS OFF)
  32 set(CMAKE_CXX_STANDARD_REQUIRED ON)
  33 set(CMAKE_CXX_VISIBILITY_PRESET hidden)
  34 set(CMAKE_VISIBILITY_INLINES_HIDDEN 1)
  35
  36 # Generate compile_commands.json, which can be used for various code completion
  37 # plugins.
  38 set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
  39
  40 #-----------------------------------------------------------------------------#
  41 # Policies
  42
  43 # Required for FindGLPK since it sets CMAKE_REQUIRED_LIBRARIES
  44 if(POLICY CMP0075)
  45   cmake_policy(SET CMP0075 NEW)
  46 endif()
  47
  48 #-----------------------------------------------------------------------------#
  49 # Tell CMake where to find our dependencies
  50
  51 if(GLPK_DIR)
  52   list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}")
  53 endif()
  54
  55 # By default the contrib/get-* scripts install dependencies to deps/install.
  56 list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps/install")
  57
  58 #-----------------------------------------------------------------------------#
  59
  60 include(Helpers)
  61
  62 #-----------------------------------------------------------------------------#
  63 # User options
  64
  65 # License
  66 option(ENABLE_GPL "Enable GPL dependencies")
  67
  68 # General build options
  69 #
  70 # >> 3-valued: IGNORE ON OFF
  71 #    > allows to detect if set by user (default: IGNORE)
  72 #    > only necessary for options set for build types
  73 option(BUILD_SHARED_LIBS          "Build shared libraries and binary")
  74 cvc5_option(ENABLE_ASAN           "Enable ASAN build")
  75 cvc5_option(ENABLE_UBSAN          "Enable UBSan build")
  76 cvc5_option(ENABLE_TSAN           "Enable TSan build")
  77 cvc5_option(ENABLE_ASSERTIONS     "Enable assertions")
  78 cvc5_option(ENABLE_COMP_INC_TRACK
  79             "Enable optimizations for incremental SMT-COMP tracks")
  80 cvc5_option(ENABLE_DEBUG_SYMBOLS  "Enable debug symbols")
  81 cvc5_option(ENABLE_MUZZLE         "Suppress ALL non-result output")
  82 cvc5_option(ENABLE_STATISTICS     "Enable statistics")
  83 cvc5_option(ENABLE_TRACING        "Enable tracing")
  84 cvc5_option(ENABLE_UNIT_TESTING   "Enable unit testing")
  85 cvc5_option(ENABLE_VALGRIND       "Enable valgrind instrumentation")
  86 cvc5_option(ENABLE_AUTO_DOWNLOAD  "Enable automatic download of dependencies")
  87 cvc5_option(ENABLE_IPO            "Enable interprocedural optimization")
  88 # >> 2-valued: ON OFF
  89 #    > for options where we don't need to detect if set by user (default: OFF)
  90 option(ENABLE_BEST             "Enable dependencies known to give best performance")
  91 option(ENABLE_COVERAGE         "Enable support for gcov coverage testing")
  92 option(ENABLE_DEBUG_CONTEXT_MM "Enable the debug context memory manager")
  93 option(ENABLE_PROFILING        "Enable support for gprof profiling")
  94
  95 # Optional dependencies
  96 #
  97 # >> 3-valued: IGNORE ON OFF
  98 #    > allows to detect if set by user (default: IGNORE)
  99 #    > only necessary for options set for ENABLE_BEST
 100 cvc5_option(USE_CLN           "Use CLN instead of GMP")
 101 cvc5_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
 102 cvc5_option(USE_GLPK          "Use GLPK simplex solver")
 103 cvc5_option(USE_KISSAT        "Use Kissat SAT solver")
 104 cvc5_option(USE_EDITLINE      "Use Editline for better interactive support")
 105 # >> 2-valued: ON OFF
 106 #    > for options where we don't need to detect if set by user (default: OFF)
 107 option(USE_POLY               "Use LibPoly for polynomial arithmetic")
 108 option(USE_COCOA              "Use CoCoALib for further polynomial operations")
 109 option(USE_PYTHON2            "Force Python 2 (deprecated)")
 110
 111 # Custom install directories for dependencies
 112 # If no directory is provided by the user, we first check if the dependency was
 113 # installed via the corresponding contrib/get-* script and if not found, we
 114 # check the intalled system version. If the user provides a directory we
 115 # immediately fail if the dependency was not found at the specified location.
 116 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 117
 118 # Prepend binaries with prefix on make install
 119 set(PROGRAM_PREFIX    "" CACHE STRING "Program prefix on make install")
 120
 121 # Supported language bindings based on new C++ API
 122 option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ")
 123 option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ")
 124
 125 # Api documentation
 126 option(BUILD_DOCS "Build Api documentation")
 127
 128 # Link against static system libraries
 129 cvc5_option(STATIC_BINARY "Link against static system libraries \
 130 (enabled by default for static builds)")
 131
 132 #-----------------------------------------------------------------------------#
 133 # Internal cmake variables
 134
 135 set(OPTIMIZATION_LEVEL 3)
 136 set(GPL_LIBS "")
 137
 138 #-----------------------------------------------------------------------------#
 139 # Determine number of threads available, used to configure (default) parallel
 140 # execution of custom test targets (can be overriden with ARGS=-jN).
 141
 142 include(ProcessorCount)
 143 ProcessorCount(CTEST_NTHREADS)
 144 if(CTEST_NTHREADS EQUAL 0)
 145   set(CTEST_NTHREADS 1)
 146 endif()
 147
 148 #-----------------------------------------------------------------------------#
 149 # Build types
 150
 151 # Note: Module CodeCoverage requires the name of the debug build to conform
 152 #       to cmake standards (first letter uppercase).
 153 set(BUILD_TYPES Production Debug Testing Competition)
 154
 155 if(ENABLE_ASAN OR ENABLE_UBSAN OR ENABLE_TSAN)
 156   set(CMAKE_BUILD_TYPE Debug)
 157 endif()
 158
 159 # Set the default build type to Production
 160 if(NOT CMAKE_BUILD_TYPE)
 161   set(CMAKE_BUILD_TYPE
 162       Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
 163   # Provide drop down menu options in cmake-gui
 164   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 165 endif()
 166
 167 # Check if specified build type is valid.
 168 list(FIND BUILD_TYPES ${CMAKE_BUILD_TYPE} FOUND_BUILD_TYPE)
 169 if(${FOUND_BUILD_TYPE} EQUAL -1)
 170   message(FATAL_ERROR
 171     "'${CMAKE_BUILD_TYPE}' is not a valid build type. "
 172     "Available builds are: ${BUILD_TYPES}")
 173 endif()
 174
 175 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 176 include(Config${CMAKE_BUILD_TYPE})
 177
 178 #-----------------------------------------------------------------------------#
 179 # Compiler flags
 180
 181 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
 182 add_check_c_cxx_flag("-Wall")
 183 add_check_c_cxx_supression_flag("-Wno-unused-private-field")
 184 add_check_c_flag("-fexceptions")
 185 add_check_cxx_flag("-Wsuggest-override")
 186 add_check_cxx_flag("-Wnon-virtual-dtor")
 187 add_check_c_cxx_flag("-Wimplicit-fallthrough")
 188 add_check_c_cxx_flag("-Wshadow")
 189
 190 # Assume no dynamic initialization of thread-local variables in non-defining
 191 # translation units. This option should result in better performance and works
 192 # around crashing issues with our Windows build.
 193 add_check_cxx_flag("-fno-extern-tls-init")
 194
 195 # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
 196 # cdlist.h warnings. Remove when fixed.
 197 add_check_cxx_supression_flag("-Wno-class-memaccess")
 198
 199 if (WIN32)
 200   set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000")
 201 endif ()
 202
 203 #-----------------------------------------------------------------------------#
 204 # Use ld.gold if available
 205
 206 execute_process(COMMAND ${CMAKE_C_COMPILER}
 207                 -fuse-ld=gold
 208                 -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION)
 209 if ("${LD_VERSION}" MATCHES "GNU gold")
 210   string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold")
 211   string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold")
 212   string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold")
 213   message(STATUS "Using GNU gold linker.")
 214 endif ()
 215
 216 #-----------------------------------------------------------------------------#
 217 # Use interprocedural optimization if requested
 218
 219 if(ENABLE_IPO)
 220   set(CMAKE_INTERPROCEDURAL_OPTIMIZATION TRUE)
 221 endif()
 222
 223 #-----------------------------------------------------------------------------#
 224
 225 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
 226 # that expect AssertionException to be thrown will fail.
 227 if(NOT ENABLE_ASSERTIONS)
 228   message(STATUS "Disabling unit tests since assertions are disabled.")
 229   set(ENABLE_UNIT_TESTING OFF)
 230 endif()
 231
 232 #-----------------------------------------------------------------------------#
 233 # Shared/static libraries
 234
 235 # Embed the installation prefix as an RPATH in the executable such that the
 236 # linker can find our libraries (such as libcvc5parser) when executing the
 237 # cvc5 binary. This is for example useful when installing cvc5 with a custom
 238 # prefix on macOS (e.g. when using homebrew in a non-standard directory). If
 239 # we do not set this option, then the linker will not be able to find the
 240 # required libraries when trying to run cvc5.
 241 #
 242 # Also embed the installation prefix of the installed contrib libraries as an
 243 # RPATH. This allows to install a dynamically linked binary that depends on
 244 # dynamically linked libraries. This is dangerous, as the installed binary
 245 # breaks if the contrib library is removed or changes in other ways, we thus
 246 # print a big warning and only allow if installing to a custom installation
 247 # prefix.
 248 #
 249 # More information on RPATH in CMake:
 250 # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
 251 set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
 252
 253 # Set visibility to default if unit tests are enabled. If unit tests are
 254 # enabled, we also check if we can execute white box unit tests (some versions
 255 # of Clang have issues with the required flag).
 256 set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
 257 if(ENABLE_UNIT_TESTING)
 258   set(CMAKE_CXX_VISIBILITY_PRESET default)
 259   set(CMAKE_VISIBILITY_INLINES_HIDDEN 0)
 260
 261   # Check if Clang version has the bug that was fixed in
 262   # https://reviews.llvm.org/D93104
 263   set(ENABLE_WHITEBOX_UNIT_TESTING ON)
 264   check_cxx_compiler_flag("-faccess-control" HAVE_CXX_FLAGfaccess_control)
 265   if(NOT HAVE_CXX_FLAGfaccess_control)
 266     set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
 267     message(STATUS "Disabling white box unit tests")
 268   endif()
 269 endif()
 270
 271 #-----------------------------------------------------------------------------#
 272 # Enable the ctest testing framework
 273
 274 # This needs to be enabled here rather than in subdirectory test in order to
 275 # allow calling ctest from the root build directory.
 276 enable_testing()
 277
 278 #-----------------------------------------------------------------------------#
 279 # Check options, find packages and configure build.
 280
 281 if(BUILD_SHARED_LIBS)
 282   if (WIN32)
 283     set(CMAKE_FIND_LIBRARY_SUFFIXES .dll .lib .a)
 284   else()
 285     set(CMAKE_FIND_LIBRARY_SUFFIXES .so .dylib .a)
 286   endif()
 287 else()
 288   if (WIN32)
 289     set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a .dll)
 290   else()
 291     set(CMAKE_FIND_LIBRARY_SUFFIXES .a .so .dylib)
 292   endif()
 293 endif()
 294
 295 if(USE_PYTHON2)
 296   find_package(PythonInterp 2.7 REQUIRED)
 297 else()
 298   find_package(PythonInterp 3 REQUIRED)
 299 endif()
 300
 301 find_package(GMP 6.1 REQUIRED)
 302
 303 if(ENABLE_ASAN)
 304   # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
 305   # otherwise the -fsanitize=address check will fail while linking.
 306   set(CMAKE_REQUIRED_FLAGS -fsanitize=address)
 307   add_required_c_cxx_flag("-fsanitize=address")
 308   unset(CMAKE_REQUIRED_FLAGS)
 309   add_required_c_cxx_flag("-fno-omit-frame-pointer")
 310   add_check_c_cxx_flag("-fsanitize-recover=address")
 311 endif()
 312
 313 if(ENABLE_UBSAN)
 314   add_required_c_cxx_flag("-fsanitize=undefined")
 315   add_definitions(-DCVC5_USE_UBSAN)
 316 endif()
 317
 318 if(ENABLE_TSAN)
 319   # -fsanitize=thread requires CMAKE_REQUIRED_FLAGS to be explicitely set,
 320   # otherwise the -fsanitize=thread check will fail while linking.
 321   set(CMAKE_REQUIRED_FLAGS -fsanitize=thread)
 322   add_required_c_cxx_flag("-fsanitize=thread")
 323   unset(CMAKE_REQUIRED_FLAGS)
 324 endif()
 325
 326 if(ENABLE_ASSERTIONS)
 327   add_definitions(-DCVC5_ASSERTIONS)
 328 else()
 329   add_definitions(-DNDEBUG)
 330 endif()
 331
 332 if(ENABLE_COVERAGE)
 333   include(CodeCoverage)
 334   append_coverage_compiler_flags()
 335   add_definitions(-DCVC5_COVERAGE)
 336   setup_code_coverage_fastcov(
 337     NAME coverage
 338     PATH "${PROJECT_SOURCE_DIR}"
 339     EXCLUDE "${CMAKE_BINARY_DIR}/deps/*"
 340     DEPENDENCIES cvc5-bin
 341   )
 342 endif()
 343
 344 if(ENABLE_DEBUG_CONTEXT_MM)
 345   add_definitions(-DCVC5_DEBUG_CONTEXT_MEMORY_MANAGER)
 346 endif()
 347
 348 if(ENABLE_DEBUG_SYMBOLS)
 349   add_check_c_cxx_flag("-ggdb3")
 350 endif()
 351
 352 if(ENABLE_COMP_INC_TRACK)
 353   add_definitions(-DCVC5_SMTCOMP_APPLICATION_TRACK)
 354 endif()
 355
 356 if(ENABLE_MUZZLE)
 357   add_definitions(-DCVC5_MUZZLE)
 358 endif()
 359
 360 if(ENABLE_PROFILING)
 361   add_definitions(-DCVC5_PROFILING)
 362   add_check_c_cxx_flag("-pg")
 363 endif()
 364
 365 if(ENABLE_TRACING)
 366   add_definitions(-DCVC5_TRACING)
 367 endif()
 368
 369 if(ENABLE_STATISTICS)
 370   add_definitions(-DCVC5_STATISTICS_ON)
 371 endif()
 372
 373 if(ENABLE_VALGRIND)
 374   find_package(Valgrind REQUIRED)
 375   add_definitions(-DCVC5_VALGRIND)
 376 endif()
 377
 378 find_package(CaDiCaL REQUIRED)
 379
 380 if(USE_CLN)
 381   set(GPL_LIBS "${GPL_LIBS} cln")
 382   find_package(CLN 1.2.2 REQUIRED)
 383   set(CVC5_USE_CLN_IMP 1)
 384   set(CVC5_USE_GMP_IMP 0)
 385 else()
 386   set(CVC5_USE_CLN_IMP 0)
 387   set(CVC5_USE_GMP_IMP 1)
 388 endif()
 389
 390 if(USE_CRYPTOMINISAT)
 391   # CryptoMiniSat requires pthreads support
 392   set(THREADS_PREFER_PTHREAD_FLAG ON)
 393   find_package(Threads REQUIRED)
 394   if(THREADS_HAVE_PTHREAD_ARG)
 395     add_c_cxx_flag(-pthread)
 396   endif()
 397   find_package(CryptoMiniSat 5.8 REQUIRED)
 398   add_definitions(-DCVC5_USE_CRYPTOMINISAT)
 399 endif()
 400
 401 if(USE_GLPK)
 402   set(GPL_LIBS "${GPL_LIBS} glpk")
 403   find_package(GLPK REQUIRED)
 404   add_definitions(-DCVC5_USE_GLPK)
 405 endif()
 406
 407 if(USE_KISSAT)
 408   find_package(Kissat REQUIRED)
 409   add_definitions(-DCVC5_USE_KISSAT)
 410 endif()
 411
 412 if(USE_POLY)
 413   find_package(Poly REQUIRED)
 414   add_definitions(-DCVC5_USE_POLY)
 415   set(CVC5_USE_POLY_IMP 1)
 416 else()
 417   set(CVC5_USE_POLY_IMP 0)
 418 endif()
 419
 420 if(USE_COCOA)
 421   find_package(CoCoA REQUIRED 0.99711)
 422   add_definitions(-DCVC5_USE_COCOA)
 423 endif()
 424
 425 if(USE_EDITLINE)
 426   find_package(Editline REQUIRED)
 427   set(HAVE_LIBEDITLINE 1)
 428   if(Editline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 429     set(EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 430   endif()
 431 endif()
 432
 433 find_package(SymFPU REQUIRED)
 434
 435 if(GPL_LIBS)
 436   if(NOT ENABLE_GPL)
 437     message(FATAL_ERROR
 438       "Bad configuration detected: BSD-licensed code only, but also requested "
 439       "GPLed libraries: ${GPL_LIBS}")
 440   endif()
 441   set(CVC5_GPL_DEPS 1)
 442 endif()
 443
 444 #-----------------------------------------------------------------------------#
 445 # Provide targets to inspect iwyu suggestions
 446
 447 include(IWYU)
 448 include(fuzzing-murxla)
 449
 450 #-----------------------------------------------------------------------------#
 451
 452 include(ConfigureCvc5)
 453 if(BUILD_SHARED_LIBS)
 454   set(CVC5_STATIC_BUILD OFF)
 455 else()
 456   set(CVC5_STATIC_BUILD ON)
 457   if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin")
 458     cvc5_set_option(STATIC_BINARY ON)
 459   endif()
 460 endif()
 461
 462 #-----------------------------------------------------------------------------#
 463 # Add subdirectories
 464
 465 add_subdirectory(src)
 466
 467 if(BUILD_BINDINGS_PYTHON AND NOT BUILD_SHARED_LIBS)
 468   message(STATUS "Python bindings can only be built in a shared build.")
 469   set(BUILD_BINDINGS_PYTHON OFF)
 470 endif()
 471 if(BUILD_BINDINGS_PYTHON)
 472   set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR})
 473   add_subdirectory(src/api/python)
 474 endif()
 475
 476 if(BUILD_BINDINGS_JAVA)
 477   add_subdirectory(src/api/java)
 478 endif()
 479
 480 if(BUILD_DOCS)
 481   add_subdirectory(docs)
 482 endif()
 483
 484 add_subdirectory(test)
 485
 486 include(target-graphs)
 487
 488 #-----------------------------------------------------------------------------#
 489 # Package configuration
 490 #
 491 # Export cvc5 targets to support find_package(cvc5) in other cmake projects.
 492
 493 include(CMakePackageConfigHelpers)
 494
 495 # If we install a dynamically linked binary that also uses dynamically used
 496 # libraries from deps/install/lib, we need to be cautious. Changing these
 497 # shared libraries from deps/install/lib most probably breaks the binary.
 498 # We only allow such an installation for custom installation prefixes
 499 # (in the assumption that only reasonably experienced users use this and
 500 # also that custom installation prefixes are not used for longer periods of
 501 # time anyway). Also, we print a big warning with further instructions.
 502 if(BUILD_SHARED_LIBS)
 503   # Get the libraries that cvc5 links against
 504   get_target_property(libs cvc5 INTERFACE_LINK_LIBRARIES)
 505   set(LIBS_SHARED_FROM_DEPS "")
 506   foreach(lib ${libs})
 507     # Filter out those that are linked dynamically and come from deps/install
 508     if(lib MATCHES ".*/deps/install/lib/.*\.so")
 509       list(APPEND LIBS_SHARED_FROM_DEPS ${lib})
 510     endif()
 511   endforeach()
 512   list(LENGTH LIBS_SHARED_FROM_DEPS list_len)
 513   # Check if we actually use such "dangerous" libraries
 514   if(list_len GREATER 0)
 515     # Print a generic warning
 516     install(CODE "message(WARNING \"You are installing a dynamically linked \
 517     binary of cvc5 which may be a problem if you are using any dynamically \
 518     linked third-party library that you obtained through one of the \
 519     contrib/get-xxx scripts. The binary uses the rpath mechanism to find these \
 520     locally, hence executing such a contrib script removing the \
 521     \\\"deps/install\\\" folder most probably breaks the installed binary! \
 522     Consider installing the dynamically linked dependencies on your system \
 523     manually or link cvc5 statically.\")")
 524     # Print the libraries in question
 525     foreach(lib ${LIBS_SHARED_FROM_DEPS})
 526       install(CODE "message(WARNING \"The following library is used by the cvc5 binary: ${lib}\")")
 527     endforeach()
 528     # Check if we use a custom installation prefix
 529     if(CMAKE_INSTALL_PREFIX STREQUAL "/usr/local")
 530       install(CODE "message(FATAL_ERROR \"To avoid installing a \
 531       soon-to-be-broken binary, system-wide installation is disabled if the \
 532       binary depends on locally-built shared libraries.\")")
 533     else()
 534       install(CODE "message(WARNING \"You have selected a custom install \
 535       directory ${CMAKE_INSTALL_PREFIX}, so we expect you understood the \
 536       previous warning and know what you are doing.\")")
 537     endif()
 538   endif()
 539 endif()
 540
 541 install(EXPORT cvc5-targets
 542   FILE cvc5Targets.cmake
 543   NAMESPACE cvc5::
 544   DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5)
 545
 546 configure_package_config_file(
 547   ${CMAKE_SOURCE_DIR}/cmake/cvc5Config.cmake.in
 548   ${CMAKE_BINARY_DIR}/cmake/cvc5Config.cmake
 549   INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5
 550   PATH_VARS CMAKE_INSTALL_LIBDIR
 551 )
 552
 553 write_basic_package_version_file(
 554   ${CMAKE_CURRENT_BINARY_DIR}/cvc5ConfigVersion.cmake
 555   VERSION ${CVC5_VERSION}
 556   COMPATIBILITY ExactVersion
 557 )
 558
 559 install(FILES
 560   ${CMAKE_BINARY_DIR}/cmake/cvc5Config.cmake
 561   ${CMAKE_BINARY_DIR}/cvc5ConfigVersion.cmake
 562   DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5
 563 )
 564
 565
 566 #-----------------------------------------------------------------------------#
 567 # Print build configuration
 568
 569 # Set colors.
 570 if(NOT WIN32)
 571   string(ASCII 27 Esc)
 572   set(Green "${Esc}[32m")
 573   set(Blue "${Esc}[1;34m")
 574   set(ResetColor "${Esc}[m")
 575 endif()
 576
 577 # Convert build type to lower case.
 578 string(TOLOWER ${CMAKE_BUILD_TYPE} CVC5_BUILD_PROFILE_STRING)
 579
 580 # Get all definitions added via add_definitions.
 581 get_directory_property(CVC5_DEFINITIONS COMPILE_DEFINITIONS)
 582 string(REPLACE ";" " " CVC5_DEFINITIONS "${CVC5_DEFINITIONS}")
 583
 584 message("")
 585 print_info("cvc5 ${CVC5_VERSION}")
 586 message("")
 587 if(ENABLE_COMP_INC_TRACK)
 588   print_config("Build profile             " "${CVC5_BUILD_PROFILE_STRING} (incremental)")
 589 else()
 590   print_config("Build profile             " "${CVC5_BUILD_PROFILE_STRING}")
 591 endif()
 592 message("")
 593 print_config("GPL                       " ${ENABLE_GPL})
 594 print_config("Best configuration        " ${ENABLE_BEST})
 595 message("")
 596 print_config("Assertions                " ${ENABLE_ASSERTIONS})
 597 print_config("Debug symbols             " ${ENABLE_DEBUG_SYMBOLS})
 598 print_config("Debug context mem mgr     " ${ENABLE_DEBUG_CONTEXT_MM})
 599 message("")
 600 print_config("Muzzle                    " ${ENABLE_MUZZLE})
 601 print_config("Statistics                " ${ENABLE_STATISTICS})
 602 print_config("Tracing                   " ${ENABLE_TRACING})
 603 message("")
 604 print_config("ASan                      " ${ENABLE_ASAN})
 605 print_config("UBSan                     " ${ENABLE_UBSAN})
 606 print_config("TSan                      " ${ENABLE_TSAN})
 607 print_config("Coverage (gcov)           " ${ENABLE_COVERAGE})
 608 print_config("Profiling (gprof)         " ${ENABLE_PROFILING})
 609 print_config("Unit tests                " ${ENABLE_UNIT_TESTING})
 610 print_config("Valgrind                  " ${ENABLE_VALGRIND})
 611 message("")
 612 print_config("Shared build              " ${BUILD_SHARED_LIBS})
 613 print_config("Python bindings           " ${BUILD_BINDINGS_PYTHON})
 614 print_config("Java bindings             " ${BUILD_BINDINGS_JAVA})
 615 print_config("Python2                   " ${USE_PYTHON2})
 616 print_config("Interprocedural opt.      " ${ENABLE_IPO})
 617 message("")
 618 print_config("CryptoMiniSat             " ${USE_CRYPTOMINISAT} FOUND_SYSTEM ${CryptoMiniSat_FOUND_SYSTEM})
 619 print_config("GLPK                      " ${USE_GLPK})
 620 print_config("Kissat                    " ${USE_KISSAT} FOUND_SYSTEM ${Kissat_FOUND_SYSTEM})
 621 print_config("LibPoly                   " ${USE_POLY} FOUND_SYSTEM ${Poly_FOUND_SYSTEM})
 622 print_config("CoCoALib                  " ${USE_COCOA} FOUND_SYSTEM ${CoCoA_FOUND_SYSTEM})
 623
 624 if(CVC5_USE_CLN_IMP)
 625   print_config("MP library                " "cln" FOUND_SYSTEM ${CLN_FOUND_SYSTEM})
 626 else()
 627   print_config("MP library                " "gmp" FOUND_SYSTEM ${GMP_FOUND_SYSTEM})
 628 endif()
 629 print_config("Editline                  " ${USE_EDITLINE})
 630 message("")
 631 print_config("Api docs                  " ${BUILD_DOCS})
 632 message("")
 633 if(GLPK_DIR)
 634   print_config("GLPK dir                  " ${GLPK_DIR})
 635 endif()
 636 message("")
 637 print_config("CPPLAGS (-D...)" "${CVC5_DEFINITIONS}")
 638 print_config("CXXFLAGS       " "${CMAKE_CXX_FLAGS}")
 639 print_config("CFLAGS         " "${CMAKE_C_FLAGS}")
 640 print_config("Linker flags   " "${CMAKE_EXE_LINKER_FLAGS}")
 641 message("")
 642 print_config("Install prefix " "${CMAKE_INSTALL_PREFIX}")
 643 message("")
 644
 645 if(GPL_LIBS)
 646   message(
 647   "${Blue}cvc5 license: "
 648   "${Yellow}GPLv3 (due to optional libraries; see below)${ResetColor}"
 649   "\n"
 650   "\n"
 651   "Please note that cvc5 will be built against the following GPLed libraries:"
 652   "\n"
 653   "${GPL_LIBS}"
 654   "\n"
 655   "As these libraries are covered under the GPLv3, so is this build of cvc5."
 656   "\n"
 657   "cvc5 is also available to you under the terms of the (modified) BSD license."
 658   "\n"
 659   "If you prefer to license cvc5 under those terms, please configure cvc5 to"
 660   "\n"
 661   "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
 662   )
 663 else()
 664   message(
 665   "${Blue}cvc5 license:${ResetColor} modified BSD"
 666   "\n"
 667   "\n"
 668   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 669   "\n"
 670   "it is covered by the (modified) BSD license.  To build against GPL'ed"
 671   "\n"
 672   "libraries which can improve cvc5's performance on arithmetic and bitvector"
 673   "\n"
 674   "logics, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 675   )
 676 endif()
 677
 678 if("${CMAKE_GENERATOR}" STREQUAL "Ninja")
 679   set(BUILD_COMMAND_NAME "ninja")
 680 else()
 681   set(BUILD_COMMAND_NAME "make")
 682 endif()
 683
 684 message("")
 685 message("Now just type '${BUILD_COMMAND_NAME}', "
 686         "followed by '${BUILD_COMMAND_NAME} check' "
 687         "or '${BUILD_COMMAND_NAME} install'.")
 688 message("")