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