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