1 cmake_minimum_required(VERSION 3.1)
3 #-----------------------------------------------------------------------------#
4 # Project configuration
8 set(CVC4_MAJOR 1) # Major component of the version of CVC4.
9 set(CVC4_MINOR 7) # Minor component of the version of CVC4.
10 set(CVC4_RELEASE 0) # Release component of the version of CVC4.
12 # Extraversion component of the version of CVC4.
13 set(CVC4_EXTRAVERSION "")
15 # Shared library versioning. Increment SOVERSION for every new CVC4 release.
18 # Full release string for CVC4.
20 set(CVC4_RELEASE_STRING
21 "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
23 set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}")
26 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
27 set(CMAKE_C_STANDARD 99)
28 set(CMAKE_CXX_STANDARD 11)
30 # Generate compile_commands.json, which can be used for various code completion
32 set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
34 # Embed the installation prefix as an RPATH in the executable such that the
35 # linker can find our libraries (such as libcvc4parser) when executing the cvc4
36 # binary. This is for example useful when installing CVC4 with a custom prefix
37 # on macOS (e.g. when using homebrew in a non-standard directory). If we do not
38 # set this option, then the linker will not be able to find the required
39 # libraries when trying to run CVC4.
41 # More information on RPATH in CMake:
42 # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
43 set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib")
45 #-----------------------------------------------------------------------------#
49 #-----------------------------------------------------------------------------#
53 option(ENABLE_GPL "Enable GPL dependencies")
55 # General build options
57 # >> 3-valued: IGNORE ON OFF
58 # > allows to detect if set by user (default: IGNORE)
59 # > only necessary for options set for build types
60 cvc4_option(ENABLE_ASAN "Enable ASAN build")
61 cvc4_option(ENABLE_ASSERTIONS "Enable assertions")
62 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
63 cvc4_option(ENABLE_DUMPING "Enable dumping")
64 cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output")
65 cvc4_option(ENABLE_OPTIMIZED "Enable optimization")
66 cvc4_option(ENABLE_PORTFOLIO "Enable portfolio support")
67 cvc4_option(ENABLE_PROOFS "Enable proof support")
68 cvc4_option(ENABLE_REPLAY "Enable the replay feature")
69 cvc4_option(ENABLE_STATISTICS "Enable statistics")
70 cvc4_option(ENABLE_TRACING "Enable tracing")
71 cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing")
72 cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation")
73 cvc4_option(ENABLE_SHARED "Build as shared library")
74 cvc4_option(ENABLE_STATIC_BINARY
75 "Build static binaries with statically linked system libraries")
77 # > for options where we don't need to detect if set by user (default: OFF)
78 option(ENABLE_BEST "Enable dependencies known to give best performance")
79 option(ENABLE_COVERAGE "Enable support for gcov coverage testing")
80 option(ENABLE_DEBUG_CONTEXT_MM "Enable the debug context memory manager")
81 option(ENABLE_PROFILING "Enable support for gprof profiling")
83 # Optional dependencies
85 # >> 3-valued: IGNORE ON OFF
86 # > allows to detect if set by user (default: IGNORE)
87 # > only necessary for options set for ENABLE_BEST
88 cvc4_option(USE_ABC "Use ABC for AIG bit-blasting")
89 cvc4_option(USE_CLN "Use CLN instead of GMP")
90 cvc4_option(USE_GLPK "Use GLPK simplex solver")
91 cvc4_option(USE_READLINE "Use readline for better interactive support")
93 # > for options where we don't need to detect if set by user (default: OFF)
94 option(USE_CADICAL "Use CaDiCaL SAT solver")
95 option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
96 option(USE_DRAT2ER "Include drat2er for making eager BV proofs")
97 option(USE_LFSC "Use LFSC proof checker")
98 option(USE_SYMFPU "Use SymFPU for floating point support")
99 option(USE_PYTHON2 "Prefer using Python 2 (for Python bindings)")
100 option(USE_PYTHON3 "Prefer using Python 3 (for Python bindings)")
102 # Custom install directories for dependencies
103 # If no directory is provided by the user, we first check if the dependency was
104 # installed via the corresponding contrib/get-* script and if not found, we
105 # check the intalled system version. If the user provides a directory we
106 # immediately fail if the dependency was not found at the specified location.
107 set(ABC_DIR "" CACHE STRING "Set ABC install directory")
108 set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory")
109 set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory")
110 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
111 set(CXXTEST_DIR "" CACHE STRING "Set CxxTest install directory")
112 set(DRAT2ER_DIR "" CACHE STRING "Set drat2er install directory")
113 set(GLPK_DIR "" CACHE STRING "Set GLPK install directory")
114 set(GMP_DIR "" CACHE STRING "Set GMP install directory")
115 set(LFSC_DIR "" CACHE STRING "Set LFSC install directory")
116 set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory")
118 # Prepend binaries with prefix on make install
119 set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install")
121 # Supported language bindings
122 option(BUILD_BINDINGS_JAVA "Build Java bindings")
123 option(BUILD_BINDINGS_PYTHON "Build Python bindings")
125 #-----------------------------------------------------------------------------#
126 # Internal cmake variables
128 set(OPTIMIZATION_LEVEL 3)
131 #-----------------------------------------------------------------------------#
132 # Determine number of threads available, used to configure (default) parallel
133 # execution of custom test targets (can be overriden with ARGS=-jN).
135 include(ProcessorCount)
136 ProcessorCount(CTEST_NTHREADS)
137 if(CTEST_NTHREADS EQUAL 0)
138 set(CTEST_NTHREADS 1)
141 #-----------------------------------------------------------------------------#
144 # Note: Module CodeCoverage requires the name of the debug build to conform
145 # to cmake standards (first letter uppercase).
146 set(BUILD_TYPES Production Debug Testing Competition)
149 set(CMAKE_BUILD_TYPE Debug)
152 # Set the default build type to Production
153 if(NOT CMAKE_BUILD_TYPE)
155 Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
156 # Provide drop down menu options in cmake-gui
157 set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
160 # Check if specified build type is valid.
161 list(FIND BUILD_TYPES ${CMAKE_BUILD_TYPE} FOUND_BUILD_TYPE)
162 if(${FOUND_BUILD_TYPE} EQUAL -1)
164 "'${CMAKE_BUILD_TYPE}' is not a valid build type. "
165 "Available builds are: ${BUILD_TYPES}")
168 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
169 include(Config${CMAKE_BUILD_TYPE})
171 #-----------------------------------------------------------------------------#
174 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
175 add_check_c_cxx_flag("-Wall")
176 add_check_c_flag("-fexceptions")
177 add_check_c_cxx_flag("-Wno-deprecated")
178 add_check_cxx_flag("-Wsuggest-override")
179 add_check_cxx_flag("-Wnon-virtual-dtor")
181 # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
182 # cdlist.h warnings. Remove when fixed.
183 add_check_cxx_flag("-Wno-class-memaccess")
185 #-----------------------------------------------------------------------------#
186 # Option defaults (three-valued options (cvc4_option(...)))
188 # These options are only set if their value is IGNORE. Otherwise, the user
189 # already set the option, which we don't want to overwrite.
191 if(ENABLE_STATIC_BINARY)
192 cvc4_set_option(ENABLE_SHARED OFF)
194 cvc4_set_option(ENABLE_SHARED ON)
197 #-----------------------------------------------------------------------------#
198 # Set options for best configuration
201 cvc4_set_option(USE_ABC ON)
202 cvc4_set_option(USE_CADICAL ON)
203 cvc4_set_option(USE_CLN ON)
204 cvc4_set_option(USE_CRYPTOMINISAT ON)
205 cvc4_set_option(USE_GLPK ON)
206 cvc4_set_option(USE_READLINE ON)
209 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
210 # that expect AssertionException to be thrown will fail.
211 if(NOT ENABLE_ASSERTIONS)
212 set(ENABLE_UNIT_TESTING OFF)
215 #-----------------------------------------------------------------------------#
216 # Shared/static libraries
218 # This needs to be set before any find_package(...) command since we want to
219 # search for static libraries with suffix .a.
222 set(BUILD_SHARED_LIBS ON)
223 if(ENABLE_STATIC_BINARY)
224 set(ENABLE_STATIC_BINARY OFF)
225 message(WARNING "Disabling static binary since shared build is enabled.")
228 set(CMAKE_FIND_LIBRARY_SUFFIXES .a ${CMAKE_FIND_LIBRARY_SUFFIXES})
229 set(BUILD_SHARED_LIBS OFF)
230 # This is required to force find_package(Boost) to use static libraries.
231 set(Boost_USE_STATIC_LIBS ON)
232 cvc4_set_option(ENABLE_STATIC_BINARY ON)
234 # Never build unit tests as static binaries, otherwise we'll end up with
235 # ~300MB per unit test.
236 if(ENABLE_UNIT_TESTING)
237 message(WARNING "Disabling unit tests since static build is enabled.")
238 set(ENABLE_UNIT_TESTING OFF)
242 #-----------------------------------------------------------------------------#
243 # Enable the ctest testing framework
245 # This needs to be enabled here rather than in subdirectory test in order to
246 # allow calling ctest from the root build directory.
249 #-----------------------------------------------------------------------------#
252 # GCC version 4.5.1 builds MiniSat incorrectly with -O2, which results in
255 if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
257 COMMAND ${CMAKE_CXX_COMPILER} -dumpversion
258 OUTPUT_VARIABLE GCC_VERSION
259 OUTPUT_STRIP_TRAILING_WHITESPACE)
260 if(GCC_VERSION VERSION_EQUAL "4.5.1")
262 "GCC 4.5.1's optimizer is known to build MiniSat incorrectly "
263 "(and by extension CVC4).")
267 #-----------------------------------------------------------------------------#
268 # Check options, find packages and configure build.
271 find_package(PythonInterp 2.7 REQUIRED)
273 find_package(PythonInterp 3 REQUIRED)
275 find_package(PythonInterp REQUIRED)
278 set(GMP_HOME ${GMP_DIR})
279 find_package(GMP REQUIRED)
282 # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
283 # otherwise the -fsanitize=address check will fail while linking.
284 set(CMAKE_REQUIRED_FLAGS -fsanitize=address)
285 add_required_c_cxx_flag("-fsanitize=address")
286 unset(CMAKE_REQUIRED_FLAGS)
287 add_required_c_cxx_flag("-fno-omit-frame-pointer")
288 add_check_c_cxx_flag("-fsanitize-recover=address")
291 if(ENABLE_ASSERTIONS)
292 add_definitions(-DCVC4_ASSERTIONS)
294 add_definitions(-DNDEBUG)
298 include(CodeCoverage)
299 APPEND_COVERAGE_COMPILER_FLAGS()
300 add_definitions(-DCVC4_COVERAGE)
301 # Note: The ctest command returns a non-zero exit code if tests fail or run
302 # into a timeout. As a consequence, the coverage report is not generated. To
303 # prevent this we always return with exit code 0 after the ctest command has
305 setup_target_for_coverage_gcovr_html(
308 ctest -j${CTEST_NTHREADS} -LE "example"
309 --output-on-failure $(ARGS) || exit 0
314 if(ENABLE_DEBUG_CONTEXT_MM)
315 add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
318 if(ENABLE_DEBUG_SYMBOLS)
319 add_check_c_cxx_flag("-ggdb3")
323 add_definitions(-DCVC4_MUZZLE)
326 # This check needs to come before the USE_CLN check.
328 find_package(Boost 1.50.0 REQUIRED COMPONENTS thread)
330 message(FATAL_ERROR "Dumping not supported with a portfolio build.")
332 # Disable CLN for portfolio builds since it is not thread safe (uses an
333 # unlocked hash table internally).
335 message(WARNING "Disabling CLN support since portfolio is enabled.")
338 set(THREADS_PREFER_PTHREAD_FLAG ON)
339 find_package(Threads REQUIRED)
340 if(THREADS_HAVE_PTHREAD_ARG)
341 add_c_cxx_flag(-pthread)
343 add_definitions(-DCVC4_PORTFOLIO)
344 set(BOOST_HAS_THREAD_ATTR 1)
347 # This has to be processed after ENABLE_PORTFOLIO (disables dumping support).
349 add_definitions(-DCVC4_DUMPING)
353 add_definitions(-DCVC4_PROFILING)
354 add_check_c_cxx_flag("-pg")
358 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
359 add_definitions(-DCVC4_PROOF)
363 add_definitions(-DCVC4_REPLAY)
367 add_definitions(-DCVC4_TRACING)
370 if(ENABLE_STATISTICS)
371 add_definitions(-DCVC4_STATISTICS_ON)
375 find_package(Valgrind REQUIRED)
376 add_definitions(-DCVC4_VALGRIND)
380 set(ABC_HOME "${ABC_DIR}")
381 find_package(ABC REQUIRED)
382 add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
386 set(CaDiCaL_HOME ${CADICAL_DIR})
387 find_package(CaDiCaL REQUIRED)
388 add_definitions(-DCVC4_USE_CADICAL)
392 set(GPL_LIBS "${GPL_LIBS} cln")
393 find_package(CLN 1.2.2 REQUIRED)
394 set(CVC4_USE_CLN_IMP 1)
395 set(CVC4_USE_GMP_IMP 0)
397 set(CVC4_USE_CLN_IMP 0)
398 set(CVC4_USE_GMP_IMP 1)
401 if(USE_CRYPTOMINISAT)
402 # CryptoMiniSat requires pthreads support
403 set(THREADS_PREFER_PTHREAD_FLAG ON)
404 find_package(Threads REQUIRED)
405 if(THREADS_HAVE_PTHREAD_ARG)
406 add_c_cxx_flag(-pthread)
408 set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
409 find_package(CryptoMiniSat REQUIRED)
410 add_definitions(-DCVC4_USE_CRYPTOMINISAT)
414 set(Drat2Er_HOME ${DRAT2ER_DIR})
415 find_package(Drat2Er REQUIRED)
416 add_definitions(-DCVC4_USE_DRAT2ER)
420 set(GPL_LIBS "${GPL_LIBS} glpk")
421 set(GLPK_HOME ${GLPK_DIR})
422 find_package(GLPK REQUIRED)
423 add_definitions(-DCVC4_USE_GLPK)
427 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
428 set(LFSC_HOME ${LFSC_DIR})
429 find_package(LFSC REQUIRED)
430 add_definitions(-DCVC4_USE_LFSC)
434 set(GPL_LIBS "${GPL_LIBS} readline")
435 find_package(Readline REQUIRED)
436 set(HAVE_LIBREADLINE 1)
437 if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
438 set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
443 set(SymFPU_HOME ${SYMFPU_DIR})
444 find_package(SymFPU REQUIRED)
445 add_definitions(-DCVC4_USE_SYMFPU)
446 set(CVC4_USE_SYMFPU 1)
448 set(CVC4_USE_SYMFPU 0)
454 "Bad configuration detected: BSD-licensed code only, but also requested "
455 "GPLed libraries: ${GPL_LIBS}")
460 #-----------------------------------------------------------------------------#
461 # Generate CVC4's cvc4autoconfig.h header
463 include(ConfigureCVC4)
464 configure_file(cvc4autoconfig.h.in cvc4autoconfig.h)
465 include_directories(${CMAKE_CURRENT_BINARY_DIR})
467 #-----------------------------------------------------------------------------#
470 # signatures needs to come before src since it adds source files to libcvc4.
472 add_subdirectory(proofs/signatures)
475 add_subdirectory(doc)
476 add_subdirectory(examples EXCLUDE_FROM_ALL) # excluded from all target
477 add_subdirectory(src)
478 add_subdirectory(test)
480 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
481 add_subdirectory(src/bindings)
484 #-----------------------------------------------------------------------------#
485 # Print build configuration
487 # Convert build type to lower case.
488 string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING)
490 # Get all definitions added via add_definitions.
491 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
492 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
494 message("CVC4 ${CVC4_RELEASE_STRING}")
496 message("Build profile : ${CVC4_BUILD_PROFILE_STRING}")
498 print_config("GPL :" ENABLE_GPL)
499 print_config("Best configuration :" ENABLE_BEST)
500 print_config("Optimized :" ENABLE_OPTIMIZED)
501 print_config("Optimization level :" OPTIMIZATION_LEVEL)
503 print_config("Assertions :" ENABLE_ASSERTIONS)
504 print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS)
505 print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
507 print_config("Dumping :" ENABLE_DUMPING)
508 print_config("Muzzle :" ENABLE_MUZZLE)
509 print_config("Proofs :" ENABLE_PROOFS)
510 print_config("Replay :" ENABLE_REPLAY)
511 print_config("Statistics :" ENABLE_STATISTICS)
512 print_config("Tracing :" ENABLE_TRACING)
514 print_config("Asan :" ENABLE_ASAN)
515 print_config("Coverage (gcov) :" ENABLE_COVERAGE)
516 print_config("Profiling (gprof) :" ENABLE_PROFILING)
517 print_config("Unit tests :" ENABLE_UNIT_TESTING)
518 print_config("Valgrind :" ENABLE_VALGRIND)
520 print_config("Shared libs :" ENABLE_SHARED)
521 print_config("Static binary :" ENABLE_STATIC_BINARY)
522 print_config("Java bindings :" BUILD_BINDINGS_JAVA)
523 print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
524 print_config("Python2 :" USE_PYTHON2)
525 print_config("Python3 :" USE_PYTHON3)
527 print_config("Portfolio :" ENABLE_PORTFOLIO)
529 print_config("ABC :" USE_ABC)
530 print_config("CaDiCaL :" USE_CADICAL)
531 print_config("CryptoMiniSat :" USE_CRYPTOMINISAT)
532 print_config("drat2er :" USE_DRAT2ER)
533 print_config("GLPK :" USE_GLPK)
534 print_config("LFSC :" USE_LFSC)
537 message("MP library : cln")
539 message("MP library : gmp")
541 print_config("Readline :" ${USE_READLINE})
542 print_config("SymFPU :" ${USE_SYMFPU})
545 message("ABC dir : ${ABC_DIR}")
548 message("ANTLR dir : ${ANTLR_DIR}")
551 message("CADICAL dir : ${CADICAL_DIR}")
553 if(CRYPTOMINISAT_DIR)
554 message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}")
557 message("DRAT2ER dir : ${DRAT2ER_DIR}")
560 message("GLPK dir : ${GLPK_DIR}")
563 message("GMP dir : ${GMP_DIR}")
566 message("LFSC dir : ${LFSC_DIR}")
569 message("SYMFPU dir : ${SYMFPU_DIR}")
572 message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}")
573 message("CXXFLAGS : ${CMAKE_CXX_FLAGS}")
574 message("CFLAGS : ${CMAKE_C_FLAGS}")
576 message("Install prefix : ${CMAKE_INSTALL_PREFIX}")
581 "CVC4 license : GPLv3 (due to optional libraries; see below)"
584 "Please note that CVC4 will be built against the following GPLed libraries:"
588 "As these libraries are covered under the GPLv3, so is this build of CVC4."
590 "CVC4 is also available to you under the terms of the (modified) BSD license."
592 "If you prefer to license CVC4 under those terms, please configure CVC4 to"
594 "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
598 "CVC4 license : modified BSD"
601 "Note that this configuration is NOT built against any GPL'ed libraries, so"
603 "it is covered by the (modified) BSD license. This is, however, not the best"
605 "performing configuration of CVC4. To build against GPL'ed libraries which"
607 "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
612 message("Now just type make, followed by make check or make install.")