CMakeLists.txt

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