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} AUTO CACHE STRING "${description}")
 116   # Provide drop down menu options in cmake-gui
 117   set_property(CACHE ${var} PROPERTY STRINGS AUTO ON OFF)
 118 endmacro()
 119
 120 macro(cvc4_set_option var value)
 121   if(${var} STREQUAL "AUTO")
 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: AUTO ON OFF, allows to detect if set by user
 134 #              this is only necessary for options set for build types!
 135 cvc4_option(ENABLE_ASSERTIONS    "Enable assertions")
 136 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
 137 cvc4_option(ENABLE_DUMPING       "Enable dumpin")
 138 cvc4_option(ENABLE_MUZZLE        "Enable silencing CVC4; supress ALL non-result output")
 139 cvc4_option(ENABLE_OPTIMIZED     "Enable optimization")
 140 cvc4_option(ENABLE_PROOFS        "Enable proof support")
 141 cvc4_option(ENABLE_REPLAY        "Enable the replay feature")
 142 cvc4_option(ENABLE_TRACING       "Enable tracing")
 143 cvc4_option(ENABLE_STATISTICS    "Enable statistics")
 144 cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
 145 # >> 2-valued: ON OFF, for options where we don't need to detect if set by user
 146 option(ENABLE_COVERAGE           "Enable support for gcov coverage testing" OFF)
 147 option(ENABLE_PROFILING          "Enable support for gprof profiling" OFF)
 148 option(ENABLE_SHARED             "Build as shared library" OFF)
 149
 150 # Optional dependencies
 151 option(USE_CADICAL               "Use CaDiCaL SAT solver")
 152 option(USE_CLN                   "Use CLN instead of GMP")
 153 option(USE_CRYPTOMINISAT         "Use CryptoMiniSat SAT solver")
 154 option(USE_LFSC                  "Use LFSC proof checker")
 155 option(USE_READLINE              "Use readline for better interactive support" OFF)
 156 option(USE_SYMFPU                "Use SymFPU for floating point support")
 157
 158
 159 #-----------------------------------------------------------------------------#
 160 # Internal cmake variables
 161
 162 set(OPT_LEVEL 3)
 163 set(GPL_LIBS "")
 164
 165 set(BUILD_TYPES Production Debug Testing Competition)
 166
 167 #-----------------------------------------------------------------------------#
 168 # CVC4 build variables
 169
 170 set(CVC4_DEBUG 0)
 171 set(CVC4_BUILD_PROFILE_PRODUCTION 0)
 172 set(CVC4_BUILD_PROFILE_DEBUG 0)
 173 set(CVC4_BUILD_PROFILE_TESTING 0)
 174 set(CVC4_BUILD_PROFILE_COMPETITION 0)
 175 # Whether CVC4 is built with the (optional) GPLed library dependences.
 176 set(CVC4_GPL_DEPS 0)
 177
 178 #-----------------------------------------------------------------------------#
 179
 180 find_package(PythonInterp REQUIRED)
 181 find_package(ANTLR REQUIRED)
 182
 183 find_package(GMP REQUIRED)
 184 cvc4_link_library(${GMP_LIBRARIES})
 185 include_directories(${GMP_INCLUDE_DIR})
 186
 187 #-----------------------------------------------------------------------------#
 188 # Compiler flags
 189
 190 add_check_c_cxx_flag("-O${OPT_LEVEL}")
 191 add_check_c_flag("-fexceptions")
 192 add_check_c_cxx_flag("-Wno-deprecated")
 193 add_check_c_cxx_flag("-Wsuggest-override")
 194 add_check_cxx_flag("-Wnon-virtual-dtor")
 195
 196 #-----------------------------------------------------------------------------#
 197 # Build types
 198
 199 if(NOT CMAKE_BUILD_TYPE)
 200   set(CMAKE_BUILD_TYPE production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
 201   # Provide drop down menu options in cmake-gui
 202   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 203 endif()
 204 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 205
 206 if(CMAKE_BUILD_TYPE STREQUAL "Debug")
 207   include(ConfigDebug)
 208 elseif(CMAKE_BUILD_TYPE STREQUAL "Production")
 209   include(ConfigProduction)
 210 elseif(CMAKE_BUILD_TYPE STREQUAL "Testing")
 211   include(ConfigTesting)
 212 elseif(CMAKE_BUILD_TYPE STREQUAL "Competition")
 213   include(ConfigCompetition)
 214   # enable_static=yes
 215   #TODO
 216   # enable_static_binary=yes
 217   #TODO
 218 endif()
 219
 220 #-----------------------------------------------------------------------------#
 221
 222 if(ENABLE_ASSERTIONS)
 223   add_definitions(-DCVC4_ASSERTIONS)
 224 endif()
 225
 226 if(ENABLE_COVERAGE)
 227   include(CodeCoverage)
 228   APPEND_COVERAGE_COMPILER_FLAGS()
 229   add_definitions(-DCVC4_COVERAGE)
 230   # TODO set_up_target_for_coverage + regression tests
 231 endif()
 232
 233 if(ENABLE_DUMPING)
 234   add_definitions(-DCVC4_DUMPING)
 235 else()
 236   add_definitions(-DNDEBUG)
 237 endif()
 238
 239 if(ENABLE_DEBUG_SYMBOLS)
 240   add_check_c_cxx_flag("-ggdb3")
 241 endif()
 242
 243 if(ENABLE_MUZZLE)
 244   add_definitions(-DCVC4_MUZZLE)
 245 endif()
 246
 247 if(ENABLE_PROFILING)
 248   add_definitions(-DCVC4_PROFILING)
 249   add_check_c_cxx_flag("-pg")
 250 endif()
 251
 252 if(ENABLE_PROOFS)
 253   #TODO RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--enable-proof"
 254   add_definitions(-DCVC4_PROOF)
 255   set(CVC4_PROOF 1)
 256 endif()
 257
 258 if(ENABLE_REPLAY)
 259   add_definitions(-DCVC4_REPLAY)
 260 endif()
 261
 262 if(ENABLE_TRACING)
 263   add_definitions(-DCVC4_TRACING)
 264   set(CVC4_TRACING 1)
 265 endif()
 266
 267 if(ENABLE_SHARED)
 268   set(BUILD_SHARED_LIBS ON)
 269 endif()
 270
 271 if(ENABLE_STATISTICS)
 272   add_definitions(-DCVC4_STATISTICS_ON)
 273 endif()
 274
 275 if(ENABLE_VALGRIND)
 276   #TODO check if valgrind available
 277   add_definitions(-DCVC4_VALGRIND)
 278 endif()
 279
 280 if(USE_CADICAL)
 281   find_package(CaDiCaL REQUIRED)
 282   cvc4_link_library(${CaDiCaL_LIBRARIES})
 283   include_directories(${CaDiCaL_INCLUDE_DIR})
 284   add_definitions(-DCVC4_USE_CADICAL)
 285 endif()
 286
 287 if(USE_CLN)
 288   set(GPL_LIBS "${GPL_LIBS} cln")
 289   if(NOT ENABLE_GPL)
 290     message(FATAL_ERROR
 291       "Bad configuration detected: BSD-licensed code only, but also requested "
 292       "GPLed libraries: ${GPL_LIBS}")
 293   endif()
 294   find_package(CLN 1.2.2 REQUIRED)
 295   cvc4_link_library(${CLN_LIBRARIES})
 296   include_directories(${CLN_INCLUDE_DIR})
 297   set(CVC4_USE_CLN_IMP 1)
 298   set(CVC4_USE_GMP_IMP 0)
 299 else()
 300   set(CVC4_USE_CLN_IMP 0)
 301   set(CVC4_USE_GMP_IMP 1)
 302 endif()
 303
 304 if(USE_CRYPTOMINISAT)
 305   # CryptoMiniSat requires pthreads support
 306   set(THREADS_PREFER_PTHREAD_FLAG ON)
 307   find_package(Threads REQUIRED)
 308   if(THREADS_HAVE_PTHREAD_ARG)
 309     add_c_cxx_flag(-pthread)
 310   endif()
 311   find_package(CryptoMiniSat REQUIRED)
 312   cvc4_link_library(${CryptoMiniSat_LIBRARIES})
 313   include_directories(${CryptoMiniSat_INCLUDE_DIR})
 314   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 315 endif()
 316
 317 if(USE_LFSC)
 318   find_package(LFSC REQUIRED)
 319   include_directories(${LFSC_INCLUDE_DIR})
 320   add_definitions(-DCVC4_USE_LFSC)
 321   set(CVC4_USE_LFSC 1)
 322 else()
 323   set(CVC4_USE_LFSC 0)
 324 endif()
 325
 326 if(USE_READLINE)
 327   find_package(Readline REQUIRED)
 328   set(HAVE_LIBREADLINE 1)
 329   if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 330     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 331   else()
 332     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 0)
 333   endif()
 334 else()
 335   set(HAVE_LIBREADLINE 0)
 336 endif()
 337
 338 if(USE_SYMFPU)
 339   find_package(SymFPU REQUIRED)
 340   include_directories(${SymFPU_INCLUDE_DIR})
 341   add_definitions(-DCVC4_USE_SYMFPU)
 342   set(CVC4_USE_SYMFPU 1)
 343 else()
 344   set(CVC4_USE_SYMFPU 0)
 345 endif()
 346
 347 if(GPL_LIBS)
 348   if(NOT ENABLE_GPL)
 349     message(FATAL_ERROR
 350       "Bad configuration detected: BSD-licensed code only, but also requested "
 351       "GPLed libraries: ${GPL_LIBS}")
 352   endif()
 353   set(CVC4_GPL_DEPS 1)
 354 endif()
 355
 356 #-----------------------------------------------------------------------------#
 357
 358 set(VERSION "1.6.0-prerelease")
 359 string(TIMESTAMP MAN_DATE "%Y-%m-%d")
 360
 361 #-----------------------------------------------------------------------------#
 362
 363 include(GetGitRevisionDescription)
 364 get_git_head_revision(GIT_REFSPEC GIT_SHA1)
 365 git_local_changes(GIT_IS_DIRTY)
 366 if(${GIT_IS_DIRTY} STREQUAL "DIRTY")
 367   set(GIT_IS_DIRTY "true")
 368 else()
 369   set(GIT_IS_DIRTY "false")
 370 endif()
 371
 372 execute_process(
 373   COMMAND "${GIT_EXECUTABLE}" rev-parse --abbrev-ref HEAD
 374   OUTPUT_VARIABLE GIT_BRANCH
 375   OUTPUT_STRIP_TRAILING_WHITESPACE
 376 )
 377
 378 #-----------------------------------------------------------------------------#
 379
 380 include(ConfigureCVC4)
 381
 382 # Define to 1 if Boost threading library has support for thread attributes
 383 set(BOOST_HAS_THREAD_ATTR 0)
 384 # Defined if using the CLN multi-precision arithmetic library.
 385 set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP})
 386 # Defined if using the GMP multi-precision arithmetic library.
 387 set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP})
 388 # Defined if the requested minimum BOOST version is satisfied
 389 set(HAVE_BOOST 1)
 390 # Define to 1 if you have <boost/system/error_code.hpp>
 391 set(HAVE_BOOST_SYSTEM_ERROR_CODE_HPP 1)
 392 # Define to 1 if you have <boost/thread.hpp>
 393 set(HAVE_BOOST_THREAD_HPP 1)
 394 # Defined to 1 if clock_gettime() is supported by the platform.
 395 set(HAVE_CLOCK_GETTIME 1)
 396 # define if the compiler supports basic C++11 syntax
 397 set(HAVE_CXX11 1)
 398 # Define to 1 if you have the declaration of `optreset', and to 0 if you don't.
 399 set(HAVE_DECL_OPTRESET 0)
 400 # Define to 1 if you have the declaration of `strerror_r', and to 0 if you
 401 # don't.
 402 set(HAVE_DECL_STRERROR_R 1)
 403 # Define to 1 if you have the <dlfcn.h> header file.
 404 set(HAVE_DLFCN_H 1)
 405 # Define to 1 if you have the <ext/stdio_filebuf.h> header file.
 406 set(HAVE_EXT_STDIO_FILEBUF_H 1)
 407 # Defined to 1 if ffs() is supported by the platform.
 408 set(HAVE_FFS 1)
 409 # Define to 1 if you have the <getopt.h> header file.
 410 set(HAVE_GETOPT_H 1)
 411 # Define to 1 if you have the <inttypes.h> header file.
 412 set(HAVE_INTTYPES_H 1)
 413 # Define to 1 if you have the `gmp' library (-lgmp).
 414 set(HAVE_LIBGMP 1)
 415 ## Define to 1 if you have the `profiler' library (-lprofiler).
 416 #set(HAVE_LIBPROFILER 0)
 417 # Define to 1 to use libreadline
 418 #set(HAVE_LIBREADLINE 0)
 419 ## Define to 1 if you have the `tcmalloc' library (-ltcmalloc).
 420 #set(HAVE_LIBTCMALLOC 0)
 421 # Define to 1 if you have the <memory.h> header file.
 422 set(HAVE_MEMORY_H 1)
 423 # Defined to 1 if sigaltstack() is supported by the platform.
 424 set(HAVE_SIGALTSTACK 1)
 425 # Define to 1 if you have the <stdint.h> header file.
 426 set(HAVE_STDINT_H 1)
 427 # Define to 1 if you have the <stdlib.h> header file.
 428 set(HAVE_STDLIB_H 1)
 429 # Define to 1 if you have the `strerror_r' function.
 430 set(HAVE_STRERROR_R 1)
 431 # Define to 1 if you have the <strings.h> header file.
 432 set(HAVE_STRINGS_H 1)
 433 # Define to 1 if you have the <string.h> header file.
 434 set(HAVE_STRING_H 1)
 435 # Defined to 1 if strtok_r() is supported by the platform.
 436 set(HAVE_STRTOK_R 1)
 437 # Define to 1 if you have the <sys/stat.h> header file.
 438 set(HAVE_SYS_STAT_H 1)
 439 # Define to 1 if you have the <sys/types.h> header file.
 440 set(HAVE_SYS_TYPES_H 1)
 441 # Define to 1 if you have the <unistd.h> header file.
 442 set(HAVE_UNISTD_H 1)
 443 ## Define to the sub-directory where libtool stores uninstalled libraries.
 444 #set(LT_OBJDIR ".libs/")
 445 ## Define to 1 if you have the ANSI C header files.
 446 #set(STDC_HEADERS 1)
 447 # Define to 1 if strerror_r returns char *.
 448 set(STRERROR_R_CHAR_P 1)
 449
 450 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
 451 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 452
 453 #-----------------------------------------------------------------------------#
 454
 455 add_subdirectory(doc)
 456 add_subdirectory(src)
 457
 458 if(ENABLE_PROOFS)
 459   add_subdirectory(proofs/signatures)
 460   cvc4_link_library(signatures)
 461 endif()
 462
 463 #-----------------------------------------------------------------------------#
 464
 465 if(CVC4_BUILD_PROFILE_PRODUCTION)
 466   set(CVC4_BUILD_PROFILE_STRING "production")
 467 elseif(CVC4_BUILD_PROFILE_DEBUG)
 468   set(CVC4_BUILD_PROFILE_STRING "debug")
 469 elseif(CVC4_BUILD_PROFILE_TESTING)
 470   set(CVC4_BUILD_PROFILE_STRING "testing")
 471 elseif(CVC4_BUILD_PROFILE_COMPETITION)
 472   set(CVC4_BUILD_PROFILE_STRING "competition")
 473 endif()
 474
 475 message("CVC4 ${CVC4_RELEASE_STRING}")
 476 message("")
 477 message("Build profile     : ${CVC4_BUILD_PROFILE_STRING}")
 478 message("Optimized         : ${ENABLE_OPTIMIZED}")
 479 message("Optimization level: ${OPTIMIZATION_LEVEL}")
 480 message("Debug symbols     : ${ENABLE_DEBUG_SYMBOLS}")
 481 message("Proofs            : ${ENABLE_PROOFS}")
 482 message("Statistics        : ${ENABLE_STATISTICS}")
 483 message("Replay            : ${ENABLE_REPLAY}")
 484 message("Assertions        : ${ENABLE_ASSERTIONS}")
 485 message("Tracing           : ${ENABLE_TRACING}")
 486 message("Dumping           : ${ENABLE_DUMPING}")
 487 message("Muzzle            : ${ENABLE_MUZZLE}")
 488 message("")
 489 #message("Unit tests   : ${support_unit_tests}")
 490 message("gcov support      : ${ENABLE_COVERAGE}")
 491 message("gprof support     : ${ENABLE_PROFILING}")
 492 #message("")
 493 #message("Static libs  : ${enable_static}")
 494 #message("Shared libs  : ${enable_shared}")
 495 #message("Static binary: ${enable_static_binary}")
 496 #message("Compat lib   : ${CVC4_BUILD_LIBCOMPAT}")
 497 #message("Bindings     : ${bindings_to_be_built}")
 498 #message("")
 499 #message("Multithreaded: ${support_multithreaded}")
 500 #message("Portfolio    : ${with_portfolio}")
 501 message("")
 502 #message("ABC          : ${{with_abc}")
 503 message("CaDiCaL           : ${USE_CADICAL}")
 504 message("Cryptominisat     : ${USE_CRYPTOMINISAT}")
 505 #message("GLPK              : ${USE_GLPK}")
 506 message("LFSC              : ${USE_LFSC}")
 507 #message("MP library   : ${mplibrary}")
 508 message("Readline          : ${USE_READLINE}")
 509 message("SymFPU            : ${USE_SYMFPU}")
 510 message("")
 511 #message("CPPFLAGS     : ${CPPFLAGS}")
 512 message("CXXFLAGS          : ${CMAKE_CXX_FLAGS}")
 513 message("CFLAGS            : ${CMAKE_C_FLAGS}")
 514 #message("LIBS         : ${LIBS}")
 515 #message("LDFLAGS      : ${LDFLAGS}")
 516 #message("")
 517 #message("libcvc4 version        : ${{CVC4_LIBRARY_VERSION}")
 518 #message("libcvc4parser version  : ${CVC4_PARSER_LIBRARY_VERSION}")
 519 #message("libcvc4compat version  : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}")
 520 #message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}")
 521 #message("")
 522 #message("Install into : ${prefix}")
 523 message("")
 524
 525 if(GPL_LIBS)
 526   message(
 527   "CVC4 license      : GPLv3 (due to optional libraries; see below)"
 528   "\n"
 529   "\n"
 530   "Please note that CVC4 will be built against the following GPLed libraries:"
 531   "\n"
 532   "${GPL_LIBS}"
 533   "\n"
 534   "As these libraries are covered under the GPLv3, so is this build of CVC4."
 535   "\n"
 536   "CVC4 is also available to you under the terms of the (modified) BSD license."
 537   "\n"
 538   "If you prefer to license CVC4 under those terms, please configure CVC4 to"
 539   "\n"
 540   "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
 541   )
 542 else()
 543   message(
 544   "CVC4 license      : modified BSD"
 545   "\n"
 546   "\n"
 547   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 548   "\n"
 549   "it is covered by the (modified) BSD license.  This is, however, not the best"
 550   "\n"
 551   "performing configuration of CVC4.  To build against GPL'ed libraries which"
 552   "\n"
 553   "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 554   )
 555 endif()
 556
 557 message("")
 558 message("Now just type make, followed by make check or make install.")
 559 message("")