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
 202   # ANTLR uses pragmas that certain versions of MinGW does not support
 203   add_check_c_cxx_flag("-Wno-error=unknown-pragmas")
 204 endif ()
 205
 206 #-----------------------------------------------------------------------------#
 207 # Use ld.gold if available
 208
 209 execute_process(COMMAND ${CMAKE_C_COMPILER}
 210                 -fuse-ld=gold
 211                 -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION)
 212 if ("${LD_VERSION}" MATCHES "GNU gold")
 213   string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold")
 214   string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold")
 215   string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold")
 216   message(STATUS "Using GNU gold linker.")
 217 endif ()
 218
 219 #-----------------------------------------------------------------------------#
 220 # Use interprocedural optimization if requested
 221
 222 if(ENABLE_IPO)
 223   set(CMAKE_INTERPROCEDURAL_OPTIMIZATION TRUE)
 224 endif()
 225
 226 #-----------------------------------------------------------------------------#
 227
 228 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
 229 # that expect AssertionException to be thrown will fail.
 230 if(NOT ENABLE_ASSERTIONS)
 231   message(STATUS "Disabling unit tests since assertions are disabled.")
 232   set(ENABLE_UNIT_TESTING OFF)
 233 endif()
 234
 235 #-----------------------------------------------------------------------------#
 236 # Shared/static libraries
 237
 238 # Embed the installation prefix as an RPATH in the executable such that the
 239 # linker can find our libraries (such as libcvc5parser) when executing the
 240 # cvc5 binary. This is for example useful when installing cvc5 with a custom
 241 # prefix on macOS (e.g. when using homebrew in a non-standard directory). If
 242 # we do not set this option, then the linker will not be able to find the
 243 # required libraries when trying to run cvc5.
 244 #
 245 # Also embed the installation prefix of the installed contrib libraries as an
 246 # RPATH. This allows to install a dynamically linked binary that depends on
 247 # dynamically linked libraries. This is dangerous, as the installed binary
 248 # breaks if the contrib library is removed or changes in other ways, we thus
 249 # print a big warning and only allow if installing to a custom installation
 250 # prefix.
 251 #
 252 # More information on RPATH in CMake:
 253 # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
 254 set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
 255
 256 # Set visibility to default if unit tests are enabled. If unit tests are
 257 # enabled, we also check if we can execute white box unit tests (some versions
 258 # of Clang have issues with the required flag).
 259 set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
 260 if(ENABLE_UNIT_TESTING)
 261   set(CMAKE_CXX_VISIBILITY_PRESET default)
 262   set(CMAKE_VISIBILITY_INLINES_HIDDEN 0)
 263
 264   # Check if Clang version has the bug that was fixed in
 265   # https://reviews.llvm.org/D93104
 266   set(ENABLE_WHITEBOX_UNIT_TESTING ON)
 267   check_cxx_compiler_flag("-faccess-control" HAVE_CXX_FLAGfaccess_control)
 268   if(NOT HAVE_CXX_FLAGfaccess_control)
 269     set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
 270     message(STATUS "Disabling white box unit tests")
 271   endif()
 272 endif()
 273
 274 #-----------------------------------------------------------------------------#
 275 # Enable the ctest testing framework
 276
 277 # This needs to be enabled here rather than in subdirectory test in order to
 278 # allow calling ctest from the root build directory.
 279 enable_testing()
 280
 281 #-----------------------------------------------------------------------------#
 282 # Check options, find packages and configure build.
 283
 284 if(BUILD_SHARED_LIBS)
 285   if (WIN32)
 286     set(CMAKE_FIND_LIBRARY_SUFFIXES .dll .lib .a)
 287   else()
 288     set(CMAKE_FIND_LIBRARY_SUFFIXES .so .dylib .a)
 289   endif()
 290 else()
 291   if (WIN32)
 292     set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a .dll)
 293   else()
 294     set(CMAKE_FIND_LIBRARY_SUFFIXES .a .so .dylib)
 295   endif()
 296 endif()
 297
 298 if(USE_PYTHON2)
 299   find_package(PythonInterp 2.7 REQUIRED)
 300 else()
 301   find_package(PythonInterp 3 REQUIRED)
 302 endif()
 303
 304 find_package(GMP 6.1 REQUIRED)
 305
 306 if(ENABLE_ASAN)
 307   # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
 308   # otherwise the -fsanitize=address check will fail while linking.
 309   set(CMAKE_REQUIRED_FLAGS -fsanitize=address)
 310   add_required_c_cxx_flag("-fsanitize=address")
 311   unset(CMAKE_REQUIRED_FLAGS)
 312   add_required_c_cxx_flag("-fno-omit-frame-pointer")
 313   add_check_c_cxx_flag("-fsanitize-recover=address")
 314 endif()
 315
 316 if(ENABLE_UBSAN)
 317   add_required_c_cxx_flag("-fsanitize=undefined")
 318   add_definitions(-DCVC5_USE_UBSAN)
 319 endif()
 320
 321 if(ENABLE_TSAN)
 322   # -fsanitize=thread requires CMAKE_REQUIRED_FLAGS to be explicitely set,
 323   # otherwise the -fsanitize=thread check will fail while linking.
 324   set(CMAKE_REQUIRED_FLAGS -fsanitize=thread)
 325   add_required_c_cxx_flag("-fsanitize=thread")
 326   unset(CMAKE_REQUIRED_FLAGS)
 327 endif()
 328
 329 if(ENABLE_ASSERTIONS)
 330   add_definitions(-DCVC5_ASSERTIONS)
 331 else()
 332   add_definitions(-DNDEBUG)
 333 endif()
 334
 335 if(ENABLE_COVERAGE)
 336   include(CodeCoverage)
 337   append_coverage_compiler_flags()
 338   add_definitions(-DCVC5_COVERAGE)
 339   setup_code_coverage_fastcov(
 340     NAME coverage
 341     PATH "${PROJECT_SOURCE_DIR}"
 342     EXCLUDE "${CMAKE_BINARY_DIR}/deps/*"
 343     DEPENDENCIES cvc5-bin
 344   )
 345 endif()
 346
 347 if(ENABLE_DEBUG_CONTEXT_MM)
 348   add_definitions(-DCVC5_DEBUG_CONTEXT_MEMORY_MANAGER)
 349 endif()
 350
 351 if(ENABLE_DEBUG_SYMBOLS)
 352   add_check_c_cxx_flag("-ggdb3")
 353 endif()
 354
 355 if(ENABLE_COMP_INC_TRACK)
 356   add_definitions(-DCVC5_SMTCOMP_APPLICATION_TRACK)
 357 endif()
 358
 359 if(ENABLE_MUZZLE)
 360   add_definitions(-DCVC5_MUZZLE)
 361 endif()
 362
 363 if(ENABLE_PROFILING)
 364   add_definitions(-DCVC5_PROFILING)
 365   add_check_c_cxx_flag("-pg")
 366 endif()
 367
 368 if(ENABLE_TRACING)
 369   add_definitions(-DCVC5_TRACING)
 370 endif()
 371
 372 if(ENABLE_STATISTICS)
 373   add_definitions(-DCVC5_STATISTICS_ON)
 374 endif()
 375
 376 if(ENABLE_VALGRIND)
 377   find_package(Valgrind REQUIRED)
 378   add_definitions(-DCVC5_VALGRIND)
 379 endif()
 380
 381 find_package(CaDiCaL REQUIRED)
 382
 383 if(USE_CLN)
 384   set(GPL_LIBS "${GPL_LIBS} cln")
 385   find_package(CLN 1.2.2 REQUIRED)
 386   set(CVC5_USE_CLN_IMP 1)
 387   set(CVC5_USE_GMP_IMP 0)
 388 else()
 389   set(CVC5_USE_CLN_IMP 0)
 390   set(CVC5_USE_GMP_IMP 1)
 391 endif()
 392
 393 if(USE_CRYPTOMINISAT)
 394   # CryptoMiniSat requires pthreads support
 395   set(THREADS_PREFER_PTHREAD_FLAG ON)
 396   find_package(Threads REQUIRED)
 397   if(THREADS_HAVE_PTHREAD_ARG)
 398     add_c_cxx_flag(-pthread)
 399   endif()
 400   find_package(CryptoMiniSat 5.8 REQUIRED)
 401   add_definitions(-DCVC5_USE_CRYPTOMINISAT)
 402 endif()
 403
 404 if(USE_GLPK)
 405   set(GPL_LIBS "${GPL_LIBS} glpk")
 406   find_package(GLPK REQUIRED)
 407   add_definitions(-DCVC5_USE_GLPK)
 408 endif()
 409
 410 if(USE_KISSAT)
 411   find_package(Kissat REQUIRED)
 412   add_definitions(-DCVC5_USE_KISSAT)
 413 endif()
 414
 415 if(USE_POLY)
 416   find_package(Poly REQUIRED)
 417   add_definitions(-DCVC5_USE_POLY)
 418   set(CVC5_USE_POLY_IMP 1)
 419 else()
 420   set(CVC5_USE_POLY_IMP 0)
 421 endif()
 422
 423 if(USE_COCOA)
 424   find_package(CoCoA REQUIRED 0.99711)
 425   add_definitions(-DCVC5_USE_COCOA)
 426 endif()
 427
 428 if(USE_EDITLINE)
 429   find_package(Editline REQUIRED)
 430   set(HAVE_LIBEDITLINE 1)
 431   if(Editline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 432     set(EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 433   endif()
 434 endif()
 435
 436 find_package(SymFPU REQUIRED)
 437
 438 if(GPL_LIBS)
 439   if(NOT ENABLE_GPL)
 440     message(FATAL_ERROR
 441       "Bad configuration detected: BSD-licensed code only, but also requested "
 442       "GPLed libraries: ${GPL_LIBS}")
 443   endif()
 444   set(CVC5_GPL_DEPS 1)
 445 endif()
 446
 447 #-----------------------------------------------------------------------------#
 448 # Provide targets to inspect iwyu suggestions
 449
 450 include(IWYU)
 451 include(fuzzing-murxla)
 452
 453 #-----------------------------------------------------------------------------#
 454
 455 include(ConfigureCvc5)
 456 if(BUILD_SHARED_LIBS)
 457   set(CVC5_STATIC_BUILD OFF)
 458 else()
 459   set(CVC5_STATIC_BUILD ON)
 460   if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin")
 461     cvc5_set_option(STATIC_BINARY ON)
 462   endif()
 463 endif()
 464
 465 #-----------------------------------------------------------------------------#
 466 # Add subdirectories
 467
 468 add_subdirectory(src)
 469
 470 if(BUILD_BINDINGS_PYTHON AND NOT BUILD_SHARED_LIBS)
 471   message(STATUS "Python bindings can only be built in a shared build.")
 472   set(BUILD_BINDINGS_PYTHON OFF)
 473 endif()
 474 if(BUILD_BINDINGS_PYTHON)
 475   set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR})
 476   add_subdirectory(src/api/python)
 477 endif()
 478
 479 if(BUILD_BINDINGS_JAVA)
 480   add_subdirectory(src/api/java)
 481 endif()
 482
 483 if(BUILD_DOCS)
 484   add_subdirectory(docs)
 485 endif()
 486
 487 add_subdirectory(test)
 488
 489 include(target-graphs)
 490
 491 #-----------------------------------------------------------------------------#
 492 # Package configuration
 493 #
 494 # Export cvc5 targets to support find_package(cvc5) in other cmake projects.
 495
 496 include(CMakePackageConfigHelpers)
 497
 498 # If we install a dynamically linked binary that also uses dynamically used
 499 # libraries from deps/install/lib, we need to be cautious. Changing these
 500 # shared libraries from deps/install/lib most probably breaks the binary.
 501 # We only allow such an installation for custom installation prefixes
 502 # (in the assumption that only reasonably experienced users use this and
 503 # also that custom installation prefixes are not used for longer periods of
 504 # time anyway). Also, we print a big warning with further instructions.
 505 if(BUILD_SHARED_LIBS)
 506   # Get the libraries that cvc5 links against
 507   get_target_property(libs cvc5 INTERFACE_LINK_LIBRARIES)
 508   set(LIBS_SHARED_FROM_DEPS "")
 509   foreach(lib ${libs})
 510     # Filter out those that are linked dynamically and come from deps/install
 511     if(lib MATCHES ".*/deps/install/lib/.*\.so")
 512       list(APPEND LIBS_SHARED_FROM_DEPS ${lib})
 513     endif()
 514   endforeach()
 515   list(LENGTH LIBS_SHARED_FROM_DEPS list_len)
 516   # Check if we actually use such "dangerous" libraries
 517   if(list_len GREATER 0)
 518     # Print a generic warning
 519     install(CODE "message(WARNING \"You are installing a dynamically linked \
 520     binary of cvc5 which may be a problem if you are using any dynamically \
 521     linked third-party library that you obtained through one of the \
 522     contrib/get-xxx scripts. The binary uses the rpath mechanism to find these \
 523     locally, hence executing such a contrib script removing the \
 524     \\\"deps/install\\\" folder most probably breaks the installed binary! \
 525     Consider installing the dynamically linked dependencies on your system \
 526     manually or link cvc5 statically.\")")
 527     # Print the libraries in question
 528     foreach(lib ${LIBS_SHARED_FROM_DEPS})
 529       install(CODE "message(WARNING \"The following library is used by the cvc5 binary: ${lib}\")")
 530     endforeach()
 531     # Check if we use a custom installation prefix
 532     if(CMAKE_INSTALL_PREFIX STREQUAL "/usr/local")
 533       install(CODE "message(FATAL_ERROR \"To avoid installing a \
 534       soon-to-be-broken binary, system-wide installation is disabled if the \
 535       binary depends on locally-built shared libraries.\")")
 536     else()
 537       install(CODE "message(WARNING \"You have selected a custom install \
 538       directory ${CMAKE_INSTALL_PREFIX}, so we expect you understood the \
 539       previous warning and know what you are doing.\")")
 540     endif()
 541   endif()
 542 endif()
 543
 544 install(EXPORT cvc5-targets
 545   FILE cvc5Targets.cmake
 546   NAMESPACE cvc5::
 547   DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5)
 548
 549 configure_package_config_file(
 550   ${CMAKE_SOURCE_DIR}/cmake/cvc5Config.cmake.in
 551   ${CMAKE_BINARY_DIR}/cmake/cvc5Config.cmake
 552   INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5
 553   PATH_VARS CMAKE_INSTALL_LIBDIR
 554 )
 555
 556 write_basic_package_version_file(
 557   ${CMAKE_CURRENT_BINARY_DIR}/cvc5ConfigVersion.cmake
 558   VERSION ${CVC5_VERSION}
 559   COMPATIBILITY ExactVersion
 560 )
 561
 562 install(FILES
 563   ${CMAKE_BINARY_DIR}/cmake/cvc5Config.cmake
 564   ${CMAKE_BINARY_DIR}/cvc5ConfigVersion.cmake
 565   DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/cvc5
 566 )
 567
 568
 569 #-----------------------------------------------------------------------------#
 570 # Print build configuration
 571
 572 # Set colors.
 573 if(NOT WIN32)
 574   string(ASCII 27 Esc)
 575   set(Green "${Esc}[32m")
 576   set(Blue "${Esc}[1;34m")
 577   set(ResetColor "${Esc}[m")
 578 endif()
 579
 580 # Convert build type to lower case.
 581 string(TOLOWER ${CMAKE_BUILD_TYPE} CVC5_BUILD_PROFILE_STRING)
 582
 583 # Get all definitions added via add_definitions.
 584 get_directory_property(CVC5_DEFINITIONS COMPILE_DEFINITIONS)
 585 string(REPLACE ";" " " CVC5_DEFINITIONS "${CVC5_DEFINITIONS}")
 586
 587 message("")
 588 print_info("cvc5 ${CVC5_VERSION}")
 589 message("")
 590 if(ENABLE_COMP_INC_TRACK)
 591   print_config("Build profile             " "${CVC5_BUILD_PROFILE_STRING} (incremental)")
 592 else()
 593   print_config("Build profile             " "${CVC5_BUILD_PROFILE_STRING}")
 594 endif()
 595 message("")
 596 print_config("GPL                       " ${ENABLE_GPL})
 597 print_config("Best configuration        " ${ENABLE_BEST})
 598 message("")
 599 print_config("Assertions                " ${ENABLE_ASSERTIONS})
 600 print_config("Debug symbols             " ${ENABLE_DEBUG_SYMBOLS})
 601 print_config("Debug context mem mgr     " ${ENABLE_DEBUG_CONTEXT_MM})
 602 message("")
 603 print_config("Muzzle                    " ${ENABLE_MUZZLE})
 604 print_config("Statistics                " ${ENABLE_STATISTICS})
 605 print_config("Tracing                   " ${ENABLE_TRACING})
 606 message("")
 607 print_config("ASan                      " ${ENABLE_ASAN})
 608 print_config("UBSan                     " ${ENABLE_UBSAN})
 609 print_config("TSan                      " ${ENABLE_TSAN})
 610 print_config("Coverage (gcov)           " ${ENABLE_COVERAGE})
 611 print_config("Profiling (gprof)         " ${ENABLE_PROFILING})
 612 print_config("Unit tests                " ${ENABLE_UNIT_TESTING})
 613 print_config("Valgrind                  " ${ENABLE_VALGRIND})
 614 message("")
 615 print_config("Shared build              " ${BUILD_SHARED_LIBS})
 616 print_config("Python bindings           " ${BUILD_BINDINGS_PYTHON})
 617 print_config("Java bindings             " ${BUILD_BINDINGS_JAVA})
 618 print_config("Python2                   " ${USE_PYTHON2})
 619 print_config("Interprocedural opt.      " ${ENABLE_IPO})
 620 message("")
 621 print_config("CryptoMiniSat             " ${USE_CRYPTOMINISAT} FOUND_SYSTEM ${CryptoMiniSat_FOUND_SYSTEM})
 622 print_config("GLPK                      " ${USE_GLPK})
 623 print_config("Kissat                    " ${USE_KISSAT} FOUND_SYSTEM ${Kissat_FOUND_SYSTEM})
 624 print_config("LibPoly                   " ${USE_POLY} FOUND_SYSTEM ${Poly_FOUND_SYSTEM})
 625 print_config("CoCoALib                  " ${USE_COCOA} FOUND_SYSTEM ${CoCoA_FOUND_SYSTEM})
 626
 627 if(CVC5_USE_CLN_IMP)
 628   print_config("MP library                " "cln" FOUND_SYSTEM ${CLN_FOUND_SYSTEM})
 629 else()
 630   print_config("MP library                " "gmp" FOUND_SYSTEM ${GMP_FOUND_SYSTEM})
 631 endif()
 632 print_config("Editline                  " ${USE_EDITLINE})
 633 message("")
 634 print_config("Api docs                  " ${BUILD_DOCS})
 635 message("")
 636 if(GLPK_DIR)
 637   print_config("GLPK dir                  " ${GLPK_DIR})
 638 endif()
 639 message("")
 640 print_config("CPPLAGS (-D...)" "${CVC5_DEFINITIONS}")
 641 print_config("CXXFLAGS       " "${CMAKE_CXX_FLAGS}")
 642 print_config("CFLAGS         " "${CMAKE_C_FLAGS}")
 643 print_config("Linker flags   " "${CMAKE_EXE_LINKER_FLAGS}")
 644 message("")
 645 print_config("Install prefix " "${CMAKE_INSTALL_PREFIX}")
 646 message("")
 647
 648 if(GPL_LIBS)
 649   message(
 650   "${Blue}cvc5 license: "
 651   "${Yellow}GPLv3 (due to optional libraries; see below)${ResetColor}"
 652   "\n"
 653   "\n"
 654   "Please note that cvc5 will be built against the following GPLed libraries:"
 655   "\n"
 656   "${GPL_LIBS}"
 657   "\n"
 658   "As these libraries are covered under the GPLv3, so is this build of cvc5."
 659   "\n"
 660   "cvc5 is also available to you under the terms of the (modified) BSD license."
 661   "\n"
 662   "If you prefer to license cvc5 under those terms, please configure cvc5 to"
 663   "\n"
 664   "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
 665   )
 666 else()
 667   message(
 668   "${Blue}cvc5 license:${ResetColor} modified BSD"
 669   "\n"
 670   "\n"
 671   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 672   "\n"
 673   "it is covered by the (modified) BSD license.  To build against GPL'ed"
 674   "\n"
 675   "libraries which can improve cvc5's performance on arithmetic and bitvector"
 676   "\n"
 677   "logics, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 678   )
 679 endif()
 680
 681 if("${CMAKE_GENERATOR}" STREQUAL "Ninja")
 682   set(BUILD_COMMAND_NAME "ninja")
 683 else()
 684   set(BUILD_COMMAND_NAME "make")
 685 endif()
 686
 687 message("")
 688 message("Now just type '${BUILD_COMMAND_NAME}', "
 689         "followed by '${BUILD_COMMAND_NAME} check' "
 690         "or '${BUILD_COMMAND_NAME} install'.")
 691 message("")