CMakeLists.txt

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