1 cmake_minimum_required (VERSION 3.0.1)
3 #-----------------------------------------------------------------------------#
7 # Major component of the version of CVC4.
9 # Minor component of the version of CVC4.
11 # Release component of the version of CVC4.
13 # Extraversion component of the version of CVC4.
14 set(CVC4_EXTRAVERSION "-prerelease")
16 # Full release string for CVC4.
18 set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
20 set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}")
23 # Define to the full name of this package.
24 set(PACKAGE_NAME "${PROJECT_NAME}")
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.
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")
39 #-----------------------------------------------------------------------------#
41 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
42 set(CMAKE_C_STANDARD 99)
43 set(CMAKE_CXX_STANDARD 11)
45 #-----------------------------------------------------------------------------#
48 include(CheckCCompilerFlag)
49 include(CheckCXXCompilerFlag)
51 macro(add_c_flag flag)
53 set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
55 set(CMAKE_C_FLAGS "${flag}")
57 message(STATUS "Configuring with C flag '${flag}'")
60 macro(add_cxx_flag flag)
62 set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
64 set(CMAKE_CXX_FLAGS "${flag}")
66 message(STATUS "Configuring with CXX flag '${flag}'")
69 macro(add_c_cxx_flag flag)
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})
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})
90 macro(add_check_c_cxx_flag flag)
91 add_check_c_flag(${flag})
92 add_check_cxx_flag(${flag})
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")
101 add_cxx_flag(${flag})
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")
113 macro(add_required_c_cxx_flag flag)
114 add_required_c_flag(${flag})
115 add_required_cxx_flag(${flag})
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})
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})
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)
142 # Only set option if the user did not set an option.
143 macro(cvc4_set_option var value)
144 if(${var} STREQUAL "IGNORE")
149 #-----------------------------------------------------------------------------#
153 option(ENABLE_GPL "Enable GPL dependencies" OFF)
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")
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")
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")
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")
201 # Supported language bindings
202 option(BUILD_BINDINGS_JAVA "Build Java bindings" OFF)
203 option(BUILD_BINDINGS_PYTHON "Build Python bindings" OFF)
205 # All bindings: c,java,csharp,perl,php,python,ruby,tcl,ocaml
208 #-----------------------------------------------------------------------------#
209 # Internal cmake variables
214 set(BUILD_TYPES Production Debug Testing Competition)
216 #-----------------------------------------------------------------------------#
217 # CVC4 build variables
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.
227 #-----------------------------------------------------------------------------#
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")
236 #-----------------------------------------------------------------------------#
240 set(CMAKE_BUILD_TYPE Debug)
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})
249 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
251 if(CMAKE_BUILD_TYPE STREQUAL "Debug")
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)
261 # enable_static_binary=yes
265 #-----------------------------------------------------------------------------#
266 # Option defaults (three-valued options (cvc4_option(...)))
268 cvc4_set_option(ENABLE_PORTFOLIO OFF)
269 cvc4_set_option(ENABLE_SHARED ON)
270 cvc4_set_option(ENABLE_VALGRIND OFF)
272 #-----------------------------------------------------------------------------#
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)
282 find_package(PythonInterp REQUIRED)
284 set(ANTLR_HOME ${ANTLR_DIR})
285 find_package(ANTLR REQUIRED)
287 set(GMP_HOME ${GMP_DIR})
288 find_package(GMP REQUIRED)
289 libcvc4_link_libraries(${GMP_LIBRARIES})
290 libcvc4_include_directories(${GMP_INCLUDE_DIR})
293 #-----------------------------------------------------------------------------#
294 # Enable the ctest testing framework
298 #-----------------------------------------------------------------------------#
300 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
301 set(BUILD_BINDINGS TRUE)
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")
312 if(ENABLE_ASSERTIONS)
313 add_definitions(-DCVC4_ASSERTIONS)
317 include(CodeCoverage)
318 APPEND_COVERAGE_COMPILER_FLAGS()
319 add_definitions(-DCVC4_COVERAGE)
320 setup_target_for_coverage_lcov(
322 EXECUTABLE ctest $(ARGS)
323 DEPENDENCIES cvc4-bin)
327 add_definitions(-DCVC4_DUMPING)
329 add_definitions(-DNDEBUG)
332 if(ENABLE_DEBUG_SYMBOLS)
333 add_check_c_cxx_flag("-ggdb3")
337 add_definitions(-DCVC4_MUZZLE)
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).
345 set(THREADS_PREFER_PTHREAD_FLAG ON)
346 find_package(Threads REQUIRED)
347 if(THREADS_HAVE_PTHREAD_ARG)
348 add_c_cxx_flag(-pthread)
350 add_definitions(-DCVC4_PORTFOLIO)
354 add_definitions(-DCVC4_PROFILING)
355 add_check_c_cxx_flag("-pg")
359 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
360 add_definitions(-DCVC4_PROOF)
362 libcvc4_link_libraries(signatures)
366 add_definitions(-DCVC4_REPLAY)
370 add_definitions(-DCVC4_TRACING)
374 if(ENABLE_UNIT_TESTING)
375 find_package(CxxTest REQUIRED)
376 # Force shared libs for unit tests, static libs with unit tests are not
378 set(ENABLE_SHARED ON)
382 set(BUILD_SHARED_LIBS ON)
385 if(ENABLE_STATISTICS)
386 add_definitions(-DCVC4_STATISTICS_ON)
390 #TODO check if valgrind available
391 add_definitions(-DCVC4_VALGRIND)
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})
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)
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)
418 set(CVC4_USE_CLN_IMP 0)
419 set(CVC4_USE_GMP_IMP 1)
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)
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)
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)
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)
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)
463 set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 0)
466 set(HAVE_LIBREADLINE 0)
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)
476 set(CVC4_USE_SYMFPU 0)
482 "Bad configuration detected: BSD-licensed code only, but also requested "
483 "GPLed libraries: ${GPL_LIBS}")
488 #-----------------------------------------------------------------------------#
490 set(VERSION "1.6.0-prerelease")
491 string(TIMESTAMP MAN_DATE "%Y-%m-%d")
493 #-----------------------------------------------------------------------------#
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")
501 set(GIT_IS_DIRTY "false")
505 COMMAND "${GIT_EXECUTABLE}" rev-parse --abbrev-ref HEAD
506 OUTPUT_VARIABLE GIT_BRANCH
507 OUTPUT_STRIP_TRAILING_WHITESPACE
510 #-----------------------------------------------------------------------------#
512 include(ConfigureCVC4)
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
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
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
534 #set(HAVE_DECL_STRERROR_R 1)
535 ## Define to 1 if you have the <dlfcn.h> header file.
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.
541 # Define to 1 if you have the <getopt.h> header file.
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).
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.
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.
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.
579 # Define to 1 if strerror_r returns char *.
580 set(STRERROR_R_CHAR_P 1)
582 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
583 include_directories(${CMAKE_CURRENT_BINARY_DIR})
585 #-----------------------------------------------------------------------------#
587 add_subdirectory(doc)
588 add_subdirectory(src)
590 add_subdirectory(src/bindings)
592 if(BUILD_BINDINGS_JAVA)
593 add_subdirectory(test/java)
595 add_subdirectory(test/regress)
596 add_subdirectory(test/system)
597 if(ENABLE_UNIT_TESTING)
598 add_subdirectory(test/unit)
602 add_subdirectory(proofs/signatures)
605 #-----------------------------------------------------------------------------#
606 # Print build configuration
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")
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}")
622 message("CVC4 ${CVC4_RELEASE_STRING}")
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}")
636 message("Unit tests : ${ENABLE_UNIT_TESTING}")
637 message("Coverage (gcov) : ${ENABLE_COVERAGE}")
638 message("Profiling (gprof) : ${ENABLE_PROFILING}")
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}")
645 #message("Multithreaded: ${support_multithreaded}")
646 message("Portfolio : ${ENABLE_PORTFOLIO}")
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}")
654 message("MP library : cln")
656 message("MP library : gmp")
658 message("Readline : ${USE_READLINE}")
659 message("SymFPU : ${USE_SYMFPU}")
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}")
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}")
672 message("Install prefix : ${CMAKE_INSTALL_PREFIX}")
677 "CVC4 license : GPLv3 (due to optional libraries; see below)"
680 "Please note that CVC4 will be built against the following GPLed libraries:"
684 "As these libraries are covered under the GPLv3, so is this build of CVC4."
686 "CVC4 is also available to you under the terms of the (modified) BSD license."
688 "If you prefer to license CVC4 under those terms, please configure CVC4 to"
690 "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
694 "CVC4 license : modified BSD"
697 "Note that this configuration is NOT built against any GPL'ed libraries, so"
699 "it is covered by the (modified) BSD license. This is, however, not the best"
701 "performing configuration of CVC4. To build against GPL'ed libraries which"
703 "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
708 message("Now just type make, followed by make check or make install.")