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 # 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_LFSC          "Use LFSC proof checker")
  97 option(USE_SYMFPU        "Use SymFPU for floating point support")
  98 option(USE_PYTHON2       "Prefer using Python 2 (for Python bindings)")
  99 option(USE_PYTHON3       "Prefer using Python 3 (for Python bindings)")
 100
 101 # Custom install directories for dependencies
 102 # If no directory is provided by the user, we first check if the dependency was
 103 # installed via the corresponding contrib/get-* script and if not found, we
 104 # check the intalled system version. If the user provides a directory we
 105 # immediately fail if the dependency was not found at the specified location.
 106 set(ABC_DIR           "" CACHE STRING "Set ABC install directory")
 107 set(ANTLR_DIR         "" CACHE STRING "Set ANTLR3 install directory")
 108 set(CADICAL_DIR       "" CACHE STRING "Set CaDiCaL install directory")
 109 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
 110 set(CXXTEST_DIR       "" CACHE STRING "Set CxxTest install directory")
 111 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 112 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
 113 set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
 114 set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 115
 116 # Prepend binaries with prefix on make install
 117 set(PROGRAM_PREFIX    "" CACHE STRING "Program prefix on make install")
 118
 119 # Supported language bindings
 120 option(BUILD_BINDINGS_JAVA   "Build Java bindings")
 121 option(BUILD_BINDINGS_PYTHON "Build Python bindings")
 122
 123 #-----------------------------------------------------------------------------#
 124 # Internal cmake variables
 125
 126 set(OPTIMIZATION_LEVEL 3)
 127 set(GPL_LIBS "")
 128
 129 #-----------------------------------------------------------------------------#
 130 # Determine number of threads available, used to configure (default) parallel
 131 # execution of custom test targets (can be overriden with ARGS=-jN).
 132
 133 include(ProcessorCount)
 134 ProcessorCount(CTEST_NTHREADS)
 135 if(CTEST_NTHREADS EQUAL 0)
 136   set(CTEST_NTHREADS 1)
 137 endif()
 138
 139 #-----------------------------------------------------------------------------#
 140 # Build types
 141
 142 # Note: Module CodeCoverage requires the name of the debug build to conform
 143 #       to cmake standards (first letter uppercase).
 144 set(BUILD_TYPES Production Debug Testing Competition)
 145
 146 if(ENABLE_ASAN)
 147   set(CMAKE_BUILD_TYPE Debug)
 148 endif()
 149
 150 # Set the default build type to Production
 151 if(NOT CMAKE_BUILD_TYPE)
 152   set(CMAKE_BUILD_TYPE
 153       Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
 154   # Provide drop down menu options in cmake-gui
 155   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 156 endif()
 157
 158 # Check if specified build type is valid.
 159 list(FIND BUILD_TYPES ${CMAKE_BUILD_TYPE} FOUND_BUILD_TYPE)
 160 if(${FOUND_BUILD_TYPE} EQUAL -1)
 161   message(FATAL_ERROR
 162     "'${CMAKE_BUILD_TYPE}' is not a valid build type. "
 163     "Available builds are: ${BUILD_TYPES}")
 164 endif()
 165
 166 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 167 include(Config${CMAKE_BUILD_TYPE})
 168
 169 #-----------------------------------------------------------------------------#
 170 # Compiler flags
 171
 172 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
 173 add_check_c_cxx_flag("-Wall")
 174 add_check_c_flag("-fexceptions")
 175 add_check_c_cxx_flag("-Wno-deprecated")
 176 add_check_cxx_flag("-Wsuggest-override")
 177 add_check_cxx_flag("-Wnon-virtual-dtor")
 178
 179 # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
 180 # cdlist.h warnings. Remove when fixed.
 181 add_check_cxx_flag("-Wno-class-memaccess")
 182
 183 #-----------------------------------------------------------------------------#
 184 # Option defaults (three-valued options (cvc4_option(...)))
 185 #
 186 # These options are only set if their value is IGNORE. Otherwise, the user
 187 # already set the option, which we don't want to overwrite.
 188
 189 if(ENABLE_STATIC_BINARY)
 190   cvc4_set_option(ENABLE_SHARED OFF)
 191 else()
 192   cvc4_set_option(ENABLE_SHARED ON)
 193 endif()
 194
 195 #-----------------------------------------------------------------------------#
 196 # Set options for best configuration
 197
 198 if(ENABLE_BEST)
 199   cvc4_set_option(USE_ABC ON)
 200   cvc4_set_option(USE_CADICAL ON)
 201   cvc4_set_option(USE_CLN ON)
 202   cvc4_set_option(USE_CRYPTOMINISAT ON)
 203   cvc4_set_option(USE_GLPK ON)
 204   cvc4_set_option(USE_READLINE ON)
 205 endif()
 206
 207 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
 208 # that expect AssertionException to be thrown will fail.
 209 if(NOT ENABLE_ASSERTIONS)
 210   set(ENABLE_UNIT_TESTING OFF)
 211 endif()
 212
 213 # Never build unit tests as static binaries, otherwise we'll end up with
 214 # ~300MB per unit test.
 215 if(ENABLE_UNIT_TESTING)
 216   if(NOT ENABLE_SHARED)
 217     message(WARNING "Disabling static build since unit testing is enabled.")
 218   endif()
 219   set(ENABLE_SHARED ON)
 220 endif()
 221
 222 #-----------------------------------------------------------------------------#
 223 # Shared/static libraries
 224 #
 225 # This needs to be set before any find_package(...) command since we want to
 226 # search for static libraries with suffix .a.
 227
 228 if(ENABLE_SHARED)
 229   set(BUILD_SHARED_LIBS ON)
 230   if(ENABLE_STATIC_BINARY)
 231     set(ENABLE_STATIC_BINARY OFF)
 232     message(WARNING "Disabling static binary since shared build is enabled.")
 233   endif()
 234 else()
 235   set(CMAKE_FIND_LIBRARY_SUFFIXES ".a ${CMAKE_FIND_LIBRARY_SUFFIXES}")
 236   set(BUILD_SHARED_LIBS OFF)
 237   # This is required to force find_package(Boost) to use static libraries.
 238   set(Boost_USE_STATIC_LIBS ON)
 239   cvc4_set_option(ENABLE_STATIC_BINARY ON)
 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_GLPK)
 414   set(GPL_LIBS "${GPL_LIBS} glpk")
 415   set(GLPK_HOME ${GLPK_DIR})
 416   find_package(GLPK REQUIRED)
 417   add_definitions(-DCVC4_USE_GLPK)
 418 endif()
 419
 420 if(USE_LFSC)
 421   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
 422   set(LFSC_HOME ${LFSC_DIR})
 423   find_package(LFSC REQUIRED)
 424   add_definitions(-DCVC4_USE_LFSC)
 425 endif()
 426
 427 if(USE_READLINE)
 428   set(GPL_LIBS "${GPL_LIBS} readline")
 429   find_package(Readline REQUIRED)
 430   set(HAVE_LIBREADLINE 1)
 431   if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 432     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 433   endif()
 434 endif()
 435
 436 if(USE_SYMFPU)
 437   set(SymFPU_HOME ${SYMFPU_DIR})
 438   find_package(SymFPU REQUIRED)
 439   add_definitions(-DCVC4_USE_SYMFPU)
 440   set(CVC4_USE_SYMFPU 1)
 441 else()
 442   set(CVC4_USE_SYMFPU 0)
 443 endif()
 444
 445 if(GPL_LIBS)
 446   if(NOT ENABLE_GPL)
 447     message(FATAL_ERROR
 448       "Bad configuration detected: BSD-licensed code only, but also requested "
 449       "GPLed libraries: ${GPL_LIBS}")
 450   endif()
 451   set(CVC4_GPL_DEPS 1)
 452 endif()
 453
 454 #-----------------------------------------------------------------------------#
 455 # Generate CVC4's cvc4autoconfig.h header
 456
 457 include(ConfigureCVC4)
 458 configure_file(cvc4autoconfig.h.in cvc4autoconfig.h)
 459 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 460
 461 #-----------------------------------------------------------------------------#
 462 # Add subdirectories
 463
 464 # signatures needs to come before src since it adds source files to libcvc4.
 465 if(ENABLE_PROOFS)
 466   add_subdirectory(proofs/signatures)
 467 endif()
 468
 469 add_subdirectory(doc)
 470 add_subdirectory(examples EXCLUDE_FROM_ALL)  # excluded from all target
 471 add_subdirectory(src)
 472 add_subdirectory(test)
 473
 474 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
 475   add_subdirectory(src/bindings)
 476 endif()
 477
 478 #-----------------------------------------------------------------------------#
 479 # Print build configuration
 480
 481 # Convert build type to lower case.
 482 string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING)
 483
 484 # Get all definitions added via add_definitions.
 485 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
 486 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
 487
 488 message("CVC4 ${CVC4_RELEASE_STRING}")
 489 message("")
 490 message("Build profile        : ${CVC4_BUILD_PROFILE_STRING}")
 491 message("")
 492 print_config("GPL                  :" ENABLE_GPL)
 493 print_config("Best configuration   :" ENABLE_BEST)
 494 print_config("Optimized            :" ENABLE_OPTIMIZED)
 495 print_config("Optimization level   :" OPTIMIZATION_LEVEL)
 496 message("")
 497 print_config("Assertions           :" ENABLE_ASSERTIONS)
 498 print_config("Debug symbols        :" ENABLE_DEBUG_SYMBOLS)
 499 print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
 500 message("")
 501 print_config("Dumping              :" ENABLE_DUMPING)
 502 print_config("Muzzle               :" ENABLE_MUZZLE)
 503 print_config("Proofs               :" ENABLE_PROOFS)
 504 print_config("Replay               :" ENABLE_REPLAY)
 505 print_config("Statistics           :" ENABLE_STATISTICS)
 506 print_config("Tracing              :" ENABLE_TRACING)
 507 message("")
 508 print_config("Asan                 :" ENABLE_ASAN)
 509 print_config("Coverage (gcov)      :" ENABLE_COVERAGE)
 510 print_config("Profiling (gprof)    :" ENABLE_PROFILING)
 511 print_config("Unit tests           :" ENABLE_UNIT_TESTING)
 512 print_config("Valgrind             :" ENABLE_VALGRIND)
 513 message("")
 514 print_config("Shared libs          :" ENABLE_SHARED)
 515 print_config("Static binary        :" ENABLE_STATIC_BINARY)
 516 print_config("Java bindings        :" BUILD_BINDINGS_JAVA)
 517 print_config("Python bindings      :" BUILD_BINDINGS_PYTHON)
 518 print_config("Python2              :" USE_PYTHON2)
 519 print_config("Python3              :" USE_PYTHON3)
 520 message("")
 521 print_config("Portfolio            :" ENABLE_PORTFOLIO)
 522 message("")
 523 print_config("ABC                  :" USE_ABC)
 524 print_config("CaDiCaL              :" USE_CADICAL)
 525 print_config("CryptoMiniSat        :" USE_CRYPTOMINISAT)
 526 print_config("GLPK                 :" USE_GLPK)
 527 print_config("LFSC                 :" USE_LFSC)
 528
 529 if(CVC4_USE_CLN_IMP)
 530   message("MP library           : cln")
 531 else()
 532   message("MP library           : gmp")
 533 endif()
 534 print_config("Readline             :" ${USE_READLINE})
 535 print_config("SymFPU               :" ${USE_SYMFPU})
 536 message("")
 537 if(ABC_DIR)
 538   message("ABC dir              : ${ABC_DIR}")
 539 endif()
 540 if(ANTLR_DIR)
 541   message("ANTLR dir            : ${ANTLR_DIR}")
 542 endif()
 543 if(CADICAL_DIR)
 544   message("CADICAL dir          : ${CADICAL_DIR}")
 545 endif()
 546 if(CRYPTOMINISAT_DIR)
 547   message("CRYPTOMINISAT dir    : ${CRYPTOMINISAT_DIR}")
 548 endif()
 549 if(GLPK_DIR)
 550   message("GLPK dir             : ${GLPK_DIR}")
 551 endif()
 552 if(GMP_DIR)
 553   message("GMP dir              : ${GMP_DIR}")
 554 endif()
 555 if(LFSC_DIR)
 556   message("LFSC dir             : ${LFSC_DIR}")
 557 endif()
 558 if(SYMFPU_DIR)
 559   message("SYMFPU dir           : ${SYMFPU_DIR}")
 560 endif()
 561 message("")
 562 message("CPPLAGS (-D...)      : ${CVC4_DEFINITIONS}")
 563 message("CXXFLAGS             : ${CMAKE_CXX_FLAGS}")
 564 message("CFLAGS               : ${CMAKE_C_FLAGS}")
 565 message("")
 566 message("Install prefix       : ${CMAKE_INSTALL_PREFIX}")
 567 message("")
 568
 569 if(GPL_LIBS)
 570   message(
 571   "CVC4 license         : GPLv3 (due to optional libraries; see below)"
 572   "\n"
 573   "\n"
 574   "Please note that CVC4 will be built against the following GPLed libraries:"
 575   "\n"
 576   "${GPL_LIBS}"
 577   "\n"
 578   "As these libraries are covered under the GPLv3, so is this build of CVC4."
 579   "\n"
 580   "CVC4 is also available to you under the terms of the (modified) BSD license."
 581   "\n"
 582   "If you prefer to license CVC4 under those terms, please configure CVC4 to"
 583   "\n"
 584   "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
 585   )
 586 else()
 587   message(
 588   "CVC4 license         : modified BSD"
 589   "\n"
 590   "\n"
 591   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 592   "\n"
 593   "it is covered by the (modified) BSD license.  This is, however, not the best"
 594   "\n"
 595   "performing configuration of CVC4.  To build against GPL'ed libraries which"
 596   "\n"
 597   "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 598   )
 599 endif()
 600
 601 message("")
 602 message("Now just type make, followed by make check or make install.")
 603 message("")