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   if(CMAKE_C_FLAGS)
  53     set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
  54   else()
  55     set(CMAKE_C_FLAGS "${flag}")
  56   endif()
  57   message(STATUS "Configuring with C flag '${flag}'")
  58 endmacro()
  59
  60 macro(add_cxx_flag flag)
  61   if(CMAKE_CXX_FLAGS)
  62     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
  63   else()
  64     set(CMAKE_CXX_FLAGS "${flag}")
  65   endif()
  66   message(STATUS "Configuring with CXX flag '${flag}'")
  67 endmacro()
  68
  69 macro(add_c_cxx_flag flag)
  70   add_c_flag(${flag})
  71   add_cxx_flag(${flag})
  72 endmacro()
  73
  74 macro(add_check_c_flag flag)
  75   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
  76   check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
  77   if(HAVE_FLAG${flagname})
  78     add_c_flag(${flag})
  79   endif()
  80 endmacro()
  81
  82 macro(add_check_cxx_flag flag)
  83   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
  84   check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
  85   if(HAVE_FLAG${flagname})
  86     add_cxx_flag(${flag})
  87   endif()
  88 endmacro()
  89
  90 macro(add_check_c_cxx_flag flag)
  91   add_check_c_flag(${flag})
  92   add_check_cxx_flag(${flag})
  93 endmacro()
  94
  95 macro(add_required_cxx_flag flag)
  96   string(REGEX REPLACE "[-=]" "_" flagnamename ${flag})
  97   check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
  98   if (NOT HAVE_FLAG${flagname})
  99     message(FATAL_ERROR "Required compiler flag ${flag} not supported")
 100   endif()
 101   add_cxx_flag(${flag})
 102 endmacro()
 103
 104 macro(add_required_c_flag flag)
 105   string(REGEX REPLACE "[-=]" "_" flagname ${flag})
 106   check_c_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_c_flag(${flag})
 111 endmacro()
 112
 113 macro(add_required_c_cxx_flag flag)
 114   add_required_c_flag(${flag})
 115   add_required_cxx_flag(${flag})
 116 endmacro()
 117
 118 # Collect all libraries that must be linked against libcvc4. These will be
 119 # actually linked in src/CMakeLists.txt with target_link_libaries(...).
 120 macro(libcvc4_link_libraries library)
 121   set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library})
 122 endmacro()
 123
 124 # Collect all include directories that are required for libcvc4. These will be
 125 # actually included in src/CMakeLists.txt with target_include_directories(...).
 126 macro(libcvc4_include_directories dirs)
 127   set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs})
 128 endmacro()
 129
 130 # CVC4 Boolean options are three-valued to detect if an option was set by the
 131 # user. The available values are: IGNORE (default), ON, OFF
 132 # Default options do not override options that were set by the user, i.e.,
 133 # cvc4_set_option only sets an option if it's value is still IGNORE.
 134 # This e.g., allows the user to disable proofs for debug builds (where proofs
 135 # are enabled by default).
 136 macro(cvc4_option var description)
 137   set(${var} IGNORE CACHE STRING "${description}")
 138   # Provide drop down menu options in cmake-gui
 139   set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF)
 140 endmacro()
 141
 142 # Only set option if the user did not set an option.
 143 macro(cvc4_set_option var value)
 144   if(${var} STREQUAL "IGNORE")
 145     set(${var} ${value})
 146   endif()
 147 endmacro()
 148
 149 #-----------------------------------------------------------------------------#
 150 # User options
 151
 152 # License
 153 option(ENABLE_GPL                "Enable GPL dependencies" OFF)
 154
 155 # General build options
 156 # >> 3-valued: INGORE ON OFF, allows to detect if set by user
 157 #              this is only necessary for options set for build types!
 158 cvc4_option(ENABLE_ASAN          "Enable ASAN build")
 159 cvc4_option(ENABLE_ASSERTIONS    "Enable assertions")
 160 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
 161 cvc4_option(ENABLE_DUMPING       "Enable dumpin")
 162 cvc4_option(ENABLE_MUZZLE        "Enable silencing CVC4; supress ALL non-result output")
 163 cvc4_option(ENABLE_OPTIMIZED     "Enable optimization")
 164 cvc4_option(ENABLE_PORTFOLIO     "Enable portfolio support")
 165 cvc4_option(ENABLE_PROOFS        "Enable proof support")
 166 cvc4_option(ENABLE_REPLAY        "Enable the replay feature")
 167 cvc4_option(ENABLE_STATISTICS    "Enable statistics")
 168 cvc4_option(ENABLE_TRACING       "Enable tracing")
 169 cvc4_option(ENABLE_UNIT_TESTING  "Enable unit testing")
 170 cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
 171 cvc4_option(ENABLE_SHARED        "Build as shared library")
 172
 173 # >> 2-valued: ON OFF, for options where we don't need to detect if set by user
 174 option(ENABLE_COVERAGE           "Enable support for gcov coverage testing")
 175 option(ENABLE_PROFILING          "Enable support for gprof profiling")
 176
 177 # Optional dependencies
 178 option(USE_ABC                   "Use ABC for AIG bit-blasting")
 179 option(USE_CADICAL               "Use CaDiCaL SAT solver")
 180 option(USE_CLN                   "Use CLN instead of GMP")
 181 option(USE_CRYPTOMINISAT         "Use CryptoMiniSat SAT solver")
 182 option(USE_GLPK                  "Use GLPK simplex solver")
 183 option(USE_LFSC                  "Use LFSC proof checker")
 184 option(USE_READLINE              "Use readline for better interactive support")
 185 option(USE_SYMFPU                "Use SymFPU for floating point support")
 186
 187 # Custom install directories for dependencies
 188 # If no directory is provided by the user, we first check if the dependency was
 189 # installed via the corresponding contrib/get-* script and if not found, we
 190 # check the intalled system version. If the user provides a directory we
 191 # immediately fail if the dependency was not found at the specified location.
 192 set(ABC_DIR           "" CACHE STRING "Set ABC install directory")
 193 set(ANTLR_DIR         "" CACHE STRING "Set ANTLR3 install directory")
 194 set(CADICAL_DIR       "" CACHE STRING "Set CaDiCaL install directory")
 195 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
 196 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 197 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
 198 set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
 199 set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 200
 201 # Supported language bindings
 202 option(BUILD_BINDINGS_JAVA       "Build Java bindings" OFF)
 203 option(BUILD_BINDINGS_PYTHON     "Build Python bindings" OFF)
 204
 205 # All bindings: c,java,csharp,perl,php,python,ruby,tcl,ocaml
 206
 207
 208 #-----------------------------------------------------------------------------#
 209 # Internal cmake variables
 210
 211 set(OPT_LEVEL 3)
 212 set(GPL_LIBS "")
 213
 214 set(BUILD_TYPES Production Debug Testing Competition)
 215
 216 #-----------------------------------------------------------------------------#
 217 # CVC4 build variables
 218
 219 set(CVC4_DEBUG 0)
 220 set(CVC4_BUILD_PROFILE_PRODUCTION 0)
 221 set(CVC4_BUILD_PROFILE_DEBUG 0)
 222 set(CVC4_BUILD_PROFILE_TESTING 0)
 223 set(CVC4_BUILD_PROFILE_COMPETITION 0)
 224 # Whether CVC4 is built with the (optional) GPLed library dependences.
 225 set(CVC4_GPL_DEPS 0)
 226
 227 #-----------------------------------------------------------------------------#
 228 # Compiler flags
 229
 230 add_check_c_cxx_flag("-O${OPT_LEVEL}")
 231 add_check_c_flag("-fexceptions")
 232 add_check_c_cxx_flag("-Wno-deprecated")
 233 add_check_cxx_flag("-Wsuggest-override")
 234 add_check_cxx_flag("-Wnon-virtual-dtor")
 235
 236 #-----------------------------------------------------------------------------#
 237 # Build types
 238
 239 if(ENABLE_ASAN)
 240   set(CMAKE_BUILD_TYPE Debug)
 241 endif()
 242
 243 # Set the default build type to Production
 244 if(NOT CMAKE_BUILD_TYPE)
 245   set(CMAKE_BUILD_TYPE Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
 246   # Provide drop down menu options in cmake-gui
 247   set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 248 endif()
 249 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 250
 251 if(CMAKE_BUILD_TYPE STREQUAL "Debug")
 252   include(ConfigDebug)
 253 elseif(CMAKE_BUILD_TYPE STREQUAL "Production")
 254   include(ConfigProduction)
 255 elseif(CMAKE_BUILD_TYPE STREQUAL "Testing")
 256   include(ConfigTesting)
 257 elseif(CMAKE_BUILD_TYPE STREQUAL "Competition")
 258   include(ConfigCompetition)
 259   # enable_static=yes
 260   #TODO
 261   # enable_static_binary=yes
 262   #TODO
 263 endif()
 264
 265 #-----------------------------------------------------------------------------#
 266 # Option defaults (three-valued options (cvc4_option(...)))
 267
 268 cvc4_set_option(ENABLE_PORTFOLIO OFF)
 269 cvc4_set_option(ENABLE_SHARED ON)
 270 cvc4_set_option(ENABLE_VALGRIND OFF)
 271
 272 #-----------------------------------------------------------------------------#
 273
 274 # This needs to be set before any find_package(...) command since we want to
 275 # search for static libraries with suffix .a.
 276 if(NOT ENABLE_SHARED)
 277   set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
 278   set(CMAKE_EXE_LINKER_FLAGS "-static")
 279   set(BUILD_SHARED_LIBS OFF)
 280 endif()
 281
 282 find_package(PythonInterp REQUIRED)
 283
 284 set(ANTLR_HOME ${ANTLR_DIR})
 285 find_package(ANTLR REQUIRED)
 286
 287 set(GMP_HOME ${GMP_DIR})
 288 find_package(GMP REQUIRED)
 289 libcvc4_link_libraries(${GMP_LIBRARIES})
 290 libcvc4_include_directories(${GMP_INCLUDE_DIR})
 291
 292
 293 #-----------------------------------------------------------------------------#
 294 # Enable the ctest testing framework
 295
 296 enable_testing()
 297
 298 #-----------------------------------------------------------------------------#
 299
 300 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
 301   set(BUILD_BINDINGS TRUE)
 302 endif()
 303
 304 if(ENABLE_ASAN)
 305   set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address)
 306   add_required_c_cxx_flag("-fsanitize=address")
 307   unset(CMAKE_REQUIRED_LIBRARIES)
 308   add_required_c_cxx_flag("-fno-omit-frame-pointer")
 309   add_check_c_cxx_flag("-fsanitize-recover=address")
 310 endif()
 311
 312 if(ENABLE_ASSERTIONS)
 313   add_definitions(-DCVC4_ASSERTIONS)
 314 endif()
 315
 316 if(ENABLE_COVERAGE)
 317   include(CodeCoverage)
 318   APPEND_COVERAGE_COMPILER_FLAGS()
 319   add_definitions(-DCVC4_COVERAGE)
 320   setup_target_for_coverage_lcov(
 321     NAME coverage
 322     EXECUTABLE ctest $(ARGS)
 323     DEPENDENCIES cvc4-bin)
 324 endif()
 325
 326 if(ENABLE_DUMPING)
 327   add_definitions(-DCVC4_DUMPING)
 328 else()
 329   add_definitions(-DNDEBUG)
 330 endif()
 331
 332 if(ENABLE_DEBUG_SYMBOLS)
 333   add_check_c_cxx_flag("-ggdb3")
 334 endif()
 335
 336 if(ENABLE_MUZZLE)
 337   add_definitions(-DCVC4_MUZZLE)
 338 endif()
 339
 340 if(ENABLE_PORTFOLIO)
 341   find_package(Boost REQUIRED COMPONENTS thread)
 342   # Disable CLN for portfolio builds since it is not thread safe (uses an
 343   # unlocked hash table internally).
 344   set(USE_CLN OFF)
 345   set(THREADS_PREFER_PTHREAD_FLAG ON)
 346   find_package(Threads REQUIRED)
 347   if(THREADS_HAVE_PTHREAD_ARG)
 348     add_c_cxx_flag(-pthread)
 349   endif()
 350   add_definitions(-DCVC4_PORTFOLIO)
 351 endif()
 352
 353 if(ENABLE_PROFILING)
 354   add_definitions(-DCVC4_PROFILING)
 355   add_check_c_cxx_flag("-pg")
 356 endif()
 357
 358 if(ENABLE_PROOFS)
 359   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
 360   add_definitions(-DCVC4_PROOF)
 361   set(CVC4_PROOF 1)
 362   libcvc4_link_libraries(signatures)
 363 endif()
 364
 365 if(ENABLE_REPLAY)
 366   add_definitions(-DCVC4_REPLAY)
 367 endif()
 368
 369 if(ENABLE_TRACING)
 370   add_definitions(-DCVC4_TRACING)
 371   set(CVC4_TRACING 1)
 372 endif()
 373
 374 if(ENABLE_UNIT_TESTING)
 375         find_package(CxxTest REQUIRED)
 376   # Force shared libs for unit tests, static libs with unit tests are not
 377   # working right now.
 378   set(ENABLE_SHARED ON)
 379 endif()
 380
 381 if(ENABLE_SHARED)
 382   set(BUILD_SHARED_LIBS ON)
 383 endif()
 384
 385 if(ENABLE_STATISTICS)
 386   add_definitions(-DCVC4_STATISTICS_ON)
 387 endif()
 388
 389 if(ENABLE_VALGRIND)
 390   #TODO check if valgrind available
 391   add_definitions(-DCVC4_VALGRIND)
 392 endif()
 393
 394 if(USE_ABC)
 395   set(ABC_HOME "${ABC_DIR}")
 396   find_package(ABC REQUIRED)
 397   libcvc4_link_libraries(${ABC_LIBRARIES})
 398   libcvc4_include_directories(${ABC_INCLUDE_DIR})
 399   add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
 400 endif()
 401
 402 if(USE_CADICAL)
 403   set(CaDiCaL_HOME ${CADICAL_DIR})
 404   find_package(CaDiCaL REQUIRED)
 405   libcvc4_link_libraries(${CaDiCaL_LIBRARIES})
 406   libcvc4_include_directories(${CaDiCaL_INCLUDE_DIR})
 407   add_definitions(-DCVC4_USE_CADICAL)
 408 endif()
 409
 410 if(USE_CLN)
 411   set(GPL_LIBS "${GPL_LIBS} cln")
 412   find_package(CLN 1.2.2 REQUIRED)
 413   libcvc4_link_libraries(${CLN_LIBRARIES})
 414   libcvc4_include_directories(${CLN_INCLUDE_DIR})
 415   set(CVC4_USE_CLN_IMP 1)
 416   set(CVC4_USE_GMP_IMP 0)
 417 else()
 418   set(CVC4_USE_CLN_IMP 0)
 419   set(CVC4_USE_GMP_IMP 1)
 420 endif()
 421
 422 if(USE_CRYPTOMINISAT)
 423   # CryptoMiniSat requires pthreads support
 424   set(THREADS_PREFER_PTHREAD_FLAG ON)
 425   find_package(Threads REQUIRED)
 426   if(THREADS_HAVE_PTHREAD_ARG)
 427     add_c_cxx_flag(-pthread)
 428   endif()
 429   set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
 430   find_package(CryptoMiniSat REQUIRED)
 431   libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES})
 432   libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR})
 433   add_definitions(-DCVC4_USE_CRYPTOMINISAT)
 434 endif()
 435
 436 if(USE_GLPK)
 437   set(GPL_LIBS "${GPL_LIBS} glpk")
 438   set(GLPK_HOME ${GLPK_DIR})
 439   find_package(GLPK REQUIRED)
 440   libcvc4_link_libraries(${GLPK_LIBRARIES})
 441   libcvc4_include_directories(${GLPK_INCLUDE_DIR})
 442   add_definitions(-DCVC4_USE_GLPK)
 443 endif()
 444
 445 if(USE_LFSC)
 446   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
 447   set(LFSC_HOME ${LFSC_DIR})
 448   find_package(LFSC REQUIRED)
 449   libcvc4_link_libraries(${LFSC_LIBRARIES})
 450   libcvc4_include_directories(${LFSC_INCLUDE_DIR})
 451   add_definitions(-DCVC4_USE_LFSC)
 452   set(CVC4_USE_LFSC 1)
 453 else()
 454   set(CVC4_USE_LFSC 0)
 455 endif()
 456
 457 if(USE_READLINE)
 458   find_package(Readline REQUIRED)
 459   set(HAVE_LIBREADLINE 1)
 460   if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
 461     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
 462   else()
 463     set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 0)
 464   endif()
 465 else()
 466   set(HAVE_LIBREADLINE 0)
 467 endif()
 468
 469 if(USE_SYMFPU)
 470   set(SymFPU_HOME ${SYMFPU_DIR})
 471   find_package(SymFPU REQUIRED)
 472   libcvc4_include_directories(${SymFPU_INCLUDE_DIR})
 473   add_definitions(-DCVC4_USE_SYMFPU)
 474   set(CVC4_USE_SYMFPU 1)
 475 else()
 476   set(CVC4_USE_SYMFPU 0)
 477 endif()
 478
 479 if(GPL_LIBS)
 480   if(NOT ENABLE_GPL)
 481     message(FATAL_ERROR
 482       "Bad configuration detected: BSD-licensed code only, but also requested "
 483       "GPLed libraries: ${GPL_LIBS}")
 484   endif()
 485   set(CVC4_GPL_DEPS 1)
 486 endif()
 487
 488 #-----------------------------------------------------------------------------#
 489
 490 set(VERSION "1.6.0-prerelease")
 491 string(TIMESTAMP MAN_DATE "%Y-%m-%d")
 492
 493 #-----------------------------------------------------------------------------#
 494
 495 include(GetGitRevisionDescription)
 496 get_git_head_revision(GIT_REFSPEC GIT_SHA1)
 497 git_local_changes(GIT_IS_DIRTY)
 498 if(${GIT_IS_DIRTY} STREQUAL "DIRTY")
 499   set(GIT_IS_DIRTY "true")
 500 else()
 501   set(GIT_IS_DIRTY "false")
 502 endif()
 503
 504 execute_process(
 505   COMMAND "${GIT_EXECUTABLE}" rev-parse --abbrev-ref HEAD
 506   OUTPUT_VARIABLE GIT_BRANCH
 507   OUTPUT_STRIP_TRAILING_WHITESPACE
 508 )
 509
 510 #-----------------------------------------------------------------------------#
 511
 512 include(ConfigureCVC4)
 513
 514 # Define to 1 if Boost threading library has support for thread attributes
 515 set(BOOST_HAS_THREAD_ATTR 0)
 516 # Defined if using the CLN multi-precision arithmetic library.
 517 set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP})
 518 # Defined if using the GMP multi-precision arithmetic library.
 519 set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP})
 520 ## Defined if the requested minimum BOOST version is satisfied
 521 #set(HAVE_BOOST 1)
 522 ## Define to 1 if you have <boost/system/error_code.hpp>
 523 #set(HAVE_BOOST_SYSTEM_ERROR_CODE_HPP 1)
 524 ## Define to 1 if you have <boost/thread.hpp>
 525 #set(HAVE_BOOST_THREAD_HPP 1)
 526 # Defined to 1 if clock_gettime() is supported by the platform.
 527 set(HAVE_CLOCK_GETTIME 1)
 528 # define if the compiler supports basic C++11 syntax
 529 set(HAVE_CXX11 1)
 530 # Define to 1 if you have the declaration of `optreset', and to 0 if you don't.
 531 set(HAVE_DECL_OPTRESET 0)
 532 ## Define to 1 if you have the declaration of `strerror_r', and to 0 if you
 533 ## don't.
 534 #set(HAVE_DECL_STRERROR_R 1)
 535 ## Define to 1 if you have the <dlfcn.h> header file.
 536 #set(HAVE_DLFCN_H 1)
 537 # Define to 1 if you have the <ext/stdio_filebuf.h> header file.
 538 set(HAVE_EXT_STDIO_FILEBUF_H 1)
 539 # Defined to 1 if ffs() is supported by the platform.
 540 set(HAVE_FFS 1)
 541 # Define to 1 if you have the <getopt.h> header file.
 542 set(HAVE_GETOPT_H 1)
 543 ## Define to 1 if you have the <inttypes.h> header file.
 544 #set(HAVE_INTTYPES_H 1)
 545 ## Define to 1 if you have the `gmp' library (-lgmp).
 546 #set(HAVE_LIBGMP 1)
 547 ## Define to 1 if you have the `profiler' library (-lprofiler).
 548 #set(HAVE_LIBPROFILER 0)
 549 # Define to 1 to use libreadline
 550 #set(HAVE_LIBREADLINE 0)
 551 ## Define to 1 if you have the `tcmalloc' library (-ltcmalloc).
 552 #set(HAVE_LIBTCMALLOC 0)
 553 ## Define to 1 if you have the <memory.h> header file.
 554 #set(HAVE_MEMORY_H 1)
 555 # Defined to 1 if sigaltstack() is supported by the platform.
 556 set(HAVE_SIGALTSTACK 1)
 557 ## Define to 1 if you have the <stdint.h> header file.
 558 #set(HAVE_STDINT_H 1)
 559 ## Define to 1 if you have the <stdlib.h> header file.
 560 #set(HAVE_STDLIB_H 1)
 561 # Define to 1 if you have the `strerror_r' function.
 562 set(HAVE_STRERROR_R 1)
 563 ## Define to 1 if you have the <strings.h> header file.
 564 #set(HAVE_STRINGS_H 1)
 565 ## Define to 1 if you have the <string.h> header file.
 566 #set(HAVE_STRING_H 1)
 567 # Defined to 1 if strtok_r() is supported by the platform.
 568 set(HAVE_STRTOK_R 1)
 569 ## Define to 1 if you have the <sys/stat.h> header file.
 570 #set(HAVE_SYS_STAT_H 1)
 571 ## Define to 1 if you have the <sys/types.h> header file.
 572 #set(HAVE_SYS_TYPES_H 1)
 573 # Define to 1 if you have the <unistd.h> header file.
 574 set(HAVE_UNISTD_H 1)
 575 ## Define to the sub-directory where libtool stores uninstalled libraries.
 576 #set(LT_OBJDIR ".libs/")
 577 ## Define to 1 if you have the ANSI C header files.
 578 #set(STDC_HEADERS 1)
 579 # Define to 1 if strerror_r returns char *.
 580 set(STRERROR_R_CHAR_P 1)
 581
 582 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
 583 include_directories(${CMAKE_CURRENT_BINARY_DIR})
 584
 585 #-----------------------------------------------------------------------------#
 586
 587 add_subdirectory(doc)
 588 add_subdirectory(src)
 589 if(BUILD_BINDINGS)
 590   add_subdirectory(src/bindings)
 591 endif()
 592 if(BUILD_BINDINGS_JAVA)
 593   add_subdirectory(test/java)
 594 endif()
 595 add_subdirectory(test/regress)
 596 add_subdirectory(test/system)
 597 if(ENABLE_UNIT_TESTING)
 598         add_subdirectory(test/unit)
 599 endif()
 600
 601 if(ENABLE_PROOFS)
 602   add_subdirectory(proofs/signatures)
 603 endif()
 604
 605 #-----------------------------------------------------------------------------#
 606 # Print build configuration
 607
 608 if(CVC4_BUILD_PROFILE_PRODUCTION)
 609   set(CVC4_BUILD_PROFILE_STRING "production")
 610 elseif(CVC4_BUILD_PROFILE_DEBUG)
 611   set(CVC4_BUILD_PROFILE_STRING "debug")
 612 elseif(CVC4_BUILD_PROFILE_TESTING)
 613   set(CVC4_BUILD_PROFILE_STRING "testing")
 614 elseif(CVC4_BUILD_PROFILE_COMPETITION)
 615   set(CVC4_BUILD_PROFILE_STRING "competition")
 616 endif()
 617
 618 # Get all definitions added via add_definitions to print it below
 619 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
 620 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
 621
 622 message("CVC4 ${CVC4_RELEASE_STRING}")
 623 message("")
 624 message("Build profile     : ${CVC4_BUILD_PROFILE_STRING}")
 625 message("Optimized         : ${ENABLE_OPTIMIZED}")
 626 message("Optimization level: ${OPTIMIZATION_LEVEL}")
 627 message("Debug symbols     : ${ENABLE_DEBUG_SYMBOLS}")
 628 message("Proofs            : ${ENABLE_PROOFS}")
 629 message("Statistics        : ${ENABLE_STATISTICS}")
 630 message("Replay            : ${ENABLE_REPLAY}")
 631 message("Assertions        : ${ENABLE_ASSERTIONS}")
 632 message("Tracing           : ${ENABLE_TRACING}")
 633 message("Dumping           : ${ENABLE_DUMPING}")
 634 message("Muzzle            : ${ENABLE_MUZZLE}")
 635 message("")
 636 message("Unit tests        : ${ENABLE_UNIT_TESTING}")
 637 message("Coverage (gcov)   : ${ENABLE_COVERAGE}")
 638 message("Profiling (gprof) : ${ENABLE_PROFILING}")
 639 message("")
 640 message("Shared libs       : ${ENABLE_SHARED}")
 641 #message("Static binary: ${enable_static_binary}")
 642 #message("Compat lib   : ${CVC4_BUILD_LIBCOMPAT}")
 643 #message("Bindings     : ${bindings_to_be_built}")
 644 #message("")
 645 #message("Multithreaded: ${support_multithreaded}")
 646 message("Portfolio         : ${ENABLE_PORTFOLIO}")
 647 message("")
 648 message("ABC               : ${USE_ABC}")
 649 message("CaDiCaL           : ${USE_CADICAL}")
 650 message("CryptoMiniSat     : ${USE_CRYPTOMINISAT}")
 651 message("GLPK              : ${USE_GLPK}")
 652 message("LFSC              : ${USE_LFSC}")
 653 if(CVC4_USE_CLN_IMP)
 654   message("MP library        : cln")
 655 else()
 656   message("MP library        : gmp")
 657 endif()
 658 message("Readline          : ${USE_READLINE}")
 659 message("SymFPU            : ${USE_SYMFPU}")
 660 message("")
 661 message("CPPLAGS (-D...)   : ${CVC4_DEFINITIONS}")
 662 message("CXXFLAGS          : ${CMAKE_CXX_FLAGS}")
 663 message("CFLAGS            : ${CMAKE_C_FLAGS}")
 664 #message("LIBS         : ${LIBS}")
 665 #message("LDFLAGS      : ${LDFLAGS}")
 666 #message("")
 667 #message("libcvc4 version        : ${{CVC4_LIBRARY_VERSION}")
 668 #message("libcvc4parser version  : ${CVC4_PARSER_LIBRARY_VERSION}")
 669 #message("libcvc4compat version  : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}")
 670 #message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}")
 671 #message("")
 672 message("Install prefix    : ${CMAKE_INSTALL_PREFIX}")
 673 message("")
 674
 675 if(GPL_LIBS)
 676   message(
 677   "CVC4 license      : GPLv3 (due to optional libraries; see below)"
 678   "\n"
 679   "\n"
 680   "Please note that CVC4 will be built against the following GPLed libraries:"
 681   "\n"
 682   "${GPL_LIBS}"
 683   "\n"
 684   "As these libraries are covered under the GPLv3, so is this build of CVC4."
 685   "\n"
 686   "CVC4 is also available to you under the terms of the (modified) BSD license."
 687   "\n"
 688   "If you prefer to license CVC4 under those terms, please configure CVC4 to"
 689   "\n"
 690   "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
 691   )
 692 else()
 693   message(
 694   "CVC4 license      : modified BSD"
 695   "\n"
 696   "\n"
 697   "Note that this configuration is NOT built against any GPL'ed libraries, so"
 698   "\n"
 699   "it is covered by the (modified) BSD license.  This is, however, not the best"
 700   "\n"
 701   "performing configuration of CVC4.  To build against GPL'ed libraries which"
 702   "\n"
 703   "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
 704   )
 705 endif()
 706
 707 message("")
 708 message("Now just type make, followed by make check or make install.")
 709 message("")