CMakeLists.txt

   1 cmake_minimum_required(VERSION 3.1)
   2
   3 if(POLICY CMP0075)
   4   cmake_policy(SET CMP0075 NEW)
   5 endif()
   6
   7 #-----------------------------------------------------------------------------#
   8
   9 project(cvc4)
  10
  11 set(CVC4_MAJOR   1) # Major component of the version of CVC4.
  12 set(CVC4_MINOR   7) # Minor component of the version of CVC4.
  13 set(CVC4_RELEASE 0) # Release component of the version of CVC4.
  14
  15 # Extraversion component of the version of CVC4.
  16 set(CVC4_EXTRAVERSION "-prerelease")
  17
  18 # Shared library versioning. Increment SOVERSION for every new CVC4 release.
  19 set(CVC4_SOVERSION 5)
  20
  21 # Full release string for CVC4.
  22 if(CVC4_RELEASE)
  23   set(CVC4_RELEASE_STRING
  24       "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
  25 else()
  26   set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}")
  27 endif()
  28
  29 # Define to the full name of this package.
  30 set(PACKAGE_NAME "${PROJECT_NAME}")
  31
  32 #### These defines are only use in autotools make files, will likely be
  33 #### replaced with corresponding CPack stuff
  34 ## Define to the full name and version of this package.
  35 #set(PACKAGE_STRING "${PROJECT_NAME} ${CVC4_RELEASE_STRING}")
  36 ## Define to the one symbol short name of this package.
  37 #set(PACKAGE_TARNAME "${PROJECT_NAME}")
  38 ## Define to the home page for this package.
  39 #set(PACKAGE_URL "")
  40 ## Define to the version of this package.
  41 #set(PACKAGE_VERSION "${CVC4_RELEASE_STRING}")
  42 ## Define to the address where bug reports for this package should be sent.
  43 #set(PACKAGE_BUGREPORT "cvc4-bugs@cs.stanford.edu")
  44
  45 #-----------------------------------------------------------------------------#
  46
  47 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
  48 set(CMAKE_C_STANDARD 99)
  49 set(CMAKE_CXX_STANDARD 11)
  50
  51 #-----------------------------------------------------------------------------#
  52 # Macros
  53
  54 include(CheckCCompilerFlag)
  55 include(CheckCXXCompilerFlag)
  56
  57 macro(add_c_flag flag)
  58   if(CMAKE_C_FLAGS)
  59     set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
  60   else()
  61     set(CMAKE_C_FLAGS "${flag}")
  62   endif()
  63   message(STATUS "Configuring with C flag '${flag}'")
  64 endmacro()
  65
  66 macro(add_cxx_flag flag)
  67   if(CMAKE_CXX_FLAGS)
  68     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
  69   else()
  70     set(CMAKE_CXX_FLAGS "${flag}")
  71   endif()
  72   message(STATUS "Configuring with CXX flag '${flag}'")
  73 endmacro()
  74
  75 macro(add_c_cxx_flag flag)
  76   add_c_flag(${flag})
  77   add_cxx_flag(${flag})
  78 endmacro()
  79
  80 macro(add_check_c_flag flag)
  81   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
  82   check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
  83   if(HAVE_FLAG${flagname})
  84     add_c_flag(${flag})
  85   endif()
  86 endmacro()
  87
  88 macro(add_check_cxx_flag flag)
  89   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
  90   check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
  91   if(HAVE_FLAG${flagname})
  92     add_cxx_flag(${flag})
  93   endif()
  94 endmacro()
  95
  96 macro(add_check_c_cxx_flag flag)
  97   add_check_c_flag(${flag})
  98   add_check_cxx_flag(${flag})
  99 endmacro()
 100
 101 macro(add_required_cxx_flag flag)
 102   string(REGEX REPLACE "[-=]" "_" flagnamename ${flag})
 103   check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
 104   if (NOT HAVE_FLAG${flagname})
 105     message(FATAL_ERROR "Required compiler flag ${flag} not supported")
 106   endif()
 107   add_cxx_flag(${flag})
 108 endmacro()
 109
 110 macro(add_required_c_flag flag)
 111   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
 112   check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
 113   if (NOT HAVE_FLAG${flagname})
 114     message(FATAL_ERROR "Required compiler flag ${flag} not supported")
 115   endif()
 116   add_c_flag(${flag})
 117 endmacro()
 118
 119 macro(add_required_c_cxx_flag flag)
 120   add_required_c_flag(${flag})
 121   add_required_cxx_flag(${flag})
 122 endmacro()
 123
 124 # CVC4 Boolean options are three-valued to detect if an option was set by the
 125 # user. The available values are: IGNORE (default), ON, OFF
 126 # Default options do not override options that were set by the user, i.e.,
 127 # cvc4_set_option only sets an option if it's value is still IGNORE.
 128 # This e.g., allows the user to disable proofs for debug builds (where proofs
 129 # are enabled by default).
 130 macro(cvc4_option var description)
 131   set(${var} IGNORE CACHE STRING "${description}")
 132   # Provide drop down menu options in cmake-gui
 133   set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF)
 134 endmacro()
 135
 136 # Only set option if the user did not set an option.
 137 macro(cvc4_set_option var value)
 138   if(${var} STREQUAL "IGNORE")
 139     set(${var} ${value})
 140   endif()
 141 endmacro()
 142
 143 # Prepend 'prepand_value' to each element of the list 'in_list'. The result
 144 # is stored in 'out_list'.
 145 function(list_prepend in_list prepand_value out_list)
 146   foreach(_elem ${${in_list}})
 147     list(APPEND ${out_list} "${prepand_value}${_elem}")
 148   endforeach()
 149   set(${out_list} ${${out_list}} PARENT_SCOPE)
 150 endfunction()
 151
 152 #-----------------------------------------------------------------------------#
 153 # libcvc4 macros
 154
 155 # Collect all libraries that must be linked against libcvc4. These will be
 156 # actually linked in src/CMakeLists.txt with target_link_libaries(...).
 157 macro(libcvc4_link_libraries library)
 158   set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library})
 159 endmacro()
 160
 161 # Collect all include directories that are required for libcvc4. These will be
 162 # actually included in src/CMakeLists.txt with target_include_directories(...).
 163 macro(libcvc4_include_directories dirs)
 164   set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs})
 165 endmacro()
 166
 167 # Collect all source files that are required to build libcvc4 in LIBCVC4_SRCS
 168 # or LIBCVC4_GEN_SRCS. If GENERATED is the first argument the sources are
 169 # added to LIBCVC4_GEN_SRCS. All sources are prepended with the absolute
 170 # current path path. CMAKE_CURRENT_BINARY_DIR is prepended
 171 # to generated source files.
 172 macro(libcvc4_add_sources)
 173   set(_sources ${ARGV})
 174
 175   # Check if the first argument is GENERATED.
 176   list(GET _sources 0 _generated)
 177   if(${_generated} STREQUAL "GENERATED")
 178     list(REMOVE_AT _sources 0)
 179     set(_cur_path ${CMAKE_CURRENT_BINARY_DIR})
 180     set(_append_to LIBCVC4_GEN_SRCS)
 181   else()
 182     set(_cur_path ${CMAKE_CURRENT_SOURCE_DIR})
 183     set(_append_to LIBCVC4_SRCS)
 184   endif()
 185
 186   # Prepend source files with current path.
 187   foreach(_src ${_sources})
 188     list(APPEND ${_append_to} "${_cur_path}/${_src}")
 189   endforeach()
 190
 191   file(RELATIVE_PATH
 192        _rel_path "${PROJECT_SOURCE_DIR}/src" "${CMAKE_CURRENT_SOURCE_DIR}")
 193
 194   # Make changes to list ${_append_to} visible to the parent scope if not
 195   # called from src/.
 196   # Note: ${_append_to} refers to the variable name whereas ${${_append_to}}
 197   # refers to the contents of the variable.
 198   if(_rel_path)
 199     set(${_append_to} ${${_append_to}} PARENT_SCOPE)
 200   endif()
 201 endmacro()
 202
 203 #-----------------------------------------------------------------------------#
 204 # User options
 205
 206 # License
 207 option(ENABLE_GPL "Enable GPL dependencies")
 208
 209 # General build options
 210 #
 211 # >> 3-valued: INGORE ON OFF
 212 #    > allows to detect if set by user (default: IGNORE)
 213 #    > only necessary for options set for build types
 214 cvc4_option(ENABLE_ASAN          "Enable ASAN build")
 215 cvc4_option(ENABLE_ASSERTIONS    "Enable assertions")
 216 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
 217 cvc4_option(ENABLE_DUMPING       "Enable dumping")
 218 cvc4_option(ENABLE_MUZZLE        "Suppress ALL non-result output")
 219 cvc4_option(ENABLE_OPTIMIZED     "Enable optimization")
 220 cvc4_option(ENABLE_PORTFOLIO     "Enable portfolio support")
 221 cvc4_option(ENABLE_PROOFS        "Enable proof support")
 222 cvc4_option(ENABLE_REPLAY        "Enable the replay feature")
 223 cvc4_option(ENABLE_STATISTICS    "Enable statistics")
 224 cvc4_option(ENABLE_TRACING       "Enable tracing")
 225 cvc4_option(ENABLE_UNIT_TESTING  "Enable unit testing")
 226 cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
 227 cvc4_option(ENABLE_SHARED        "Build as shared library")
 228 # >> 2-valued: ON OFF
 229 #    > for options where we don't need to detect if set by user (default: OFF)
 230 option(ENABLE_BEST             "Enable dependencies known to give best performance")
 231 option(ENABLE_COVERAGE         "Enable support for gcov coverage testing")
 232 option(ENABLE_DEBUG_CONTEXT_MM "Enable the debug context memory manager")
 233 option(ENABLE_PROFILING        "Enable support for gprof profiling")
 234
 235 # Optional dependencies
 236 #
 237 # >> 3-valued: INGORE ON OFF
 238 #    > allows to detect if set by user (default: IGNORE)
 239 #    > only necessary for options set for ENABLE_BEST
 240 cvc4_option(USE_ABC      "Use ABC for AIG bit-blasting")
 241 cvc4_option(USE_CLN      "Use CLN instead of GMP")
 242 cvc4_option(USE_GLPK     "Use GLPK simplex solver")
 243 cvc4_option(USE_READLINE "Use readline for better interactive support")
 244 # >> 2-valued: ON OFF
 245 #    > for options where we don't need to detect if set by user (default: OFF)
 246 option(USE_CADICAL       "Use CaDiCaL SAT solver")
 247 option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
 248 option(USE_LFSC          "Use LFSC proof checker")
 249 option(USE_SYMFPU        "Use SymFPU for floating point support")
 250 option(USE_PYTHON2       "Prefer using Python 2 (for Python bindings)")
 251
 252 # Custom install directories for dependencies
 253 # If no directory is provided by the user, we first check if the dependency was
 254 # installed via the corresponding contrib/get-* script and if not found, we
 255 # check the intalled system version. If the user provides a directory we
 256 # immediately fail if the dependency was not found at the specified location.
 257 set(ABC_DIR           "" CACHE STRING "Set ABC install directory")
 258 set(ANTLR_DIR         "" CACHE STRING "Set ANTLR3 install directory")
 259 set(CADICAL_DIR       "" CACHE STRING "Set CaDiCaL install directory")
 260 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
 261 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 262 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
 263 set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
 264 set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 265
 266 # Supported language bindings
 267 option(BUILD_BINDINGS_JAVA   "Build Java bindings")
 268 option(BUILD_BINDINGS_PYTHON "Build Python bindings")
 269
 270 #-----------------------------------------------------------------------------#
 271 # Internal cmake variables
 272
 273 set(OPTIMIZATION_LEVEL 3)
 274 set(GPL_LIBS "")
 275
 276 set(BUILD_TYPES Production Debug Testing Competition)
 277
 278 #-----------------------------------------------------------------------------#
 279 # CVC4 build variables
 280
 281 set(CVC4_DEBUG 0)
 282 set(CVC4_BUILD_PROFILE_PRODUCTION 0)
 283 set(CVC4_BUILD_PROFILE_DEBUG 0)
 284 set(CVC4_BUILD_PROFILE_TESTING 0)
 285 set(CVC4_BUILD_PROFILE_COMPETITION 0)
 286
 287 #-----------------------------------------------------------------------------#
 288 # Build types
 289
 290 if(ENABLE_ASAN)
 291   set(CMAKE_BUILD_TYPE Debug)
 292 endif()
 293
 294 # Set the default build type to Production
 295 if(NOT CMAKE_BUILD_TYPE)
 296   set(CMAKE_BUILD_TYPE
 297       Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
 298   # Provide drop down menu options in cmake-gui
 299   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 300 endif()
 301 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 302
 303 if(CMAKE_BUILD_TYPE STREQUAL "Debug")
 304   include(ConfigDebug)
 305 elseif(CMAKE_BUILD_TYPE STREQUAL "Production")
 306   include(ConfigProduction)
 307 elseif(CMAKE_BUILD_TYPE STREQUAL "Testing")
 308   include(ConfigTesting)
 309 elseif(CMAKE_BUILD_TYPE STREQUAL "Competition")
 310   include(ConfigCompetition)
 311 endif()
 312
 313 #-----------------------------------------------------------------------------#
 314 # Compiler flags
 315
 316 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
 317 add_check_c_flag("-fexceptions")
 318 add_check_c_cxx_flag("-Wno-deprecated")
 319 add_check_cxx_flag("-Wsuggest-override")
 320 add_check_cxx_flag("-Wnon-virtual-dtor")
 321
 322 #-----------------------------------------------------------------------------#
 323 # Option defaults (three-valued options (cvc4_option(...)))
 324
 325 cvc4_set_option(ENABLE_PORTFOLIO OFF)
 326 cvc4_set_option(ENABLE_SHARED ON)
 327 cvc4_set_option(ENABLE_VALGRIND OFF)
 328 cvc4_set_option(USE_ABC OFF)
 329 cvc4_set_option(USE_GLPK OFF)
 330 cvc4_set_option(USE_READLINE OFF)
 331
 332 #-----------------------------------------------------------------------------#
 333 # Set options for best configuration
 334
 335 if (ENABLE_BEST)
 336   cvc4_set_option(USE_ABC ON)
 337   cvc4_set_option(USE_CLN ON)
 338   cvc4_set_option(USE_GLPK ON)
 339   cvc4_set_option(USE_READLINE ON)
 340 endif()
 341
 342 #-----------------------------------------------------------------------------#
 343
 344 # This needs to be set before any find_package(...) command since we want to
 345 # search for static libraries with suffix .a.
 346 if(NOT ENABLE_SHARED)
 347   set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
 348   set(CMAKE_EXE_LINKER_FLAGS "-static")
 349   set(BUILD_SHARED_LIBS OFF)
 350 endif()
 351
 352 #-----------------------------------------------------------------------------#
 353 # Enable the ctest testing framework
 354
 355 # This needs to be enabled here rather than in subdirectory test in order to
 356 # allow calling ctest from the root build directory.
 357 enable_testing()
 358
 359 #-----------------------------------------------------------------------------#
 360 # Check options, find packages and configure build.
 361
 362 if(USE_PYTHON2)
 363   find_package(PythonInterp 2.7 REQUIRED)
 364 else()
 365   find_package(PythonInterp 3)
 366   find_package(PythonInterp REQUIRED)
 367 endif()
 368
 369 set(GMP_HOME ${GMP_DIR})
 370 find_package(GMP REQUIRED)
 371 libcvc4_link_libraries(${GMP_LIBRARIES})
 372 libcvc4_include_directories(${GMP_INCLUDE_DIR})
 373
 374 if(ENABLE_ASAN)
 375   set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address)
 376   add_required_c_cxx_flag("-fsanitize=address")
 377   unset(CMAKE_REQUIRED_LIBRARIES)
 378   add_required_c_cxx_flag("-fno-omit-frame-pointer")
 379   add_check_c_cxx_flag("-fsanitize-recover=address")
 380 endif()
 381
 382 if(ENABLE_ASSERTIONS)
 383   add_definitions(-DCVC4_ASSERTIONS)
 384 else()
 385   add_definitions(-DNDEBUG)
 386 endif()
 387
 388 if(ENABLE_COVERAGE)
 389   include(CodeCoverage)
 390   APPEND_COVERAGE_COMPILER_FLAGS()
 391   add_definitions(-DCVC4_COVERAGE)
 392   setup_target_for_coverage_lcov(
 393     NAME coverage
 394     EXECUTABLE ctest $(ARGS)
 395     DEPENDENCIES cvc4-bin)
 396 endif()
 397
 398 if(ENABLE_DEBUG_CONTEXT_MM)
 399   add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
 400 endif()
 401
 402 if(ENABLE_DUMPING)
 403   add_definitions(-DCVC4_DUMPING)
 404 endif()
 405
 406 if(ENABLE_DEBUG_SYMBOLS)
 407   add_check_c_cxx_flag("-ggdb3")
 408 endif()
 409
 410 if(ENABLE_MUZZLE)
 411   add_definitions(-DCVC4_MUZZLE)
 412 endif()
 413
 414 if(ENABLE_PORTFOLIO)
 415   find_package(Boost 1.50.0 REQUIRED COMPONENTS thread)
 416   # Disable CLN for portfolio builds since it is not thread safe (uses an
 417   # unlocked hash table internally).
 418   if(USE_CLN)
 419     message(WARNING "Disabling CLN support since portfolio is enabled.")
 420     set(USE_CLN OFF)
 421   endif()
 422   set(THREADS_PREFER_PTHREAD_FLAG ON)
 423   find_package(Threads REQUIRED)
 424   if(THREADS_HAVE_PTHREAD_ARG)
 425     add_c_cxx_flag(-pthread)
 426   endif()
 427   add_definitions(-DCVC4_PORTFOLIO)
 428   set(BOOST_HAS_THREAD_ATTR 1)
 429 endif()
 430
 431 if(ENABLE_PROFILING)
 432   add_definitions(-DCVC4_PROFILING)
 433   add_check_c_cxx_flag("-pg")
 434 endif()
 435
 436 if(ENABLE_PROOFS)
 437   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
 438   add_definitions(-DCVC4_PROOF)
 439   set(CVC4_PROOF 1)
 440 endif()
 441
 442 if(ENABLE_REPLAY)
 443   add_definitions(-DCVC4_REPLAY)
 444 endif()
 445
 446 if(ENABLE_TRACING)
 447   add_definitions(-DCVC4_TRACING)
 448   set(CVC4_TRACING 1)
 449 endif()
 450
 451 if(ENABLE_UNIT_TESTING)
 452         find_package(CxxTest REQUIRED)
 453   # Force shared libs for unit tests, static libs with unit tests are not
 454   # working right now.
 455   set(ENABLE_SHARED ON)
 456 endif()
 457
 458 if(ENABLE_SHARED)
 459   set(BUILD_SHARED_LIBS ON)
 460 endif()
 461
 462 if(ENABLE_STATISTICS)
 463   add_definitions(-DCVC4_STATISTICS_ON)
 464 endif()
 465
 466 if(ENABLE_VALGRIND)
 467   find_package(Valgrind REQUIRED)
 468   libcvc4_include_directories(${Valgrind_INCLUDE_DIR})
 469   add_definitions(-DCVC4_VALGRIND)
 470 endif()
 471
 472 if(USE_ABC)
 473   set(ABC_HOME "${ABC_DIR}")
 474   find_package(ABC REQUIRED)
 475   libcvc4_link_libraries(${ABC_LIBRARIES})
 476   libcvc4_include_directories(${ABC_INCLUDE_DIR})
 477   add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
 478 endif()
 479
 480 if(USE_CADICAL)
 481   set(CaDiCaL_HOME ${CADICAL_DIR})
 482   find_package(CaDiCaL REQUIRED)
 483   libcvc4_link_libraries(${CaDiCaL_LIBRARIES})
 484   libcvc4_include_directories(${CaDiCaL_INCLUDE_DIR})
 485   add_definitions(-DCVC4_USE_CADICAL)
 486 endif()
 487
 488 if(USE_CLN)
 489   set(GPL_LIBS "${GPL_LIBS} cln")
 490   find_package(CLN 1.2.2 REQUIRED)
 491   libcvc4_link_libraries(${CLN_LIBRARIES})
 492   libcvc4_include_directories(${CLN_INCLUDE_DIR})
 493   set(CVC4_USE_CLN_IMP 1)
 494   set(CVC4_USE_GMP_IMP 0)
 495 else()
 496   set(CVC4_USE_CLN_IMP 0)
 497   set(CVC4_USE_GMP_IMP 1)
 498 endif()
 499
 500 if(USE_CRYPTOMINISAT)
 501   # CryptoMiniSat requires pthreads support
 502   set(THREADS_PREFER_PTHREAD_FLAG ON)
 503   find_package(Threads REQUIRED)
 504   if(THREADS_HAVE_PTHREAD_ARG)
 505     add_c_cxx_flag(-pthread)
 506   endif()
 507   set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
 508   find_package(CryptoMiniSat REQUIRED)
 509   libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES})
 510   libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR})
 511   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 512 endif()
 513
 514 if(USE_GLPK)
 515   set(GPL_LIBS "${GPL_LIBS} glpk")
 516   set(GLPK_HOME ${GLPK_DIR})
 517   find_package(GLPK REQUIRED)
 518   libcvc4_link_libraries(${GLPK_LIBRARIES})
 519   libcvc4_include_directories(${GLPK_INCLUDE_DIR})
 520   add_definitions(-DCVC4_USE_GLPK)
 521 endif()
 522
 523 if(USE_LFSC)
 524   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
 525   set(LFSC_HOME ${LFSC_DIR})
 526   find_package(LFSC REQUIRED)
 527   libcvc4_link_libraries(${LFSC_LIBRARIES})
 528   libcvc4_include_directories(${LFSC_INCLUDE_DIR})
 529   add_definitions(-DCVC4_USE_LFSC)
 530   set(CVC4_USE_LFSC 1)
 531 else()
 532   set(CVC4_USE_LFSC 0)
 533 endif()
 534
 535 if(USE_READLINE)
 536   find_package(Readline REQUIRED)
 537   set(HAVE_LIBREADLINE 1)
 538   if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 539     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 540   endif()
 541 endif()
 542
 543 if(USE_SYMFPU)
 544   set(SymFPU_HOME ${SYMFPU_DIR})
 545   find_package(SymFPU REQUIRED)
 546   libcvc4_include_directories(${SymFPU_INCLUDE_DIR})
 547   add_definitions(-DCVC4_USE_SYMFPU)
 548   set(CVC4_USE_SYMFPU 1)
 549 else()
 550   set(CVC4_USE_SYMFPU 0)
 551 endif()
 552
 553 if(GPL_LIBS)
 554   if(NOT ENABLE_GPL)
 555     message(FATAL_ERROR
 556       "Bad configuration detected: BSD-licensed code only, but also requested "
 557       "GPLed libraries: ${GPL_LIBS}")
 558   endif()
 559   set(CVC4_GPL_DEPS 1)
 560 endif()
 561
 562 #-----------------------------------------------------------------------------#
 563
 564 include(GetGitRevisionDescription)
 565 get_git_head_revision(GIT_REFSPEC GIT_SHA1)
 566 git_local_changes(GIT_IS_DIRTY)
 567 if(${GIT_IS_DIRTY} STREQUAL "DIRTY")
 568   set(GIT_IS_DIRTY "true")
 569 else()
 570   set(GIT_IS_DIRTY "false")
 571 endif()
 572
 573 execute_process(
 574   COMMAND "${GIT_EXECUTABLE}" rev-parse --abbrev-ref HEAD
 575   OUTPUT_VARIABLE GIT_BRANCH
 576   OUTPUT_STRIP_TRAILING_WHITESPACE
 577 )
 578
 579 #-----------------------------------------------------------------------------#
 580 # Generate CVC4's cvc4autoconfig.h header
 581
 582 include(ConfigureCVC4)
 583 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
 584 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 585
 586 #-----------------------------------------------------------------------------#
 587 # Add subdirectories
 588
 589 # signatures needs to come before src since it adds source files to libcvc4.
 590 if(ENABLE_PROOFS)
 591   add_subdirectory(proofs/signatures)
 592 endif()
 593
 594 add_subdirectory(doc)
 595 add_subdirectory(src)
 596 add_subdirectory(test)
 597
 598 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
 599   add_subdirectory(src/bindings)
 600 endif()
 601
 602 #-----------------------------------------------------------------------------#
 603 # Print build configuration
 604
 605 if(CVC4_BUILD_PROFILE_PRODUCTION)
 606   set(CVC4_BUILD_PROFILE_STRING "production")
 607 elseif(CVC4_BUILD_PROFILE_DEBUG)
 608   set(CVC4_BUILD_PROFILE_STRING "debug")
 609 elseif(CVC4_BUILD_PROFILE_TESTING)
 610   set(CVC4_BUILD_PROFILE_STRING "testing")
 611 elseif(CVC4_BUILD_PROFILE_COMPETITION)
 612   set(CVC4_BUILD_PROFILE_STRING "competition")
 613 endif()
 614
 615 # Get all definitions added via add_definitions to print it below
 616 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
 617 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
 618
 619 # Print configuration of 2-valued or 3-valued option 'var' with prefix 'str'
 620 macro(print_config str var)
 621   if(${var} STREQUAL "ON")
 622     set(OPT_VAL_STR "on")
 623   elseif(${var} STREQUAL "OFF")
 624     set(OPT_VAL_STR "off")
 625   elseif(${var} STREQUAL "IGNORE")
 626     set(OPT_VAL_STR "default")
 627   endif()
 628   message("${str} ${OPT_VAL_STR}")
 629 endmacro()
 630
 631 message("CVC4 ${CVC4_RELEASE_STRING}")
 632 message("")
 633 message("Build profile        : ${CVC4_BUILD_PROFILE_STRING}")
 634 message("")
 635 print_config("GPL                  :" ENABLE_GPL)
 636 print_config("Best configuration   :" ENABLE_BEST)
 637 print_config("Optimized            :" ENABLE_OPTIMIZED)
 638 print_config("Optimization level   :" OPTIMIZATION_LEVEL)
 639 message("")
 640 print_config("Assertions           :" ENABLE_ASSERTIONS)
 641 print_config("Debug symbols        :" ENABLE_DEBUG_SYMBOLS)
 642 print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
 643 message("")
 644 print_config("Dumping              :" ENABLE_DUMPING)
 645 print_config("Muzzle               :" ENABLE_MUZZLE)
 646 print_config("Proofs               :" ENABLE_PROOFS)
 647 print_config("Replay               :" ENABLE_REPLAY)
 648 print_config("Statistics           :" ENABLE_STATISTICS)
 649 print_config("Tracing              :" ENABLE_TRACING)
 650 message("")
 651 print_config("Asan                 :" ENABLE_ASAN)
 652 print_config("Coverage (gcov)      :" ENABLE_COVERAGE)
 653 print_config("Profiling (gprof)    :" ENABLE_PROFILING)
 654 print_config("Unit tests           :" ENABLE_UNIT_TESTING)
 655 print_config("Valgrind             :" ENABLE_VALGRIND)
 656 message("")
 657 print_config("Shared libs          :" ENABLE_SHARED)
 658 print_config("Java bindings        :" BUILD_BINDINGS_JAVA)
 659 print_config("Python bindings      :" BUILD_BINDINGS_PYTHON)
 660 message("")
 661 print_config("Portfolio            :" ENABLE_PORTFOLIO)
 662 message("")
 663 print_config("ABC                  :" USE_ABC)
 664 print_config("CaDiCaL              :" USE_CADICAL)
 665 print_config("CryptoMiniSat        :" USE_CRYPTOMINISAT)
 666 print_config("GLPK                 :" USE_GLPK)
 667 print_config("LFSC                 :" USE_LFSC)
 668
 669 if(CVC4_USE_CLN_IMP)
 670   message("MP library           : cln")
 671 else()
 672   message("MP library           : gmp")
 673 endif()
 674 print_config("Readline             :" ${USE_READLINE})
 675 print_config("SymFPU               :" ${USE_SYMFPU})
 676 message("")
 677 if(ABC_DIR)
 678   message("ABC dir              : ${ABC_DIR}")
 679 endif()
 680 if(ANTLR_DIR)
 681   message("ANTLR dir            : ${ANTLR_DIR}")
 682 endif()
 683 if(CADICAL_DIR)
 684   message("CADICAL dir          : ${CADICAL_DIR}")
 685 endif()
 686 if(CRYPTOMINISAT_DIR)
 687   message("CRYPTOMINISAT dir    : ${CRYPTOMINISAT_DIR}")
 688 endif()
 689 if(GLPK_DIR)
 690   message("GLPK dir             : ${GLPK_DIR}")
 691 endif()
 692 if(GMP_DIR)
 693   message("GMP dir              : ${GMP_DIR}")
 694 endif()
 695 if(LFSC_DIR)
 696   message("LFSC dir             : ${LFSC_DIR}")
 697 endif()
 698 if(SYMFPU_DIR)
 699   message("SYMFPU dir           : ${SYMFPU_DIR}")
 700 endif()
 701 message("")
 702 message("CPPLAGS (-D...)      : ${CVC4_DEFINITIONS}")
 703 message("CXXFLAGS             : ${CMAKE_CXX_FLAGS}")
 704 message("CFLAGS               : ${CMAKE_C_FLAGS}")
 705 #message("LIBS         : ${LIBS}")
 706 #message("LDFLAGS      : ${LDFLAGS}")
 707 #message("")
 708 #message("libcvc4 version        : ${{CVC4_LIBRARY_VERSION}")
 709 #message("libcvc4parser version  : ${CVC4_PARSER_LIBRARY_VERSION}")
 710 #message("libcvc4compat version  : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}")
 711 #message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}")
 712 #message("")
 713 message("Install prefix       : ${CMAKE_INSTALL_PREFIX}")
 714 message("")
 715
 716 if(GPL_LIBS)
 717   message(
 718   "CVC4 license         : GPLv3 (due to optional libraries; see below)"
 719   "\n"
 720   "\n"
 721   "Please note that CVC4 will be built against the following GPLed libraries:"
 722   "\n"
 723   "${GPL_LIBS}"
 724   "\n"
 725   "As these libraries are covered under the GPLv3, so is this build of CVC4."
 726   "\n"
 727   "CVC4 is also available to you under the terms of the (modified) BSD license."
 728   "\n"
 729   "If you prefer to license CVC4 under those terms, please configure CVC4 to"
 730   "\n"
 731   "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
 732   )
 733 else()
 734   message(
 735   "CVC4 license         : modified BSD"
 736   "\n"
 737   "\n"
 738   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 739   "\n"
 740   "it is covered by the (modified) BSD license.  This is, however, not the best"
 741   "\n"
 742   "performing configuration of CVC4.  To build against GPL'ed libraries which"
 743   "\n"
 744   "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 745   )
 746 endif()
 747
 748 message("")
 749 message("Now just type make, followed by make check or make install.")
 750 message("")