CMakeLists.txt

   1 cmake_minimum_required (VERSION 3.0.1)
   2
   3 #-----------------------------------------------------------------------------#
   4
   5 project(cvc4)
   6
   7 # Major component of the version of CVC4.
   8 set(CVC4_MAJOR 1)
   9 # Minor component of the version of CVC4.
  10 set(CVC4_MINOR 6)
  11 # Release component of the version of CVC4.
  12 set(CVC4_RELEASE 0)
  13 # Extraversion component of the version of CVC4.
  14 set(CVC4_EXTRAVERSION "-prerelease")
  15
  16 # Full release string for CVC4.
  17 if(CVC4_RELEASE)
  18   set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
  19 else()
  20   set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}")
  21 endif()
  22
  23 # Define to the full name of this package.
  24 set(PACKAGE_NAME "${PROJECT_NAME}")
  25
  26 #### These defines are only use in autotools make files, will likely be
  27 #### replaced with corresponding CPack stuff
  28 ## Define to the full name and version of this package.
  29 #set(PACKAGE_STRING "${PROJECT_NAME} ${CVC4_RELEASE_STRING}")
  30 ## Define to the one symbol short name of this package.
  31 #set(PACKAGE_TARNAME "${PROJECT_NAME}")
  32 ## Define to the home page for this package.
  33 #set(PACKAGE_URL "")
  34 ## Define to the version of this package.
  35 #set(PACKAGE_VERSION "${CVC4_RELEASE_STRING}")
  36 ## Define to the address where bug reports for this package should be sent.
  37 #set(PACKAGE_BUGREPORT "cvc4-bugs@cs.stanford.edu")
  38
  39 #-----------------------------------------------------------------------------#
  40
  41 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
  42 set(CMAKE_C_STANDARD 99)
  43 set(CMAKE_CXX_STANDARD 11)
  44
  45 #-----------------------------------------------------------------------------#
  46 # Macros
  47
  48 include(CheckCCompilerFlag)
  49 include(CheckCXXCompilerFlag)
  50
  51 macro(add_c_flag flag)
  52   set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
  53   message(STATUS "Configuring with C flag '${flag}'")
  54 endmacro()
  55
  56 macro(add_cxx_flag flag)
  57   set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
  58   message(STATUS "Configuring with CXX flag '${flag}'")
  59 endmacro()
  60
  61 macro(add_c_cxx_flag flag)
  62   add_c_flag(${flag})
  63   add_cxx_flag(${flag})
  64 endmacro()
  65
  66 macro(add_check_c_flag flag)
  67   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
  68   check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
  69   if(HAVE_FLAG${flagname})
  70     add_c_flag(${flag})
  71   endif()
  72 endmacro()
  73
  74 macro(add_check_cxx_flag flag)
  75   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
  76   check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
  77   if(HAVE_FLAG${flagname})
  78     add_cxx_flag(${flag})
  79   endif()
  80 endmacro()
  81
  82 macro(add_check_c_cxx_flag flag)
  83   add_check_c_flag(${flag})
  84   add_check_cxx_flag(${flag})
  85 endmacro()
  86
  87 macro(add_required_cxx_flag flag)
  88   string(REGEX REPLACE "[-=]" "_" flagnamename ${flag})
  89   check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
  90   if (NOT HAVE_FLAG${flagname})
  91     message(FATAL_ERROR "Required compiler flag ${flag} not supported")
  92   endif()
  93   add_cxx_flag(${flag})
  94 endmacro()
  95
  96 macro(add_required_c_flag flag)
  97   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
  98   check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
  99   if (NOT HAVE_FLAG${flagname})
 100     message(FATAL_ERROR "Required compiler flag ${flag} not supported")
 101   endif()
 102   add_c_flag(${flag})
 103 endmacro()
 104
 105 macro(add_required_c_cxx_flag flag)
 106   add_required_c_flag(${flag})
 107   add_required_cxx_flag(${flag})
 108 endmacro()
 109
 110 macro(cvc4_link_library library)
 111   set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${library})
 112 endmacro()
 113
 114 macro(cvc4_option var description)
 115   set(${var} IGNORE CACHE STRING "${description}")
 116   # Provide drop down menu options in cmake-gui
 117   set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF)
 118 endmacro()
 119
 120 macro(cvc4_set_option var value)
 121   if(${var} STREQUAL "IGNORE")
 122     set(${var} ${value})
 123   endif()
 124 endmacro()
 125
 126 #-----------------------------------------------------------------------------#
 127 # User options
 128
 129 # License
 130 option(ENABLE_GPL                "Enable GPL dependencies" OFF)
 131
 132 # General build options
 133 # >> 3-valued: INGORE ON OFF, allows to detect if set by user
 134 #              this is only necessary for options set for build types!
 135 cvc4_option(ENABLE_ASAN          "Enable ASAN build")
 136 cvc4_option(ENABLE_ASSERTIONS    "Enable assertions")
 137 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
 138 cvc4_option(ENABLE_DUMPING       "Enable dumpin")
 139 cvc4_option(ENABLE_MUZZLE        "Enable silencing CVC4; supress ALL non-result output")
 140 cvc4_option(ENABLE_OPTIMIZED     "Enable optimization")
 141 cvc4_option(ENABLE_PORTFOLIO     "Enable portfolio support")
 142 cvc4_option(ENABLE_PROOFS        "Enable proof support")
 143 cvc4_option(ENABLE_REPLAY        "Enable the replay feature")
 144 cvc4_option(ENABLE_STATISTICS    "Enable statistics")
 145 cvc4_option(ENABLE_TRACING       "Enable tracing")
 146 cvc4_option(ENABLE_UNIT_TESTING  "Enable unit testing")
 147 cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
 148 cvc4_option(ENABLE_SHARED        "Build as shared library")
 149 # >> 2-valued: ON OFF, for options where we don't need to detect if set by user
 150 option(ENABLE_COVERAGE           "Enable support for gcov coverage testing" OFF)
 151 option(ENABLE_PROFILING          "Enable support for gprof profiling" OFF)
 152
 153 # Optional dependencies
 154 option(USE_CADICAL               "Use CaDiCaL SAT solver")
 155 option(USE_CLN                   "Use CLN instead of GMP")
 156 option(USE_CRYPTOMINISAT         "Use CryptoMiniSat SAT solver")
 157 option(USE_LFSC                  "Use LFSC proof checker")
 158 option(USE_READLINE              "Use readline for better interactive support" OFF)
 159 option(USE_SYMFPU                "Use SymFPU for floating point support")
 160
 161
 162 #-----------------------------------------------------------------------------#
 163 # Internal cmake variables
 164
 165 set(OPT_LEVEL 3)
 166 set(GPL_LIBS "")
 167
 168 set(BUILD_TYPES Production Debug Testing Competition)
 169
 170 #-----------------------------------------------------------------------------#
 171 # CVC4 build variables
 172
 173 set(CVC4_DEBUG 0)
 174 set(CVC4_BUILD_PROFILE_PRODUCTION 0)
 175 set(CVC4_BUILD_PROFILE_DEBUG 0)
 176 set(CVC4_BUILD_PROFILE_TESTING 0)
 177 set(CVC4_BUILD_PROFILE_COMPETITION 0)
 178 # Whether CVC4 is built with the (optional) GPLed library dependences.
 179 set(CVC4_GPL_DEPS 0)
 180
 181 #-----------------------------------------------------------------------------#
 182
 183 find_package(PythonInterp REQUIRED)
 184 find_package(ANTLR REQUIRED)
 185
 186 find_package(GMP REQUIRED)
 187 cvc4_link_library(${GMP_LIBRARIES})
 188 include_directories(${GMP_INCLUDE_DIR})
 189
 190 #-----------------------------------------------------------------------------#
 191 # Compiler flags
 192
 193 add_check_c_cxx_flag("-O${OPT_LEVEL}")
 194 add_check_c_flag("-fexceptions")
 195 add_check_c_cxx_flag("-Wno-deprecated")
 196 add_check_cxx_flag("-Wsuggest-override")
 197 add_check_cxx_flag("-Wnon-virtual-dtor")
 198
 199 #-----------------------------------------------------------------------------#
 200 # Build types
 201
 202 if(ENABLE_ASAN)
 203   set(CMAKE_BUILD_TYPE Debug)
 204 endif()
 205
 206 # Set the default build type to Production
 207 if(NOT CMAKE_BUILD_TYPE)
 208   set(CMAKE_BUILD_TYPE Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
 209   # Provide drop down menu options in cmake-gui
 210   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 211 endif()
 212 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 213
 214 if(CMAKE_BUILD_TYPE STREQUAL "Debug")
 215   include(ConfigDebug)
 216 elseif(CMAKE_BUILD_TYPE STREQUAL "Production")
 217   include(ConfigProduction)
 218 elseif(CMAKE_BUILD_TYPE STREQUAL "Testing")
 219   include(ConfigTesting)
 220 elseif(CMAKE_BUILD_TYPE STREQUAL "Competition")
 221   include(ConfigCompetition)
 222   # enable_static=yes
 223   #TODO
 224   # enable_static_binary=yes
 225   #TODO
 226 endif()
 227
 228 #-----------------------------------------------------------------------------#
 229 # Option defaults (three-valued options (cvc4_option(...)))
 230
 231 cvc4_set_option(ENABLE_PORTFOLIO OFF)
 232 cvc4_set_option(ENABLE_SHARED ON)
 233 cvc4_set_option(ENABLE_VALGRIND OFF)
 234
 235 #-----------------------------------------------------------------------------#
 236 # Enable the ctest testing framework
 237
 238 enable_testing()
 239
 240 #-----------------------------------------------------------------------------#
 241
 242 if(ENABLE_ASAN)
 243   set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address)
 244   add_required_c_cxx_flag("-fsanitize=address")
 245   unset(CMAKE_REQUIRED_LIBRARIES)
 246   add_required_c_cxx_flag("-fno-omit-frame-pointer")
 247   add_check_c_cxx_flag("-fsanitize-recover=address")
 248 endif()
 249
 250 if(ENABLE_ASSERTIONS)
 251   add_definitions(-DCVC4_ASSERTIONS)
 252 endif()
 253
 254 if(ENABLE_COVERAGE)
 255   include(CodeCoverage)
 256   APPEND_COVERAGE_COMPILER_FLAGS()
 257   add_definitions(-DCVC4_COVERAGE)
 258   setup_target_for_coverage_lcov(
 259     NAME coverage
 260     EXECUTABLE ctest $(ARGS)
 261     DEPENDENCIES cvc4-bin)
 262 endif()
 263
 264 if(ENABLE_DUMPING)
 265   add_definitions(-DCVC4_DUMPING)
 266 else()
 267   add_definitions(-DNDEBUG)
 268 endif()
 269
 270 if(ENABLE_DEBUG_SYMBOLS)
 271   add_check_c_cxx_flag("-ggdb3")
 272 endif()
 273
 274 if(ENABLE_MUZZLE)
 275   add_definitions(-DCVC4_MUZZLE)
 276 endif()
 277
 278 if(ENABLE_PORTFOLIO)
 279   find_package(Boost REQUIRED COMPONENTS thread)
 280   # Disable CLN for portfolio builds since it is not thread safe (uses an
 281   # unlocked hash table internally).
 282   set(USE_CLN OFF)
 283   set(THREADS_PREFER_PTHREAD_FLAG ON)
 284   find_package(Threads REQUIRED)
 285   if(THREADS_HAVE_PTHREAD_ARG)
 286     add_c_cxx_flag(-pthread)
 287   endif()
 288   add_definitions(-DCVC4_PORTFOLIO)
 289 endif()
 290
 291 if(ENABLE_PROFILING)
 292   add_definitions(-DCVC4_PROFILING)
 293   add_check_c_cxx_flag("-pg")
 294 endif()
 295
 296 if(ENABLE_PROOFS)
 297   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
 298   add_definitions(-DCVC4_PROOF)
 299   set(CVC4_PROOF 1)
 300 endif()
 301
 302 if(ENABLE_REPLAY)
 303   add_definitions(-DCVC4_REPLAY)
 304 endif()
 305
 306 if(ENABLE_TRACING)
 307   add_definitions(-DCVC4_TRACING)
 308   set(CVC4_TRACING 1)
 309 endif()
 310
 311 if(ENABLE_UNIT_TESTING)
 312         find_package(CxxTest REQUIRED)
 313   # Force shared libs for unit tests, static libs with unit tests are not
 314   # working right now.
 315   set(ENABLE_SHARED ON)
 316 endif()
 317
 318 if(ENABLE_SHARED)
 319   set(BUILD_SHARED_LIBS ON)
 320 endif()
 321
 322 if(ENABLE_STATISTICS)
 323   add_definitions(-DCVC4_STATISTICS_ON)
 324 endif()
 325
 326 if(ENABLE_VALGRIND)
 327   #TODO check if valgrind available
 328   add_definitions(-DCVC4_VALGRIND)
 329 endif()
 330
 331 if(USE_CADICAL)
 332   find_package(CaDiCaL REQUIRED)
 333   cvc4_link_library(${CaDiCaL_LIBRARIES})
 334   include_directories(${CaDiCaL_INCLUDE_DIR})
 335   add_definitions(-DCVC4_USE_CADICAL)
 336 endif()
 337
 338 if(USE_CLN)
 339   set(GPL_LIBS "${GPL_LIBS} cln")
 340   if(NOT ENABLE_GPL)
 341     message(FATAL_ERROR
 342       "Bad configuration detected: BSD-licensed code only, but also requested "
 343       "GPLed libraries: ${GPL_LIBS}")
 344   endif()
 345   find_package(CLN 1.2.2 REQUIRED)
 346   cvc4_link_library(${CLN_LIBRARIES})
 347   include_directories(${CLN_INCLUDE_DIR})
 348   set(CVC4_USE_CLN_IMP 1)
 349   set(CVC4_USE_GMP_IMP 0)
 350 else()
 351   set(CVC4_USE_CLN_IMP 0)
 352   set(CVC4_USE_GMP_IMP 1)
 353 endif()
 354
 355 if(USE_CRYPTOMINISAT)
 356   # CryptoMiniSat requires pthreads support
 357   set(THREADS_PREFER_PTHREAD_FLAG ON)
 358   find_package(Threads REQUIRED)
 359   if(THREADS_HAVE_PTHREAD_ARG)
 360     add_c_cxx_flag(-pthread)
 361   endif()
 362   find_package(CryptoMiniSat REQUIRED)
 363   cvc4_link_library(${CryptoMiniSat_LIBRARIES})
 364   include_directories(${CryptoMiniSat_INCLUDE_DIR})
 365   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 366 endif()
 367
 368 if(USE_LFSC)
 369   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
 370   find_package(LFSC REQUIRED)
 371   include_directories(${LFSC_INCLUDE_DIR})
 372   add_definitions(-DCVC4_USE_LFSC)
 373   set(CVC4_USE_LFSC 1)
 374 else()
 375   set(CVC4_USE_LFSC 0)
 376 endif()
 377
 378 if(USE_READLINE)
 379   find_package(Readline REQUIRED)
 380   set(HAVE_LIBREADLINE 1)
 381   if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 382     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 383   else()
 384     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 0)
 385   endif()
 386 else()
 387   set(HAVE_LIBREADLINE 0)
 388 endif()
 389
 390 if(USE_SYMFPU)
 391   find_package(SymFPU REQUIRED)
 392   include_directories(${SymFPU_INCLUDE_DIR})
 393   add_definitions(-DCVC4_USE_SYMFPU)
 394   set(CVC4_USE_SYMFPU 1)
 395 else()
 396   set(CVC4_USE_SYMFPU 0)
 397 endif()
 398
 399 if(GPL_LIBS)
 400   if(NOT ENABLE_GPL)
 401     message(FATAL_ERROR
 402       "Bad configuration detected: BSD-licensed code only, but also requested "
 403       "GPLed libraries: ${GPL_LIBS}")
 404   endif()
 405   set(CVC4_GPL_DEPS 1)
 406 endif()
 407
 408 #-----------------------------------------------------------------------------#
 409
 410 set(VERSION "1.6.0-prerelease")
 411 string(TIMESTAMP MAN_DATE "%Y-%m-%d")
 412
 413 #-----------------------------------------------------------------------------#
 414
 415 include(GetGitRevisionDescription)
 416 get_git_head_revision(GIT_REFSPEC GIT_SHA1)
 417 git_local_changes(GIT_IS_DIRTY)
 418 if(${GIT_IS_DIRTY} STREQUAL "DIRTY")
 419   set(GIT_IS_DIRTY "true")
 420 else()
 421   set(GIT_IS_DIRTY "false")
 422 endif()
 423
 424 execute_process(
 425   COMMAND "${GIT_EXECUTABLE}" rev-parse --abbrev-ref HEAD
 426   OUTPUT_VARIABLE GIT_BRANCH
 427   OUTPUT_STRIP_TRAILING_WHITESPACE
 428 )
 429
 430 #-----------------------------------------------------------------------------#
 431
 432 include(ConfigureCVC4)
 433
 434 # Define to 1 if Boost threading library has support for thread attributes
 435 set(BOOST_HAS_THREAD_ATTR 0)
 436 # Defined if using the CLN multi-precision arithmetic library.
 437 set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP})
 438 # Defined if using the GMP multi-precision arithmetic library.
 439 set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP})
 440 ## Defined if the requested minimum BOOST version is satisfied
 441 #set(HAVE_BOOST 1)
 442 ## Define to 1 if you have <boost/system/error_code.hpp>
 443 #set(HAVE_BOOST_SYSTEM_ERROR_CODE_HPP 1)
 444 ## Define to 1 if you have <boost/thread.hpp>
 445 #set(HAVE_BOOST_THREAD_HPP 1)
 446 # Defined to 1 if clock_gettime() is supported by the platform.
 447 set(HAVE_CLOCK_GETTIME 1)
 448 # define if the compiler supports basic C++11 syntax
 449 set(HAVE_CXX11 1)
 450 # Define to 1 if you have the declaration of `optreset', and to 0 if you don't.
 451 set(HAVE_DECL_OPTRESET 0)
 452 ## Define to 1 if you have the declaration of `strerror_r', and to 0 if you
 453 ## don't.
 454 #set(HAVE_DECL_STRERROR_R 1)
 455 ## Define to 1 if you have the <dlfcn.h> header file.
 456 #set(HAVE_DLFCN_H 1)
 457 # Define to 1 if you have the <ext/stdio_filebuf.h> header file.
 458 set(HAVE_EXT_STDIO_FILEBUF_H 1)
 459 # Defined to 1 if ffs() is supported by the platform.
 460 set(HAVE_FFS 1)
 461 # Define to 1 if you have the <getopt.h> header file.
 462 set(HAVE_GETOPT_H 1)
 463 ## Define to 1 if you have the <inttypes.h> header file.
 464 #set(HAVE_INTTYPES_H 1)
 465 ## Define to 1 if you have the `gmp' library (-lgmp).
 466 #set(HAVE_LIBGMP 1)
 467 ## Define to 1 if you have the `profiler' library (-lprofiler).
 468 #set(HAVE_LIBPROFILER 0)
 469 # Define to 1 to use libreadline
 470 #set(HAVE_LIBREADLINE 0)
 471 ## Define to 1 if you have the `tcmalloc' library (-ltcmalloc).
 472 #set(HAVE_LIBTCMALLOC 0)
 473 ## Define to 1 if you have the <memory.h> header file.
 474 #set(HAVE_MEMORY_H 1)
 475 # Defined to 1 if sigaltstack() is supported by the platform.
 476 set(HAVE_SIGALTSTACK 1)
 477 ## Define to 1 if you have the <stdint.h> header file.
 478 #set(HAVE_STDINT_H 1)
 479 ## Define to 1 if you have the <stdlib.h> header file.
 480 #set(HAVE_STDLIB_H 1)
 481 # Define to 1 if you have the `strerror_r' function.
 482 set(HAVE_STRERROR_R 1)
 483 ## Define to 1 if you have the <strings.h> header file.
 484 #set(HAVE_STRINGS_H 1)
 485 ## Define to 1 if you have the <string.h> header file.
 486 #set(HAVE_STRING_H 1)
 487 # Defined to 1 if strtok_r() is supported by the platform.
 488 set(HAVE_STRTOK_R 1)
 489 ## Define to 1 if you have the <sys/stat.h> header file.
 490 #set(HAVE_SYS_STAT_H 1)
 491 ## Define to 1 if you have the <sys/types.h> header file.
 492 #set(HAVE_SYS_TYPES_H 1)
 493 # Define to 1 if you have the <unistd.h> header file.
 494 set(HAVE_UNISTD_H 1)
 495 ## Define to the sub-directory where libtool stores uninstalled libraries.
 496 #set(LT_OBJDIR ".libs/")
 497 ## Define to 1 if you have the ANSI C header files.
 498 #set(STDC_HEADERS 1)
 499 # Define to 1 if strerror_r returns char *.
 500 set(STRERROR_R_CHAR_P 1)
 501
 502 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
 503 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 504
 505 #-----------------------------------------------------------------------------#
 506
 507 add_subdirectory(doc)
 508 add_subdirectory(src)
 509 add_subdirectory(test/java)
 510 add_subdirectory(test/regress)
 511 add_subdirectory(test/system)
 512 if(ENABLE_UNIT_TESTING)
 513         add_subdirectory(test/unit)
 514 endif()
 515
 516 if(ENABLE_PROOFS)
 517   add_subdirectory(proofs/signatures)
 518   cvc4_link_library(signatures)
 519 endif()
 520
 521 #-----------------------------------------------------------------------------#
 522
 523 if(CVC4_BUILD_PROFILE_PRODUCTION)
 524   set(CVC4_BUILD_PROFILE_STRING "production")
 525 elseif(CVC4_BUILD_PROFILE_DEBUG)
 526   set(CVC4_BUILD_PROFILE_STRING "debug")
 527 elseif(CVC4_BUILD_PROFILE_TESTING)
 528   set(CVC4_BUILD_PROFILE_STRING "testing")
 529 elseif(CVC4_BUILD_PROFILE_COMPETITION)
 530   set(CVC4_BUILD_PROFILE_STRING "competition")
 531 endif()
 532
 533 message("CVC4 ${CVC4_RELEASE_STRING}")
 534 message("")
 535 message("Build profile     : ${CVC4_BUILD_PROFILE_STRING}")
 536 message("Optimized         : ${ENABLE_OPTIMIZED}")
 537 message("Optimization level: ${OPTIMIZATION_LEVEL}")
 538 message("Debug symbols     : ${ENABLE_DEBUG_SYMBOLS}")
 539 message("Proofs            : ${ENABLE_PROOFS}")
 540 message("Statistics        : ${ENABLE_STATISTICS}")
 541 message("Replay            : ${ENABLE_REPLAY}")
 542 message("Assertions        : ${ENABLE_ASSERTIONS}")
 543 message("Tracing           : ${ENABLE_TRACING}")
 544 message("Dumping           : ${ENABLE_DUMPING}")
 545 message("Muzzle            : ${ENABLE_MUZZLE}")
 546 message("")
 547 message("Unit tests        : ${ENABLE_UNIT_TESTING}")
 548 message("Coverage (gcov)   : ${ENABLE_COVERAGE}")
 549 message("Profiling (gprof) : ${ENABLE_PROFILING}")
 550 message("")
 551 #message("Static libs  : ${enable_static}")
 552 if(BUILD_SHARED_LIBS)
 553         message("Shared libs       : ON")
 554 else()
 555         message("Shared libs       : OFF")
 556 endif()
 557 #message("Static binary: ${enable_static_binary}")
 558 #message("Compat lib   : ${CVC4_BUILD_LIBCOMPAT}")
 559 #message("Bindings     : ${bindings_to_be_built}")
 560 #message("")
 561 #message("Multithreaded: ${support_multithreaded}")
 562 message("Portfolio         : ${ENABLE_PORTFOLIO}")
 563 message("")
 564 #message("ABC          : ${{with_abc}")
 565 message("CaDiCaL           : ${USE_CADICAL}")
 566 message("Cryptominisat     : ${USE_CRYPTOMINISAT}")
 567 #message("GLPK              : ${USE_GLPK}")
 568 message("LFSC              : ${USE_LFSC}")
 569 #message("MP library   : ${mplibrary}")
 570 message("Readline          : ${USE_READLINE}")
 571 message("SymFPU            : ${USE_SYMFPU}")
 572 message("")
 573 #message("CPPFLAGS     : ${CPPFLAGS}")
 574 message("CXXFLAGS          : ${CMAKE_CXX_FLAGS}")
 575 message("CFLAGS            : ${CMAKE_C_FLAGS}")
 576 #message("LIBS         : ${LIBS}")
 577 #message("LDFLAGS      : ${LDFLAGS}")
 578 #message("")
 579 #message("libcvc4 version        : ${{CVC4_LIBRARY_VERSION}")
 580 #message("libcvc4parser version  : ${CVC4_PARSER_LIBRARY_VERSION}")
 581 #message("libcvc4compat version  : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}")
 582 #message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}")
 583 #message("")
 584 #message("Install into : ${prefix}")
 585 message("")
 586
 587 if(GPL_LIBS)
 588   message(
 589   "CVC4 license      : GPLv3 (due to optional libraries; see below)"
 590   "\n"
 591   "\n"
 592   "Please note that CVC4 will be built against the following GPLed libraries:"
 593   "\n"
 594   "${GPL_LIBS}"
 595   "\n"
 596   "As these libraries are covered under the GPLv3, so is this build of CVC4."
 597   "\n"
 598   "CVC4 is also available to you under the terms of the (modified) BSD license."
 599   "\n"
 600   "If you prefer to license CVC4 under those terms, please configure CVC4 to"
 601   "\n"
 602   "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
 603   )
 604 else()
 605   message(
 606   "CVC4 license      : modified BSD"
 607   "\n"
 608   "\n"
 609   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 610   "\n"
 611   "it is covered by the (modified) BSD license.  This is, however, not the best"
 612   "\n"
 613   "performing configuration of CVC4.  To build against GPL'ed libraries which"
 614   "\n"
 615   "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 616   )
 617 endif()
 618
 619 message("")
 620 message("Now just type make, followed by make check or make install.")
 621 message("")