CMakeLists.txt

   1 cmake_minimum_required(VERSION 3.2)
   2
   3 #-----------------------------------------------------------------------------#
   4 # Project configuration
   5
   6 project(cvc4)
   7
   8 set(CVC4_MAJOR   1) # Major component of the version of CVC4.
   9 set(CVC4_MINOR   8) # Minor component of the version of CVC4.
  10 set(CVC4_RELEASE 0) # Release component of the version of CVC4.
  11
  12 # Extraversion component of the version of CVC4.
  13 set(CVC4_EXTRAVERSION "-prerelease")
  14
  15 # Shared library versioning. Increment SOVERSION for every new CVC4 release.
  16 set(CVC4_SOVERSION 6)
  17
  18 # Full release string for CVC4.
  19 if(CVC4_RELEASE)
  20   set(CVC4_RELEASE_STRING
  21       "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
  22 else()
  23   set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}")
  24 endif()
  25
  26 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
  27 set(CMAKE_C_STANDARD 99)
  28 set(CMAKE_CXX_STANDARD 11)
  29 set(CMAKE_CXX_EXTENSIONS OFF)
  30
  31 # Generate compile_commands.json, which can be used for various code completion
  32 # plugins.
  33 set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
  34
  35 #-----------------------------------------------------------------------------#
  36 # Policies
  37
  38 # Required for FindGLPK since it sets CMAKE_REQUIRED_LIBRARIES
  39 if(POLICY CMP0075)
  40   cmake_policy(SET CMP0075 NEW)
  41 endif()
  42
  43 #-----------------------------------------------------------------------------#
  44 # Tell CMake where to find our dependencies
  45
  46 if(ABC_DIR)
  47   list(APPEND CMAKE_PREFIX_PATH "${ABC_DIR}")
  48 endif()
  49 if(ANTLR_DIR)
  50   list(APPEND CMAKE_PREFIX_PATH "${ANTLR_DIR}")
  51 endif()
  52 if(CADICAL_DIR)
  53   list(APPEND CMAKE_PREFIX_PATH "${CADICAL_DIR}")
  54 endif()
  55 if(CRYPTOMINISAT_DIR)
  56   list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}")
  57 endif()
  58 if(CXXTEST_DIR)
  59   list(APPEND CMAKE_PREFIX_PATH "${CXXTEST_DIR}")
  60 endif()
  61 if(DRAT2ER_DIR)
  62   list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}")
  63 endif()
  64 if(GLPK_DIR)
  65   list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}")
  66 endif()
  67 if(GMP_DIR)
  68   list(APPEND CMAKE_PREFIX_PATH "${GMP_DIR}")
  69 endif()
  70 if(LFSC_DIR)
  71   list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}")
  72 endif()
  73 if(SYMFPU_DIR)
  74   list(APPEND CMAKE_PREFIX_PATH "${SYMFPU_DIR}")
  75 endif()
  76
  77 # By default the contrib/get-* scripts install dependencies to deps/install.
  78 list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps/install")
  79
  80 #-----------------------------------------------------------------------------#
  81
  82 set(INCLUDE_INSTALL_DIR include)
  83 set(LIBRARY_INSTALL_DIR lib)
  84 set(RUNTIME_INSTALL_DIR bin)
  85
  86 #-----------------------------------------------------------------------------#
  87
  88 # Embed the installation prefix as an RPATH in the executable such that the
  89 # linker can find our libraries (such as libcvc4parser) when executing the cvc4
  90 # binary. This is for example useful when installing CVC4 with a custom prefix
  91 # on macOS (e.g. when using homebrew in a non-standard directory). If we do not
  92 # set this option, then the linker will not be able to find the required
  93 # libraries when trying to run CVC4.
  94 #
  95 # More information on RPATH in CMake:
  96 # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
  97 set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${LIBRARY_INSTALL_DIR}")
  98
  99 #-----------------------------------------------------------------------------#
 100
 101 include(Helpers)
 102
 103 #-----------------------------------------------------------------------------#
 104 # User options
 105
 106 # License
 107 option(ENABLE_GPL "Enable GPL dependencies")
 108
 109 # General build options
 110 #
 111 # >> 3-valued: IGNORE ON OFF
 112 #    > allows to detect if set by user (default: IGNORE)
 113 #    > only necessary for options set for build types
 114 cvc4_option(ENABLE_ASAN           "Enable ASAN build")
 115 cvc4_option(ENABLE_UBSAN          "Enable UBSan build")
 116 cvc4_option(ENABLE_TSAN           "Enable TSan build")
 117 cvc4_option(ENABLE_ASSERTIONS     "Enable assertions")
 118 cvc4_option(ENABLE_COMP_INC_TRACK
 119             "Enable optimizations for incremental SMT-COMP tracks")
 120 cvc4_option(ENABLE_DEBUG_SYMBOLS  "Enable debug symbols")
 121 cvc4_option(ENABLE_DUMPING        "Enable dumping")
 122 cvc4_option(ENABLE_MUZZLE         "Suppress ALL non-result output")
 123 cvc4_option(ENABLE_OPTIMIZED      "Enable optimization")
 124 cvc4_option(ENABLE_PROOFS         "Enable proof support")
 125 cvc4_option(ENABLE_REPLAY         "Enable the replay feature")
 126 cvc4_option(ENABLE_STATISTICS     "Enable statistics")
 127 cvc4_option(ENABLE_TRACING        "Enable tracing")
 128 cvc4_option(ENABLE_UNIT_TESTING   "Enable unit testing")
 129 cvc4_option(ENABLE_VALGRIND       "Enable valgrind instrumentation")
 130 cvc4_option(ENABLE_SHARED         "Build as shared library")
 131 cvc4_option(ENABLE_STATIC_BINARY
 132             "Build static binaries with statically linked system libraries")
 133 # >> 2-valued: ON OFF
 134 #    > for options where we don't need to detect if set by user (default: OFF)
 135 option(ENABLE_BEST             "Enable dependencies known to give best performance")
 136 option(ENABLE_COVERAGE         "Enable support for gcov coverage testing")
 137 option(ENABLE_DEBUG_CONTEXT_MM "Enable the debug context memory manager")
 138 option(ENABLE_PROFILING        "Enable support for gprof profiling")
 139
 140 # Optional dependencies
 141 #
 142 # >> 3-valued: IGNORE ON OFF
 143 #    > allows to detect if set by user (default: IGNORE)
 144 #    > only necessary for options set for ENABLE_BEST
 145 cvc4_option(USE_ABC           "Use ABC for AIG bit-blasting")
 146 cvc4_option(USE_CADICAL       "Use CaDiCaL SAT solver")
 147 cvc4_option(USE_CLN           "Use CLN instead of GMP")
 148 cvc4_option(USE_GLPK          "Use GLPK simplex solver")
 149 cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
 150 cvc4_option(USE_READLINE      "Use readline for better interactive support")
 151 # >> 2-valued: ON OFF
 152 #    > for options where we don't need to detect if set by user (default: OFF)
 153 option(USE_DRAT2ER            "Include drat2er for making eager BV proofs")
 154 option(USE_LFSC               "Use LFSC proof checker")
 155 option(USE_SYMFPU             "Use SymFPU for floating point support")
 156 option(USE_PYTHON2            "Prefer using Python 2 (for Python bindings)")
 157 option(USE_PYTHON3            "Prefer using Python 3 (for Python bindings)")
 158
 159 # Custom install directories for dependencies
 160 # If no directory is provided by the user, we first check if the dependency was
 161 # installed via the corresponding contrib/get-* script and if not found, we
 162 # check the intalled system version. If the user provides a directory we
 163 # immediately fail if the dependency was not found at the specified location.
 164 set(ABC_DIR           "" CACHE STRING "Set ABC install directory")
 165 set(ANTLR_DIR         "" CACHE STRING "Set ANTLR3 install directory")
 166 set(CADICAL_DIR       "" CACHE STRING "Set CaDiCaL install directory")
 167 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
 168 set(CXXTEST_DIR       "" CACHE STRING "Set CxxTest install directory")
 169 set(DRAT2ER_DIR       "" CACHE STRING "Set drat2er install directory")
 170 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 171 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
 172 set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
 173 set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 174
 175 # Prepend binaries with prefix on make install
 176 set(PROGRAM_PREFIX    "" CACHE STRING "Program prefix on make install")
 177
 178 # Supported language bindings
 179 option(BUILD_BINDINGS_JAVA   "Build Java bindings")
 180 option(BUILD_BINDINGS_PYTHON "Build Python bindings")
 181
 182 #-----------------------------------------------------------------------------#
 183 # Internal cmake variables
 184
 185 set(OPTIMIZATION_LEVEL 3)
 186 set(GPL_LIBS "")
 187
 188 #-----------------------------------------------------------------------------#
 189 # Determine number of threads available, used to configure (default) parallel
 190 # execution of custom test targets (can be overriden with ARGS=-jN).
 191
 192 include(ProcessorCount)
 193 ProcessorCount(CTEST_NTHREADS)
 194 if(CTEST_NTHREADS EQUAL 0)
 195   set(CTEST_NTHREADS 1)
 196 endif()
 197
 198 #-----------------------------------------------------------------------------#
 199 # Build types
 200
 201 # Note: Module CodeCoverage requires the name of the debug build to conform
 202 #       to cmake standards (first letter uppercase).
 203 set(BUILD_TYPES Production Debug Testing Competition)
 204
 205 if(ENABLE_ASAN OR ENABLE_UBSAN OR ENABLE_TSAN)
 206   set(CMAKE_BUILD_TYPE Debug)
 207 endif()
 208
 209 # Set the default build type to Production
 210 if(NOT CMAKE_BUILD_TYPE)
 211   set(CMAKE_BUILD_TYPE
 212       Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
 213   # Provide drop down menu options in cmake-gui
 214   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 215 endif()
 216
 217 # Check if specified build type is valid.
 218 list(FIND BUILD_TYPES ${CMAKE_BUILD_TYPE} FOUND_BUILD_TYPE)
 219 if(${FOUND_BUILD_TYPE} EQUAL -1)
 220   message(FATAL_ERROR
 221     "'${CMAKE_BUILD_TYPE}' is not a valid build type. "
 222     "Available builds are: ${BUILD_TYPES}")
 223 endif()
 224
 225 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 226 include(Config${CMAKE_BUILD_TYPE})
 227
 228 #-----------------------------------------------------------------------------#
 229 # Compiler flags
 230
 231 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
 232 add_check_c_cxx_flag("-Wall")
 233 add_check_c_flag("-fexceptions")
 234 add_check_c_cxx_flag("-Wno-deprecated")
 235 add_check_cxx_flag("-Wsuggest-override")
 236 add_check_cxx_flag("-Wnon-virtual-dtor")
 237 add_check_c_cxx_flag("-Wimplicit-fallthrough")
 238
 239 # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
 240 # cdlist.h warnings. Remove when fixed.
 241 add_check_cxx_flag("-Wno-class-memaccess")
 242
 243 #-----------------------------------------------------------------------------#
 244 # Option defaults (three-valued options (cvc4_option(...)))
 245 #
 246 # These options are only set if their value is IGNORE. Otherwise, the user
 247 # already set the option, which we don't want to overwrite.
 248
 249 if(ENABLE_STATIC_BINARY)
 250   cvc4_set_option(ENABLE_SHARED OFF)
 251 else()
 252   cvc4_set_option(ENABLE_SHARED ON)
 253 endif()
 254
 255 #-----------------------------------------------------------------------------#
 256 # Set options for best configuration
 257
 258 if(ENABLE_BEST)
 259   cvc4_set_option(USE_ABC ON)
 260   cvc4_set_option(USE_CADICAL ON)
 261   cvc4_set_option(USE_CLN ON)
 262   cvc4_set_option(USE_CRYPTOMINISAT ON)
 263   cvc4_set_option(USE_GLPK ON)
 264   cvc4_set_option(USE_READLINE ON)
 265 endif()
 266
 267 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
 268 # that expect AssertionException to be thrown will fail.
 269 if(NOT ENABLE_ASSERTIONS)
 270   set(ENABLE_UNIT_TESTING OFF)
 271 endif()
 272
 273 #-----------------------------------------------------------------------------#
 274 # Shared/static libraries
 275 #
 276 # This needs to be set before any find_package(...) command since we want to
 277 # search for static libraries with suffix .a.
 278
 279 if(ENABLE_SHARED)
 280   set(BUILD_SHARED_LIBS ON)
 281   if(ENABLE_STATIC_BINARY)
 282     set(ENABLE_STATIC_BINARY OFF)
 283     message(WARNING "Disabling static binary since shared build is enabled.")
 284   endif()
 285 else()
 286   set(CMAKE_FIND_LIBRARY_SUFFIXES .a ${CMAKE_FIND_LIBRARY_SUFFIXES})
 287   set(BUILD_SHARED_LIBS OFF)
 288   cvc4_set_option(ENABLE_STATIC_BINARY ON)
 289
 290   # Never build unit tests as static binaries, otherwise we'll end up with
 291   # ~300MB per unit test.
 292   if(ENABLE_UNIT_TESTING)
 293     message(WARNING "Disabling unit tests since static build is enabled.")
 294     set(ENABLE_UNIT_TESTING OFF)
 295   endif()
 296 endif()
 297
 298 #-----------------------------------------------------------------------------#
 299 # Enable the ctest testing framework
 300
 301 # This needs to be enabled here rather than in subdirectory test in order to
 302 # allow calling ctest from the root build directory.
 303 enable_testing()
 304
 305 #-----------------------------------------------------------------------------#
 306 # Check GCC version.
 307 #
 308 # GCC version 4.5.1 builds MiniSat incorrectly with -O2, which results in
 309 # incorrect answers.
 310
 311 if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
 312   execute_process(
 313     COMMAND ${CMAKE_CXX_COMPILER} -dumpversion
 314     OUTPUT_VARIABLE GCC_VERSION
 315     OUTPUT_STRIP_TRAILING_WHITESPACE)
 316   if(GCC_VERSION VERSION_EQUAL "4.5.1")
 317     message(FATAL_ERROR
 318       "GCC 4.5.1's optimizer is known to build MiniSat incorrectly "
 319       "(and by extension CVC4).")
 320   endif()
 321 endif()
 322
 323 #-----------------------------------------------------------------------------#
 324 # Check options, find packages and configure build.
 325
 326 if(USE_PYTHON2)
 327   find_package(PythonInterp 2.7 REQUIRED)
 328 elseif(USE_PYTHON3)
 329   find_package(PythonInterp 3 REQUIRED)
 330 else()
 331   find_package(PythonInterp REQUIRED)
 332 endif()
 333
 334 find_package(GMP REQUIRED)
 335
 336 if(ENABLE_ASAN)
 337   # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
 338   # otherwise the -fsanitize=address check will fail while linking.
 339   set(CMAKE_REQUIRED_FLAGS -fsanitize=address)
 340   add_required_c_cxx_flag("-fsanitize=address")
 341   unset(CMAKE_REQUIRED_FLAGS)
 342   add_required_c_cxx_flag("-fno-omit-frame-pointer")
 343   add_check_c_cxx_flag("-fsanitize-recover=address")
 344 endif()
 345
 346 if(ENABLE_UBSAN)
 347   add_required_c_cxx_flag("-fsanitize=undefined")
 348   add_definitions(-DCVC4_USE_UBSAN)
 349 endif()
 350
 351 if(ENABLE_TSAN)
 352   # -fsanitize=thread requires CMAKE_REQUIRED_FLAGS to be explicitely set,
 353   # otherwise the -fsanitize=thread check will fail while linking.
 354   set(CMAKE_REQUIRED_FLAGS -fsanitize=thread)
 355   add_required_c_cxx_flag("-fsanitize=thread")
 356   unset(CMAKE_REQUIRED_FLAGS)
 357 endif()
 358
 359 if(ENABLE_ASSERTIONS)
 360   add_definitions(-DCVC4_ASSERTIONS)
 361 else()
 362   add_definitions(-DNDEBUG)
 363 endif()
 364
 365 if(ENABLE_COVERAGE)
 366   include(CodeCoverage)
 367   APPEND_COVERAGE_COMPILER_FLAGS()
 368   add_definitions(-DCVC4_COVERAGE)
 369   # Note: The ctest command returns a non-zero exit code if tests fail or run
 370   # into a timeout. As a consequence, the coverage report is not generated. To
 371   # prevent this we always return with exit code 0 after the ctest command has
 372   # finished.
 373   setup_target_for_coverage_gcovr_html(
 374     NAME coverage
 375     EXECUTABLE
 376       ctest -j${CTEST_NTHREADS} -LE "example"
 377         --output-on-failure $$ARGS || exit 0
 378     DEPENDS
 379       build-tests)
 380 endif()
 381
 382 if(ENABLE_DEBUG_CONTEXT_MM)
 383   add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
 384 endif()
 385
 386 if(ENABLE_DEBUG_SYMBOLS)
 387   add_check_c_cxx_flag("-ggdb3")
 388 endif()
 389
 390 if(ENABLE_COMP_INC_TRACK)
 391   add_definitions(-DCVC4_SMTCOMP_APPLICATION_TRACK)
 392 endif()
 393
 394 if(ENABLE_MUZZLE)
 395   add_definitions(-DCVC4_MUZZLE)
 396 endif()
 397
 398 if(ENABLE_DUMPING)
 399   add_definitions(-DCVC4_DUMPING)
 400 endif()
 401
 402 if(ENABLE_PROFILING)
 403   add_definitions(-DCVC4_PROFILING)
 404   add_check_c_cxx_flag("-pg")
 405 endif()
 406
 407 if(ENABLE_PROOFS)
 408   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
 409   add_definitions(-DCVC4_PROOF)
 410 endif()
 411
 412 if(ENABLE_REPLAY)
 413   add_definitions(-DCVC4_REPLAY)
 414 endif()
 415
 416 if(ENABLE_TRACING)
 417   add_definitions(-DCVC4_TRACING)
 418 endif()
 419
 420 if(ENABLE_STATISTICS)
 421   add_definitions(-DCVC4_STATISTICS_ON)
 422 endif()
 423
 424 if(ENABLE_VALGRIND)
 425   find_package(Valgrind REQUIRED)
 426   add_definitions(-DCVC4_VALGRIND)
 427 endif()
 428
 429 if(USE_ABC)
 430   find_package(ABC REQUIRED)
 431   add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
 432 endif()
 433
 434 if(USE_CADICAL)
 435   find_package(CaDiCaL REQUIRED)
 436   add_definitions(-DCVC4_USE_CADICAL)
 437 endif()
 438
 439 if(USE_CLN)
 440   set(GPL_LIBS "${GPL_LIBS} cln")
 441   find_package(CLN 1.2.2 REQUIRED)
 442   set(CVC4_USE_CLN_IMP 1)
 443   set(CVC4_USE_GMP_IMP 0)
 444 else()
 445   set(CVC4_USE_CLN_IMP 0)
 446   set(CVC4_USE_GMP_IMP 1)
 447 endif()
 448
 449 if(USE_CRYPTOMINISAT)
 450   # CryptoMiniSat requires pthreads support
 451   set(THREADS_PREFER_PTHREAD_FLAG ON)
 452   find_package(Threads REQUIRED)
 453   if(THREADS_HAVE_PTHREAD_ARG)
 454     add_c_cxx_flag(-pthread)
 455   endif()
 456   find_package(CryptoMiniSat REQUIRED)
 457   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 458 endif()
 459
 460 if(USE_DRAT2ER)
 461   find_package(Drat2Er REQUIRED)
 462   add_definitions(-DCVC4_USE_DRAT2ER)
 463 endif()
 464
 465 if(USE_GLPK)
 466   set(GPL_LIBS "${GPL_LIBS} glpk")
 467   find_package(GLPK REQUIRED)
 468   add_definitions(-DCVC4_USE_GLPK)
 469 endif()
 470
 471 if(USE_LFSC)
 472   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
 473   find_package(LFSC REQUIRED)
 474   add_definitions(-DCVC4_USE_LFSC)
 475 endif()
 476
 477 if(USE_READLINE)
 478   set(GPL_LIBS "${GPL_LIBS} readline")
 479   find_package(Readline REQUIRED)
 480   set(HAVE_LIBREADLINE 1)
 481   if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 482     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 483   endif()
 484 endif()
 485
 486 if(USE_SYMFPU)
 487   find_package(SymFPU REQUIRED)
 488   add_definitions(-DCVC4_USE_SYMFPU)
 489   set(CVC4_USE_SYMFPU 1)
 490 else()
 491   set(CVC4_USE_SYMFPU 0)
 492 endif()
 493
 494 if(GPL_LIBS)
 495   if(NOT ENABLE_GPL)
 496     message(FATAL_ERROR
 497       "Bad configuration detected: BSD-licensed code only, but also requested "
 498       "GPLed libraries: ${GPL_LIBS}")
 499   endif()
 500   set(CVC4_GPL_DEPS 1)
 501 endif()
 502
 503 #-----------------------------------------------------------------------------#
 504 # Generate CVC4's cvc4autoconfig.h header
 505
 506 include(ConfigureCVC4)
 507 configure_file(cvc4autoconfig.h.in cvc4autoconfig.h)
 508 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 509
 510 #-----------------------------------------------------------------------------#
 511 # Add subdirectories
 512
 513 # signatures needs to come before src since it adds source files to libcvc4.
 514 if(ENABLE_PROOFS)
 515   add_subdirectory(proofs/signatures)
 516 endif()
 517
 518 add_subdirectory(doc)
 519 add_subdirectory(src)
 520 add_subdirectory(test)
 521
 522 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
 523   add_subdirectory(src/bindings)
 524 endif()
 525
 526 #-----------------------------------------------------------------------------#
 527 # Package configuration
 528 #
 529 # Export CVC4 targets to support find_package(CVC4) in other cmake projects.
 530
 531 include(CMakePackageConfigHelpers)
 532
 533 install(EXPORT cvc4-targets
 534   FILE CVC4Targets.cmake
 535   NAMESPACE CVC4::
 536   DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4)
 537
 538 configure_package_config_file(
 539   ${CMAKE_SOURCE_DIR}/cmake/CVC4Config.cmake.in
 540   ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
 541   INSTALL_DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
 542   PATH_VARS LIBRARY_INSTALL_DIR
 543 )
 544
 545 write_basic_package_version_file(
 546   ${CMAKE_CURRENT_BINARY_DIR}/CVC4ConfigVersion.cmake
 547   VERSION ${CVC4_RELEASE_STRING}
 548   COMPATIBILITY ExactVersion
 549 )
 550
 551 install(FILES
 552   ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
 553   ${CMAKE_BINARY_DIR}/CVC4ConfigVersion.cmake
 554   DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
 555 )
 556
 557
 558 #-----------------------------------------------------------------------------#
 559 # Print build configuration
 560
 561 # Convert build type to lower case.
 562 string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING)
 563
 564 # Get all definitions added via add_definitions.
 565 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
 566 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
 567
 568 message("CVC4 ${CVC4_RELEASE_STRING}")
 569 message("")
 570 if(ENABLE_COMP_INC_TRACK)
 571   message("Build profile        : ${CVC4_BUILD_PROFILE_STRING} (incremental)")
 572 else()
 573   message("Build profile        : ${CVC4_BUILD_PROFILE_STRING}")
 574 endif()
 575 message("")
 576 print_config("GPL                  :" ENABLE_GPL)
 577 print_config("Best configuration   :" ENABLE_BEST)
 578 print_config("Optimized            :" ENABLE_OPTIMIZED)
 579 print_config("Optimization level   :" OPTIMIZATION_LEVEL)
 580 message("")
 581 print_config("Assertions           :" ENABLE_ASSERTIONS)
 582 print_config("Debug symbols        :" ENABLE_DEBUG_SYMBOLS)
 583 print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
 584 message("")
 585 print_config("Dumping              :" ENABLE_DUMPING)
 586 print_config("Muzzle               :" ENABLE_MUZZLE)
 587 print_config("Proofs               :" ENABLE_PROOFS)
 588 print_config("Replay               :" ENABLE_REPLAY)
 589 print_config("Statistics           :" ENABLE_STATISTICS)
 590 print_config("Tracing              :" ENABLE_TRACING)
 591 message("")
 592 print_config("ASan                 :" ENABLE_ASAN)
 593 print_config("UBSan                :" ENABLE_UBSAN)
 594 print_config("TSan                 :" ENABLE_TSAN)
 595 print_config("Coverage (gcov)      :" ENABLE_COVERAGE)
 596 print_config("Profiling (gprof)    :" ENABLE_PROFILING)
 597 print_config("Unit tests           :" ENABLE_UNIT_TESTING)
 598 print_config("Valgrind             :" ENABLE_VALGRIND)
 599 message("")
 600 print_config("Shared libs          :" ENABLE_SHARED)
 601 print_config("Static binary        :" ENABLE_STATIC_BINARY)
 602 print_config("Java bindings        :" BUILD_BINDINGS_JAVA)
 603 print_config("Python bindings      :" BUILD_BINDINGS_PYTHON)
 604 print_config("Python2              :" USE_PYTHON2)
 605 print_config("Python3              :" USE_PYTHON3)
 606 message("")
 607 print_config("ABC                  :" USE_ABC)
 608 print_config("CaDiCaL              :" USE_CADICAL)
 609 print_config("CryptoMiniSat        :" USE_CRYPTOMINISAT)
 610 print_config("drat2er              :" USE_DRAT2ER)
 611 print_config("GLPK                 :" USE_GLPK)
 612 print_config("LFSC                 :" USE_LFSC)
 613
 614 if(CVC4_USE_CLN_IMP)
 615   message("MP library           : cln")
 616 else()
 617   message("MP library           : gmp")
 618 endif()
 619 print_config("Readline             :" ${USE_READLINE})
 620 print_config("SymFPU               :" ${USE_SYMFPU})
 621 message("")
 622 if(ABC_DIR)
 623   message("ABC dir              : ${ABC_DIR}")
 624 endif()
 625 if(ANTLR_DIR)
 626   message("ANTLR dir            : ${ANTLR_DIR}")
 627 endif()
 628 if(CADICAL_DIR)
 629   message("CADICAL dir          : ${CADICAL_DIR}")
 630 endif()
 631 if(CRYPTOMINISAT_DIR)
 632   message("CRYPTOMINISAT dir    : ${CRYPTOMINISAT_DIR}")
 633 endif()
 634 if(DRAT2ER_DIR)
 635   message("DRAT2ER dir          : ${DRAT2ER_DIR}")
 636 endif()
 637 if(GLPK_DIR)
 638   message("GLPK dir             : ${GLPK_DIR}")
 639 endif()
 640 if(GMP_DIR)
 641   message("GMP dir              : ${GMP_DIR}")
 642 endif()
 643 if(LFSC_DIR)
 644   message("LFSC dir             : ${LFSC_DIR}")
 645 endif()
 646 if(SYMFPU_DIR)
 647   message("SYMFPU dir           : ${SYMFPU_DIR}")
 648 endif()
 649 message("")
 650 message("CPPLAGS (-D...)      : ${CVC4_DEFINITIONS}")
 651 message("CXXFLAGS             : ${CMAKE_CXX_FLAGS}")
 652 message("CFLAGS               : ${CMAKE_C_FLAGS}")
 653 message("")
 654 message("Install prefix       : ${CMAKE_INSTALL_PREFIX}")
 655 message("")
 656
 657 if(GPL_LIBS)
 658   message(
 659   "CVC4 license         : GPLv3 (due to optional libraries; see below)"
 660   "\n"
 661   "\n"
 662   "Please note that CVC4 will be built against the following GPLed libraries:"
 663   "\n"
 664   "${GPL_LIBS}"
 665   "\n"
 666   "As these libraries are covered under the GPLv3, so is this build of CVC4."
 667   "\n"
 668   "CVC4 is also available to you under the terms of the (modified) BSD license."
 669   "\n"
 670   "If you prefer to license CVC4 under those terms, please configure CVC4 to"
 671   "\n"
 672   "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
 673   )
 674 else()
 675   message(
 676   "CVC4 license         : modified BSD"
 677   "\n"
 678   "\n"
 679   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 680   "\n"
 681   "it is covered by the (modified) BSD license.  This is, however, not the best"
 682   "\n"
 683   "performing configuration of CVC4.  To build against GPL'ed libraries which"
 684   "\n"
 685   "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 686   )
 687 endif()
 688
 689 message("")
 690 message("Now just type make, followed by make check or make install.")
 691 message("")