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 #-----------------------------------------------------------------------------#
38 #-----------------------------------------------------------------------------#
42 option(ENABLE_GPL "Enable GPL dependencies")
44 # General build options
46 # >> 3-valued: IGNORE ON OFF
47 # > allows to detect if set by user (default: IGNORE)
48 # > only necessary for options set for build types
49 cvc4_option(ENABLE_ASAN "Enable ASAN build")
50 cvc4_option(ENABLE_ASSERTIONS "Enable assertions")
51 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
52 cvc4_option(ENABLE_DUMPING "Enable dumping")
53 cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output")
54 cvc4_option(ENABLE_OPTIMIZED "Enable optimization")
55 cvc4_option(ENABLE_PORTFOLIO "Enable portfolio support")
56 cvc4_option(ENABLE_PROOFS "Enable proof support")
57 cvc4_option(ENABLE_REPLAY "Enable the replay feature")
58 cvc4_option(ENABLE_STATISTICS "Enable statistics")
59 cvc4_option(ENABLE_TRACING "Enable tracing")
60 cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing")
61 cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation")
62 cvc4_option(ENABLE_SHARED "Build as shared library")
64 # > for options where we don't need to detect if set by user (default: OFF)
65 option(ENABLE_BEST "Enable dependencies known to give best performance")
66 option(ENABLE_COVERAGE "Enable support for gcov coverage testing")
67 option(ENABLE_DEBUG_CONTEXT_MM "Enable the debug context memory manager")
68 option(ENABLE_PROFILING "Enable support for gprof profiling")
70 # Optional dependencies
72 # >> 3-valued: IGNORE ON OFF
73 # > allows to detect if set by user (default: IGNORE)
74 # > only necessary for options set for ENABLE_BEST
75 cvc4_option(USE_ABC "Use ABC for AIG bit-blasting")
76 cvc4_option(USE_CLN "Use CLN instead of GMP")
77 cvc4_option(USE_GLPK "Use GLPK simplex solver")
78 cvc4_option(USE_READLINE "Use readline for better interactive support")
80 # > for options where we don't need to detect if set by user (default: OFF)
81 option(USE_CADICAL "Use CaDiCaL SAT solver")
82 option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
83 option(USE_LFSC "Use LFSC proof checker")
84 option(USE_SYMFPU "Use SymFPU for floating point support")
85 option(USE_PYTHON2 "Prefer using Python 2 (for Python bindings)")
86 option(USE_PYTHON3 "Prefer using Python 3 (for Python bindings)")
88 # Custom install directories for dependencies
89 # If no directory is provided by the user, we first check if the dependency was
90 # installed via the corresponding contrib/get-* script and if not found, we
91 # check the intalled system version. If the user provides a directory we
92 # immediately fail if the dependency was not found at the specified location.
93 set(ABC_DIR "" CACHE STRING "Set ABC install directory")
94 set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory")
95 set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory")
96 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
97 set(CXXTEST_DIR "" CACHE STRING "Set CxxTest install directory")
98 set(GLPK_DIR "" CACHE STRING "Set GLPK install directory")
99 set(GMP_DIR "" CACHE STRING "Set GMP install directory")
100 set(LFSC_DIR "" CACHE STRING "Set LFSC install directory")
101 set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory")
103 # Prepend binaries with prefix on make install
104 set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install")
106 # Supported language bindings
107 option(BUILD_BINDINGS_JAVA "Build Java bindings")
108 option(BUILD_BINDINGS_PYTHON "Build Python bindings")
110 #-----------------------------------------------------------------------------#
111 # Internal cmake variables
113 set(OPTIMIZATION_LEVEL 3)
116 #-----------------------------------------------------------------------------#
117 # Determine number of threads available, used to configure (default) parallel
118 # execution of custom test targets (can be overriden with ARGS=-jN).
120 include(ProcessorCount)
121 ProcessorCount(CTEST_NTHREADS)
122 if(CTEST_NTHREADS EQUAL 0)
123 set(CTEST_NTHREADS 1)
126 #-----------------------------------------------------------------------------#
129 # Note: Module CodeCoverage requires the name of the debug build to conform
130 # to cmake standards (first letter uppercase).
131 set(BUILD_TYPES Production Debug Testing Competition)
134 set(CMAKE_BUILD_TYPE Debug)
137 # Set the default build type to Production
138 if(NOT CMAKE_BUILD_TYPE)
140 Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
141 # Provide drop down menu options in cmake-gui
142 set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
145 # Check if specified build type is valid.
146 list(FIND BUILD_TYPES ${CMAKE_BUILD_TYPE} FOUND_BUILD_TYPE)
147 if(${FOUND_BUILD_TYPE} EQUAL -1)
149 "'${CMAKE_BUILD_TYPE}' is not a valid build type. "
150 "Available builds are: ${BUILD_TYPES}")
153 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
154 include(Config${CMAKE_BUILD_TYPE})
156 #-----------------------------------------------------------------------------#
159 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
160 add_check_c_cxx_flag("-Wall")
161 add_check_c_flag("-fexceptions")
162 add_check_c_cxx_flag("-Wno-deprecated")
163 add_check_cxx_flag("-Wsuggest-override")
164 add_check_cxx_flag("-Wnon-virtual-dtor")
166 # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
167 # cdlist.h warnings. Remove when fixed.
168 add_check_cxx_flag("-Wno-class-memaccess")
170 #-----------------------------------------------------------------------------#
171 # Option defaults (three-valued options (cvc4_option(...)))
173 # These options are only set if their value is IGNORE. Otherwise, the user
174 # already set the option, which we don't want to overwrite.
176 cvc4_set_option(ENABLE_SHARED ON)
178 #-----------------------------------------------------------------------------#
179 # Set options for best configuration
182 cvc4_set_option(USE_ABC ON)
183 cvc4_set_option(USE_CADICAL ON)
184 cvc4_set_option(USE_CLN ON)
185 cvc4_set_option(USE_CRYPTOMINISAT ON)
186 cvc4_set_option(USE_GLPK ON)
187 cvc4_set_option(USE_READLINE ON)
190 # Only enable unit testing if assertions are enabled. Otherwise, unit tests
191 # that expect AssertionException to be thrown will fail.
192 if(NOT ENABLE_ASSERTIONS)
193 set(ENABLE_UNIT_TESTING OFF)
196 # Never build unit tests as static binaries, otherwise we'll end up with
197 # ~300MB per unit test.
198 if(ENABLE_UNIT_TESTING)
199 set(ENABLE_SHARED ON)
202 #-----------------------------------------------------------------------------#
203 # Shared/static libraries
205 # This needs to be set before any find_package(...) command since we want to
206 # search for static libraries with suffix .a.
209 set(BUILD_SHARED_LIBS ON)
211 set(CMAKE_FIND_LIBRARY_SUFFIXES ".a ${CMAKE_FIND_LIBRARY_SUFFIXES}")
212 set(BUILD_SHARED_LIBS OFF)
213 # This is required to force find_package(Boost) to use static libraries.
214 set(Boost_USE_STATIC_LIBS ON)
217 #-----------------------------------------------------------------------------#
218 # Enable the ctest testing framework
220 # This needs to be enabled here rather than in subdirectory test in order to
221 # allow calling ctest from the root build directory.
224 #-----------------------------------------------------------------------------#
227 # GCC version 4.5.1 builds MiniSat incorrectly with -O2, which results in
230 if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
232 COMMAND ${CMAKE_CXX_COMPILER} -dumpversion
233 OUTPUT_VARIABLE GCC_VERSION
234 OUTPUT_STRIP_TRAILING_WHITESPACE)
235 if(GCC_VERSION VERSION_EQUAL "4.5.1")
237 "GCC 4.5.1's optimizer is known to build MiniSat incorrectly "
238 "(and by extension CVC4).")
242 #-----------------------------------------------------------------------------#
243 # Check options, find packages and configure build.
246 find_package(PythonInterp 2.7 REQUIRED)
248 find_package(PythonInterp 3 REQUIRED)
250 find_package(PythonInterp REQUIRED)
253 set(GMP_HOME ${GMP_DIR})
254 find_package(GMP REQUIRED)
257 # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
258 # otherwise the -fsanitize=address check will fail while linking.
259 set(CMAKE_REQUIRED_FLAGS -fsanitize=address)
260 add_required_c_cxx_flag("-fsanitize=address")
261 unset(CMAKE_REQUIRED_FLAGS)
262 add_required_c_cxx_flag("-fno-omit-frame-pointer")
263 add_check_c_cxx_flag("-fsanitize-recover=address")
266 if(ENABLE_ASSERTIONS)
267 add_definitions(-DCVC4_ASSERTIONS)
269 add_definitions(-DNDEBUG)
273 include(CodeCoverage)
274 APPEND_COVERAGE_COMPILER_FLAGS()
275 add_definitions(-DCVC4_COVERAGE)
276 # Note: The ctest command returns a non-zero exit code if tests fail or run
277 # into a timeout. As a consequence, the coverage report is not generated. To
278 # prevent this we always return with exit code 0 after the ctest command has
280 setup_target_for_coverage_lcov(
283 ctest -j${CTEST_NTHREADS} -LE "example"
284 --output-on-failure $(ARGS) || exit 0
289 if(ENABLE_DEBUG_CONTEXT_MM)
290 add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
293 if(ENABLE_DEBUG_SYMBOLS)
294 add_check_c_cxx_flag("-ggdb3")
298 add_definitions(-DCVC4_MUZZLE)
301 # This check needs to come before the USE_CLN check.
303 find_package(Boost 1.50.0 REQUIRED COMPONENTS thread)
305 message(FATAL_ERROR "Dumping not supported with a portfolio build.")
307 # Disable CLN for portfolio builds since it is not thread safe (uses an
308 # unlocked hash table internally).
310 message(WARNING "Disabling CLN support since portfolio is enabled.")
313 set(THREADS_PREFER_PTHREAD_FLAG ON)
314 find_package(Threads REQUIRED)
315 if(THREADS_HAVE_PTHREAD_ARG)
316 add_c_cxx_flag(-pthread)
318 add_definitions(-DCVC4_PORTFOLIO)
319 set(BOOST_HAS_THREAD_ATTR 1)
322 # This has to be processed after ENABLE_PORTFOLIO (disables dumping support).
324 add_definitions(-DCVC4_DUMPING)
328 add_definitions(-DCVC4_PROFILING)
329 add_check_c_cxx_flag("-pg")
333 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
334 add_definitions(-DCVC4_PROOF)
338 add_definitions(-DCVC4_REPLAY)
342 add_definitions(-DCVC4_TRACING)
345 if(ENABLE_STATISTICS)
346 add_definitions(-DCVC4_STATISTICS_ON)
350 find_package(Valgrind REQUIRED)
351 add_definitions(-DCVC4_VALGRIND)
355 set(ABC_HOME "${ABC_DIR}")
356 find_package(ABC REQUIRED)
357 add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
361 set(CaDiCaL_HOME ${CADICAL_DIR})
362 find_package(CaDiCaL REQUIRED)
363 add_definitions(-DCVC4_USE_CADICAL)
367 set(GPL_LIBS "${GPL_LIBS} cln")
368 find_package(CLN 1.2.2 REQUIRED)
369 set(CVC4_USE_CLN_IMP 1)
370 set(CVC4_USE_GMP_IMP 0)
372 set(CVC4_USE_CLN_IMP 0)
373 set(CVC4_USE_GMP_IMP 1)
376 if(USE_CRYPTOMINISAT)
377 # CryptoMiniSat requires pthreads support
378 set(THREADS_PREFER_PTHREAD_FLAG ON)
379 find_package(Threads REQUIRED)
380 if(THREADS_HAVE_PTHREAD_ARG)
381 add_c_cxx_flag(-pthread)
383 set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
384 find_package(CryptoMiniSat REQUIRED)
385 add_definitions(-DCVC4_USE_CRYPTOMINISAT)
389 set(GPL_LIBS "${GPL_LIBS} glpk")
390 set(GLPK_HOME ${GLPK_DIR})
391 find_package(GLPK REQUIRED)
392 add_definitions(-DCVC4_USE_GLPK)
396 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
397 set(LFSC_HOME ${LFSC_DIR})
398 find_package(LFSC REQUIRED)
399 add_definitions(-DCVC4_USE_LFSC)
403 set(GPL_LIBS "${GPL_LIBS} readline")
404 find_package(Readline REQUIRED)
405 set(HAVE_LIBREADLINE 1)
406 if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
407 set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
412 set(SymFPU_HOME ${SYMFPU_DIR})
413 find_package(SymFPU REQUIRED)
414 add_definitions(-DCVC4_USE_SYMFPU)
415 set(CVC4_USE_SYMFPU 1)
417 set(CVC4_USE_SYMFPU 0)
423 "Bad configuration detected: BSD-licensed code only, but also requested "
424 "GPLed libraries: ${GPL_LIBS}")
429 #-----------------------------------------------------------------------------#
430 # Generate CVC4's cvc4autoconfig.h header
432 include(ConfigureCVC4)
433 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
434 include_directories(${CMAKE_CURRENT_BINARY_DIR})
436 #-----------------------------------------------------------------------------#
439 # signatures needs to come before src since it adds source files to libcvc4.
441 add_subdirectory(proofs/signatures)
444 add_subdirectory(doc)
445 add_subdirectory(examples EXCLUDE_FROM_ALL) # excluded from all target
446 add_subdirectory(src)
447 add_subdirectory(test)
449 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
450 add_subdirectory(src/bindings)
453 #-----------------------------------------------------------------------------#
454 # Print build configuration
456 # Convert build type to lower case.
457 string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING)
459 # Get all definitions added via add_definitions.
460 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
461 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
463 message("CVC4 ${CVC4_RELEASE_STRING}")
465 message("Build profile : ${CVC4_BUILD_PROFILE_STRING}")
467 print_config("GPL :" ENABLE_GPL)
468 print_config("Best configuration :" ENABLE_BEST)
469 print_config("Optimized :" ENABLE_OPTIMIZED)
470 print_config("Optimization level :" OPTIMIZATION_LEVEL)
472 print_config("Assertions :" ENABLE_ASSERTIONS)
473 print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS)
474 print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
476 print_config("Dumping :" ENABLE_DUMPING)
477 print_config("Muzzle :" ENABLE_MUZZLE)
478 print_config("Proofs :" ENABLE_PROOFS)
479 print_config("Replay :" ENABLE_REPLAY)
480 print_config("Statistics :" ENABLE_STATISTICS)
481 print_config("Tracing :" ENABLE_TRACING)
483 print_config("Asan :" ENABLE_ASAN)
484 print_config("Coverage (gcov) :" ENABLE_COVERAGE)
485 print_config("Profiling (gprof) :" ENABLE_PROFILING)
486 print_config("Unit tests :" ENABLE_UNIT_TESTING)
487 print_config("Valgrind :" ENABLE_VALGRIND)
489 print_config("Shared libs :" ENABLE_SHARED)
490 print_config("Java bindings :" BUILD_BINDINGS_JAVA)
491 print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
492 print_config("Python2 :" USE_PYTHON2)
493 print_config("Python3 :" USE_PYTHON3)
495 print_config("Portfolio :" ENABLE_PORTFOLIO)
497 print_config("ABC :" USE_ABC)
498 print_config("CaDiCaL :" USE_CADICAL)
499 print_config("CryptoMiniSat :" USE_CRYPTOMINISAT)
500 print_config("GLPK :" USE_GLPK)
501 print_config("LFSC :" USE_LFSC)
504 message("MP library : cln")
506 message("MP library : gmp")
508 print_config("Readline :" ${USE_READLINE})
509 print_config("SymFPU :" ${USE_SYMFPU})
512 message("ABC dir : ${ABC_DIR}")
515 message("ANTLR dir : ${ANTLR_DIR}")
518 message("CADICAL dir : ${CADICAL_DIR}")
520 if(CRYPTOMINISAT_DIR)
521 message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}")
524 message("GLPK dir : ${GLPK_DIR}")
527 message("GMP dir : ${GMP_DIR}")
530 message("LFSC dir : ${LFSC_DIR}")
533 message("SYMFPU dir : ${SYMFPU_DIR}")
536 message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}")
537 message("CXXFLAGS : ${CMAKE_CXX_FLAGS}")
538 message("CFLAGS : ${CMAKE_C_FLAGS}")
540 message("Install prefix : ${CMAKE_INSTALL_PREFIX}")
545 "CVC4 license : GPLv3 (due to optional libraries; see below)"
548 "Please note that CVC4 will be built against the following GPLed libraries:"
552 "As these libraries are covered under the GPLv3, so is this build of CVC4."
554 "CVC4 is also available to you under the terms of the (modified) BSD license."
556 "If you prefer to license CVC4 under those terms, please configure CVC4 to"
558 "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
562 "CVC4 license : modified BSD"
565 "Note that this configuration is NOT built against any GPL'ed libraries, so"
567 "it is covered by the (modified) BSD license. This is, however, not the best"
569 "performing configuration of CVC4. To build against GPL'ed libraries which"
571 "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
576 message("Now just type make, followed by make check or make install.")