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 "-prerelease")
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_LFSC "Use LFSC proof checker")
97 option(USE_SYMFPU "Use SymFPU for floating point support")
98 option(USE_PYTHON2 "Prefer using Python 2 (for Python bindings)")
99 option(USE_PYTHON3 "Prefer using Python 3 (for Python bindings)")
101 # Custom install directories for dependencies
102 # If no directory is provided by the user, we first check if the dependency was
103 # installed via the corresponding contrib/get-* script and if not found, we
104 # check the intalled system version. If the user provides a directory we
105 # immediately fail if the dependency was not found at the specified location.
106 set(ABC_DIR "" CACHE STRING "Set ABC install directory")
107 set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory")
108 set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory")
109 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
110 set(CXXTEST_DIR "" CACHE STRING "Set CxxTest install directory")
111 set(GLPK_DIR "" CACHE STRING "Set GLPK install directory")
112 set(GMP_DIR "" CACHE STRING "Set GMP install directory")
113 set(LFSC_DIR "" CACHE STRING "Set LFSC install directory")
114 set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory")
116 # Prepend binaries with prefix on make install
117 set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install")
119 # Supported language bindings
120 option(BUILD_BINDINGS_JAVA "Build Java bindings")
121 option(BUILD_BINDINGS_PYTHON "Build Python bindings")
123 #-----------------------------------------------------------------------------#
124 # Internal cmake variables
126 set(OPTIMIZATION_LEVEL 3)
129 #-----------------------------------------------------------------------------#
130 # Determine number of threads available, used to configure (default) parallel
131 # execution of custom test targets (can be overriden with ARGS=-jN).
133 include(ProcessorCount)
134 ProcessorCount(CTEST_NTHREADS)
135 if(CTEST_NTHREADS EQUAL 0)
136 set(CTEST_NTHREADS 1)
139 #-----------------------------------------------------------------------------#
142 # Note: Module CodeCoverage requires the name of the debug build to conform
143 # to cmake standards (first letter uppercase).
144 set(BUILD_TYPES Production Debug Testing Competition)
147 set(CMAKE_BUILD_TYPE Debug)
150 # Set the default build type to Production
151 if(NOT CMAKE_BUILD_TYPE)
153 Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
154 # Provide drop down menu options in cmake-gui
155 set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
158 # Check if specified build type is valid.
159 list(FIND BUILD_TYPES ${CMAKE_BUILD_TYPE} FOUND_BUILD_TYPE)
160 if(${FOUND_BUILD_TYPE} EQUAL -1)
162 "'${CMAKE_BUILD_TYPE}' is not a valid build type. "
163 "Available builds are: ${BUILD_TYPES}")
166 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
167 include(Config${CMAKE_BUILD_TYPE})
169 #-----------------------------------------------------------------------------#
172 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
173 add_check_c_cxx_flag("-Wall")
174 add_check_c_flag("-fexceptions")
175 add_check_c_cxx_flag("-Wno-deprecated")
176 add_check_cxx_flag("-Wsuggest-override")
177 add_check_cxx_flag("-Wnon-virtual-dtor")
179 # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
180 # cdlist.h warnings. Remove when fixed.
181 add_check_cxx_flag("-Wno-class-memaccess")
183 #-----------------------------------------------------------------------------#
184 # Option defaults (three-valued options (cvc4_option(...)))
186 # These options are only set if their value is IGNORE. Otherwise, the user
187 # already set the option, which we don't want to overwrite.
189 if(ENABLE_STATIC_BINARY)
190 cvc4_set_option(ENABLE_SHARED OFF)
192 cvc4_set_option(ENABLE_SHARED ON)
195 #-----------------------------------------------------------------------------#
196 # Set options for best configuration
199 cvc4_set_option(USE_ABC ON)
200 cvc4_set_option(USE_CADICAL ON)
201 cvc4_set_option(USE_CLN ON)
202 cvc4_set_option(USE_CRYPTOMINISAT ON)
203 cvc4_set_option(USE_GLPK ON)
204 cvc4_set_option(USE_READLINE ON)
207 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
208 # that expect AssertionException to be thrown will fail.
209 if(NOT ENABLE_ASSERTIONS)
210 set(ENABLE_UNIT_TESTING OFF)
213 # Never build unit tests as static binaries, otherwise we'll end up with
214 # ~300MB per unit test.
215 if(ENABLE_UNIT_TESTING)
216 if(NOT ENABLE_SHARED)
217 message(WARNING "Disabling static build since unit testing is enabled.")
219 set(ENABLE_SHARED ON)
222 #-----------------------------------------------------------------------------#
223 # Shared/static libraries
225 # This needs to be set before any find_package(...) command since we want to
226 # search for static libraries with suffix .a.
229 set(BUILD_SHARED_LIBS ON)
230 if(ENABLE_STATIC_BINARY)
231 set(ENABLE_STATIC_BINARY OFF)
232 message(WARNING "Disabling static binary since shared build is enabled.")
235 set(CMAKE_FIND_LIBRARY_SUFFIXES ".a ${CMAKE_FIND_LIBRARY_SUFFIXES}")
236 set(BUILD_SHARED_LIBS OFF)
237 # This is required to force find_package(Boost) to use static libraries.
238 set(Boost_USE_STATIC_LIBS ON)
239 cvc4_set_option(ENABLE_STATIC_BINARY ON)
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(GPL_LIBS "${GPL_LIBS} glpk")
415 set(GLPK_HOME ${GLPK_DIR})
416 find_package(GLPK REQUIRED)
417 add_definitions(-DCVC4_USE_GLPK)
421 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
422 set(LFSC_HOME ${LFSC_DIR})
423 find_package(LFSC REQUIRED)
424 add_definitions(-DCVC4_USE_LFSC)
428 set(GPL_LIBS "${GPL_LIBS} readline")
429 find_package(Readline REQUIRED)
430 set(HAVE_LIBREADLINE 1)
431 if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
432 set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
437 set(SymFPU_HOME ${SYMFPU_DIR})
438 find_package(SymFPU REQUIRED)
439 add_definitions(-DCVC4_USE_SYMFPU)
440 set(CVC4_USE_SYMFPU 1)
442 set(CVC4_USE_SYMFPU 0)
448 "Bad configuration detected: BSD-licensed code only, but also requested "
449 "GPLed libraries: ${GPL_LIBS}")
454 #-----------------------------------------------------------------------------#
455 # Generate CVC4's cvc4autoconfig.h header
457 include(ConfigureCVC4)
458 configure_file(cvc4autoconfig.h.in cvc4autoconfig.h)
459 include_directories(${CMAKE_CURRENT_BINARY_DIR})
461 #-----------------------------------------------------------------------------#
464 # signatures needs to come before src since it adds source files to libcvc4.
466 add_subdirectory(proofs/signatures)
469 add_subdirectory(doc)
470 add_subdirectory(examples EXCLUDE_FROM_ALL) # excluded from all target
471 add_subdirectory(src)
472 add_subdirectory(test)
474 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
475 add_subdirectory(src/bindings)
478 #-----------------------------------------------------------------------------#
479 # Print build configuration
481 # Convert build type to lower case.
482 string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING)
484 # Get all definitions added via add_definitions.
485 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
486 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
488 message("CVC4 ${CVC4_RELEASE_STRING}")
490 message("Build profile : ${CVC4_BUILD_PROFILE_STRING}")
492 print_config("GPL :" ENABLE_GPL)
493 print_config("Best configuration :" ENABLE_BEST)
494 print_config("Optimized :" ENABLE_OPTIMIZED)
495 print_config("Optimization level :" OPTIMIZATION_LEVEL)
497 print_config("Assertions :" ENABLE_ASSERTIONS)
498 print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS)
499 print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
501 print_config("Dumping :" ENABLE_DUMPING)
502 print_config("Muzzle :" ENABLE_MUZZLE)
503 print_config("Proofs :" ENABLE_PROOFS)
504 print_config("Replay :" ENABLE_REPLAY)
505 print_config("Statistics :" ENABLE_STATISTICS)
506 print_config("Tracing :" ENABLE_TRACING)
508 print_config("Asan :" ENABLE_ASAN)
509 print_config("Coverage (gcov) :" ENABLE_COVERAGE)
510 print_config("Profiling (gprof) :" ENABLE_PROFILING)
511 print_config("Unit tests :" ENABLE_UNIT_TESTING)
512 print_config("Valgrind :" ENABLE_VALGRIND)
514 print_config("Shared libs :" ENABLE_SHARED)
515 print_config("Static binary :" ENABLE_STATIC_BINARY)
516 print_config("Java bindings :" BUILD_BINDINGS_JAVA)
517 print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
518 print_config("Python2 :" USE_PYTHON2)
519 print_config("Python3 :" USE_PYTHON3)
521 print_config("Portfolio :" ENABLE_PORTFOLIO)
523 print_config("ABC :" USE_ABC)
524 print_config("CaDiCaL :" USE_CADICAL)
525 print_config("CryptoMiniSat :" USE_CRYPTOMINISAT)
526 print_config("GLPK :" USE_GLPK)
527 print_config("LFSC :" USE_LFSC)
530 message("MP library : cln")
532 message("MP library : gmp")
534 print_config("Readline :" ${USE_READLINE})
535 print_config("SymFPU :" ${USE_SYMFPU})
538 message("ABC dir : ${ABC_DIR}")
541 message("ANTLR dir : ${ANTLR_DIR}")
544 message("CADICAL dir : ${CADICAL_DIR}")
546 if(CRYPTOMINISAT_DIR)
547 message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}")
550 message("GLPK dir : ${GLPK_DIR}")
553 message("GMP dir : ${GMP_DIR}")
556 message("LFSC dir : ${LFSC_DIR}")
559 message("SYMFPU dir : ${SYMFPU_DIR}")
562 message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}")
563 message("CXXFLAGS : ${CMAKE_CXX_FLAGS}")
564 message("CFLAGS : ${CMAKE_C_FLAGS}")
566 message("Install prefix : ${CMAKE_INSTALL_PREFIX}")
571 "CVC4 license : GPLv3 (due to optional libraries; see below)"
574 "Please note that CVC4 will be built against the following GPLed libraries:"
578 "As these libraries are covered under the GPLv3, so is this build of CVC4."
580 "CVC4 is also available to you under the terms of the (modified) BSD license."
582 "If you prefer to license CVC4 under those terms, please configure CVC4 to"
584 "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
588 "CVC4 license : modified BSD"
591 "Note that this configuration is NOT built against any GPL'ed libraries, so"
593 "it is covered by the (modified) BSD license. This is, however, not the best"
595 "performing configuration of CVC4. To build against GPL'ed libraries which"
597 "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
602 message("Now just type make, followed by make check or make install.")