1 cmake_minimum_required(VERSION 3.1)
4 cmake_policy(SET CMP0075 NEW)
7 #-----------------------------------------------------------------------------#
11 # Major component of the version of CVC4.
13 # Minor component of the version of CVC4.
15 # Release component of the version of CVC4.
17 # Extraversion component of the version of CVC4.
18 set(CVC4_EXTRAVERSION "-prerelease")
20 # Full release string for CVC4.
22 set(CVC4_RELEASE_STRING
23 "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
25 set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}")
28 # Define to the full name of this package.
29 set(PACKAGE_NAME "${PROJECT_NAME}")
31 # Shared library versioning. Increment SOVERSION for every new CVC4 release.
32 set(CVC4_VERSION "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}")
35 #### These defines are only use in autotools make files, will likely be
36 #### replaced with corresponding CPack stuff
37 ## Define to the full name and version of this package.
38 #set(PACKAGE_STRING "${PROJECT_NAME} ${CVC4_RELEASE_STRING}")
39 ## Define to the one symbol short name of this package.
40 #set(PACKAGE_TARNAME "${PROJECT_NAME}")
41 ## Define to the home page for this package.
43 ## Define to the version of this package.
44 #set(PACKAGE_VERSION "${CVC4_RELEASE_STRING}")
45 ## Define to the address where bug reports for this package should be sent.
46 #set(PACKAGE_BUGREPORT "cvc4-bugs@cs.stanford.edu")
48 #-----------------------------------------------------------------------------#
50 set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
51 set(CMAKE_C_STANDARD 99)
52 set(CMAKE_CXX_STANDARD 11)
54 #-----------------------------------------------------------------------------#
57 include(CheckCCompilerFlag)
58 include(CheckCXXCompilerFlag)
60 macro(add_c_flag flag)
62 set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
64 set(CMAKE_C_FLAGS "${flag}")
66 message(STATUS "Configuring with C flag '${flag}'")
69 macro(add_cxx_flag flag)
71 set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
73 set(CMAKE_CXX_FLAGS "${flag}")
75 message(STATUS "Configuring with CXX flag '${flag}'")
78 macro(add_c_cxx_flag flag)
83 macro(add_check_c_flag flag)
84 string(REGEX REPLACE "[-=]" "_" flagname ${flag})
85 check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
86 if(HAVE_FLAG${flagname})
91 macro(add_check_cxx_flag flag)
92 string(REGEX REPLACE "[-=]" "_" flagname ${flag})
93 check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
94 if(HAVE_FLAG${flagname})
99 macro(add_check_c_cxx_flag flag)
100 add_check_c_flag(${flag})
101 add_check_cxx_flag(${flag})
104 macro(add_required_cxx_flag flag)
105 string(REGEX REPLACE "[-=]" "_" flagnamename ${flag})
106 check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
107 if (NOT HAVE_FLAG${flagname})
108 message(FATAL_ERROR "Required compiler flag ${flag} not supported")
110 add_cxx_flag(${flag})
113 macro(add_required_c_flag flag)
114 string(REGEX REPLACE "[-=]" "_" flagname ${flag})
115 check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
116 if (NOT HAVE_FLAG${flagname})
117 message(FATAL_ERROR "Required compiler flag ${flag} not supported")
122 macro(add_required_c_cxx_flag flag)
123 add_required_c_flag(${flag})
124 add_required_cxx_flag(${flag})
127 # CVC4 Boolean options are three-valued to detect if an option was set by the
128 # user. The available values are: IGNORE (default), ON, OFF
129 # Default options do not override options that were set by the user, i.e.,
130 # cvc4_set_option only sets an option if it's value is still IGNORE.
131 # This e.g., allows the user to disable proofs for debug builds (where proofs
132 # are enabled by default).
133 macro(cvc4_option var description)
134 set(${var} IGNORE CACHE STRING "${description}")
135 # Provide drop down menu options in cmake-gui
136 set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF)
139 # Only set option if the user did not set an option.
140 macro(cvc4_set_option var value)
141 if(${var} STREQUAL "IGNORE")
146 # Prepend 'prepand_value' to each element of the list 'in_list'. The result
147 # is stored in 'out_list'.
148 function(list_prepend in_list prepand_value out_list)
149 foreach(_elem ${${in_list}})
150 list(APPEND ${out_list} "${prepand_value}${_elem}")
152 set(${out_list} ${${out_list}} PARENT_SCOPE)
155 #-----------------------------------------------------------------------------#
158 # Collect all libraries that must be linked against libcvc4. These will be
159 # actually linked in src/CMakeLists.txt with target_link_libaries(...).
160 macro(libcvc4_link_libraries library)
161 set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library})
164 # Collect all include directories that are required for libcvc4. These will be
165 # actually included in src/CMakeLists.txt with target_include_directories(...).
166 macro(libcvc4_include_directories dirs)
167 set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs})
170 # Collect all source files that are required to build libcvc4 in LIBCVC4_SRCS
171 # or LIBCVC4_GEN_SRCS. If GENERATED is the first argument the sources are
172 # added to LIBCVC4_GEN_SRCS. All sources are prepended with the absolute
173 # current path path. CMAKE_CURRENT_BINARY_DIR is prepended
174 # to generated source files.
175 macro(libcvc4_add_sources)
176 set(_sources ${ARGV})
178 # Check if the first argument is GENERATED.
179 list(GET _sources 0 _generated)
180 if(${_generated} STREQUAL "GENERATED")
181 list(REMOVE_AT _sources 0)
182 set(_cur_path ${CMAKE_CURRENT_BINARY_DIR})
183 set(_append_to LIBCVC4_GEN_SRCS)
185 set(_cur_path ${CMAKE_CURRENT_SOURCE_DIR})
186 set(_append_to LIBCVC4_SRCS)
189 # Prepend source files with current path.
190 foreach(_src ${_sources})
191 list(APPEND ${_append_to} "${_cur_path}/${_src}")
195 _rel_path "${PROJECT_SOURCE_DIR}/src" "${CMAKE_CURRENT_SOURCE_DIR}")
197 # Make changes to list ${_append_to} visible to the parent scope if not
199 # Note: ${_append_to} refers to the variable name whereas ${${_append_to}}
200 # refers to the contents of the variable.
202 set(${_append_to} ${${_append_to}} PARENT_SCOPE)
206 #-----------------------------------------------------------------------------#
210 option(ENABLE_GPL "Enable GPL dependencies")
212 # General build options
214 # >> 3-valued: INGORE ON OFF
215 # > allows to detect if set by user (default: IGNORE)
216 # > only necessary for options set for build types
217 cvc4_option(ENABLE_ASAN "Enable ASAN build")
218 cvc4_option(ENABLE_ASSERTIONS "Enable assertions")
219 cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
220 cvc4_option(ENABLE_DUMPING "Enable dumping")
221 cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output")
222 cvc4_option(ENABLE_OPTIMIZED "Enable optimization")
223 cvc4_option(ENABLE_PORTFOLIO "Enable portfolio support")
224 cvc4_option(ENABLE_PROOFS "Enable proof support")
225 cvc4_option(ENABLE_REPLAY "Enable the replay feature")
226 cvc4_option(ENABLE_STATISTICS "Enable statistics")
227 cvc4_option(ENABLE_TRACING "Enable tracing")
228 cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing")
229 cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation")
230 cvc4_option(ENABLE_SHARED "Build as shared library")
231 # >> 2-valued: ON OFF
232 # > for options where we don't need to detect if set by user (default: OFF)
233 option(ENABLE_BEST "Enable dependencies known to give best performance")
234 option(ENABLE_COVERAGE "Enable support for gcov coverage testing")
235 option(ENABLE_DEBUG_CONTEXT_MM "Enable the debug context memory manager")
236 option(ENABLE_PROFILING "Enable support for gprof profiling")
238 # Optional dependencies
240 # >> 3-valued: INGORE ON OFF
241 # > allows to detect if set by user (default: IGNORE)
242 # > only necessary for options set for ENABLE_BEST
243 cvc4_option(USE_ABC "Use ABC for AIG bit-blasting")
244 cvc4_option(USE_CLN "Use CLN instead of GMP")
245 cvc4_option(USE_GLPK "Use GLPK simplex solver")
246 cvc4_option(USE_READLINE "Use readline for better interactive support")
247 # >> 2-valued: ON OFF
248 # > for options where we don't need to detect if set by user (default: OFF)
249 option(USE_CADICAL "Use CaDiCaL SAT solver")
250 option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
251 option(USE_LFSC "Use LFSC proof checker")
252 option(USE_SYMFPU "Use SymFPU for floating point support")
254 # Custom install directories for dependencies
255 # If no directory is provided by the user, we first check if the dependency was
256 # installed via the corresponding contrib/get-* script and if not found, we
257 # check the intalled system version. If the user provides a directory we
258 # immediately fail if the dependency was not found at the specified location.
259 set(ABC_DIR "" CACHE STRING "Set ABC install directory")
260 set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory")
261 set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory")
262 set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
263 set(GLPK_DIR "" CACHE STRING "Set GLPK install directory")
264 set(GMP_DIR "" CACHE STRING "Set GMP install directory")
265 set(LFSC_DIR "" CACHE STRING "Set LFSC install directory")
266 set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory")
268 # Supported language bindings
269 option(BUILD_BINDINGS_JAVA "Build Java bindings")
270 option(BUILD_BINDINGS_PYTHON "Build Python bindings")
272 #-----------------------------------------------------------------------------#
273 # Internal cmake variables
275 set(OPTIMIZATION_LEVEL 3)
278 set(BUILD_TYPES Production Debug Testing Competition)
280 #-----------------------------------------------------------------------------#
281 # CVC4 build variables
284 set(CVC4_BUILD_PROFILE_PRODUCTION 0)
285 set(CVC4_BUILD_PROFILE_DEBUG 0)
286 set(CVC4_BUILD_PROFILE_TESTING 0)
287 set(CVC4_BUILD_PROFILE_COMPETITION 0)
289 #-----------------------------------------------------------------------------#
293 set(CMAKE_BUILD_TYPE Debug)
296 # Set the default build type to Production
297 if(NOT CMAKE_BUILD_TYPE)
299 Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
300 # Provide drop down menu options in cmake-gui
301 set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
303 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
305 if(CMAKE_BUILD_TYPE STREQUAL "Debug")
307 elseif(CMAKE_BUILD_TYPE STREQUAL "Production")
308 include(ConfigProduction)
309 elseif(CMAKE_BUILD_TYPE STREQUAL "Testing")
310 include(ConfigTesting)
311 elseif(CMAKE_BUILD_TYPE STREQUAL "Competition")
312 include(ConfigCompetition)
315 #-----------------------------------------------------------------------------#
318 add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
319 add_check_c_flag("-fexceptions")
320 add_check_c_cxx_flag("-Wno-deprecated")
321 add_check_cxx_flag("-Wsuggest-override")
322 add_check_cxx_flag("-Wnon-virtual-dtor")
324 #-----------------------------------------------------------------------------#
325 # Option defaults (three-valued options (cvc4_option(...)))
327 cvc4_set_option(ENABLE_PORTFOLIO OFF)
328 cvc4_set_option(ENABLE_SHARED ON)
329 cvc4_set_option(ENABLE_VALGRIND OFF)
330 cvc4_set_option(USE_ABC OFF)
331 cvc4_set_option(USE_GLPK OFF)
332 cvc4_set_option(USE_READLINE OFF)
334 #-----------------------------------------------------------------------------#
335 # Set options for best configuration
338 cvc4_set_option(USE_ABC ON)
339 cvc4_set_option(USE_CLN ON)
340 cvc4_set_option(USE_GLPK ON)
341 cvc4_set_option(USE_READLINE ON)
344 #-----------------------------------------------------------------------------#
346 # This needs to be set before any find_package(...) command since we want to
347 # search for static libraries with suffix .a.
348 if(NOT ENABLE_SHARED)
349 set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
350 set(CMAKE_EXE_LINKER_FLAGS "-static")
351 set(BUILD_SHARED_LIBS OFF)
354 #-----------------------------------------------------------------------------#
355 # Enable the ctest testing framework
359 #-----------------------------------------------------------------------------#
361 set(GMP_HOME ${GMP_DIR})
362 find_package(GMP REQUIRED)
363 libcvc4_link_libraries(${GMP_LIBRARIES})
364 libcvc4_include_directories(${GMP_INCLUDE_DIR})
367 set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address)
368 add_required_c_cxx_flag("-fsanitize=address")
369 unset(CMAKE_REQUIRED_LIBRARIES)
370 add_required_c_cxx_flag("-fno-omit-frame-pointer")
371 add_check_c_cxx_flag("-fsanitize-recover=address")
374 if(ENABLE_ASSERTIONS)
375 add_definitions(-DCVC4_ASSERTIONS)
377 add_definitions(-DNDEBUG)
381 include(CodeCoverage)
382 APPEND_COVERAGE_COMPILER_FLAGS()
383 add_definitions(-DCVC4_COVERAGE)
384 setup_target_for_coverage_lcov(
386 EXECUTABLE ctest $(ARGS)
387 DEPENDENCIES cvc4-bin)
390 if(ENABLE_DEBUG_CONTEXT_MM)
391 add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
395 add_definitions(-DCVC4_DUMPING)
398 if(ENABLE_DEBUG_SYMBOLS)
399 add_check_c_cxx_flag("-ggdb3")
403 add_definitions(-DCVC4_MUZZLE)
407 find_package(Boost 1.50.0 REQUIRED COMPONENTS thread)
408 # Disable CLN for portfolio builds since it is not thread safe (uses an
409 # unlocked hash table internally).
411 message(WARNING "Disabling CLN support since portfolio is enabled.")
414 set(THREADS_PREFER_PTHREAD_FLAG ON)
415 find_package(Threads REQUIRED)
416 if(THREADS_HAVE_PTHREAD_ARG)
417 add_c_cxx_flag(-pthread)
419 add_definitions(-DCVC4_PORTFOLIO)
420 set(BOOST_HAS_THREAD_ATTR 1)
424 add_definitions(-DCVC4_PROFILING)
425 add_check_c_cxx_flag("-pg")
429 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
430 add_definitions(-DCVC4_PROOF)
435 add_definitions(-DCVC4_REPLAY)
439 add_definitions(-DCVC4_TRACING)
443 if(ENABLE_UNIT_TESTING)
444 find_package(CxxTest REQUIRED)
445 # Force shared libs for unit tests, static libs with unit tests are not
447 set(ENABLE_SHARED ON)
451 set(BUILD_SHARED_LIBS ON)
454 if(ENABLE_STATISTICS)
455 add_definitions(-DCVC4_STATISTICS_ON)
459 find_package(Valgrind REQUIRED)
460 libcvc4_include_directories(${Valgrind_INCLUDE_DIR})
461 add_definitions(-DCVC4_VALGRIND)
465 set(ABC_HOME "${ABC_DIR}")
466 find_package(ABC REQUIRED)
467 libcvc4_link_libraries(${ABC_LIBRARIES})
468 libcvc4_include_directories(${ABC_INCLUDE_DIR})
469 add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
473 set(CaDiCaL_HOME ${CADICAL_DIR})
474 find_package(CaDiCaL REQUIRED)
475 libcvc4_link_libraries(${CaDiCaL_LIBRARIES})
476 libcvc4_include_directories(${CaDiCaL_INCLUDE_DIR})
477 add_definitions(-DCVC4_USE_CADICAL)
481 set(GPL_LIBS "${GPL_LIBS} cln")
482 find_package(CLN 1.2.2 REQUIRED)
483 libcvc4_link_libraries(${CLN_LIBRARIES})
484 libcvc4_include_directories(${CLN_INCLUDE_DIR})
485 set(CVC4_USE_CLN_IMP 1)
486 set(CVC4_USE_GMP_IMP 0)
488 set(CVC4_USE_CLN_IMP 0)
489 set(CVC4_USE_GMP_IMP 1)
492 if(USE_CRYPTOMINISAT)
493 # CryptoMiniSat requires pthreads support
494 set(THREADS_PREFER_PTHREAD_FLAG ON)
495 find_package(Threads REQUIRED)
496 if(THREADS_HAVE_PTHREAD_ARG)
497 add_c_cxx_flag(-pthread)
499 set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
500 find_package(CryptoMiniSat REQUIRED)
501 libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES})
502 libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR})
503 add_definitions(-DCVC4_USE_CRYPTOMINISAT)
507 set(GPL_LIBS "${GPL_LIBS} glpk")
508 set(GLPK_HOME ${GLPK_DIR})
509 find_package(GLPK REQUIRED)
510 libcvc4_link_libraries(${GLPK_LIBRARIES})
511 libcvc4_include_directories(${GLPK_INCLUDE_DIR})
512 add_definitions(-DCVC4_USE_GLPK)
516 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
517 set(LFSC_HOME ${LFSC_DIR})
518 find_package(LFSC REQUIRED)
519 libcvc4_link_libraries(${LFSC_LIBRARIES})
520 libcvc4_include_directories(${LFSC_INCLUDE_DIR})
521 add_definitions(-DCVC4_USE_LFSC)
528 find_package(Readline REQUIRED)
529 set(HAVE_LIBREADLINE 1)
530 if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
531 set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
536 set(SymFPU_HOME ${SYMFPU_DIR})
537 find_package(SymFPU REQUIRED)
538 libcvc4_include_directories(${SymFPU_INCLUDE_DIR})
539 add_definitions(-DCVC4_USE_SYMFPU)
540 set(CVC4_USE_SYMFPU 1)
542 set(CVC4_USE_SYMFPU 0)
548 "Bad configuration detected: BSD-licensed code only, but also requested "
549 "GPLed libraries: ${GPL_LIBS}")
554 #-----------------------------------------------------------------------------#
556 include(GetGitRevisionDescription)
557 get_git_head_revision(GIT_REFSPEC GIT_SHA1)
558 git_local_changes(GIT_IS_DIRTY)
559 if(${GIT_IS_DIRTY} STREQUAL "DIRTY")
560 set(GIT_IS_DIRTY "true")
562 set(GIT_IS_DIRTY "false")
566 COMMAND "${GIT_EXECUTABLE}" rev-parse --abbrev-ref HEAD
567 OUTPUT_VARIABLE GIT_BRANCH
568 OUTPUT_STRIP_TRAILING_WHITESPACE
571 #-----------------------------------------------------------------------------#
572 # Generate CVC4's cvc4autoconfig.h header
574 include(ConfigureCVC4)
575 configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
576 include_directories(${CMAKE_CURRENT_BINARY_DIR})
578 #-----------------------------------------------------------------------------#
581 # signatures needs to come before src since it adds source files to libcvc4.
583 add_subdirectory(proofs/signatures)
586 add_subdirectory(doc)
587 add_subdirectory(src)
589 if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
590 add_subdirectory(src/bindings)
593 if(BUILD_BINDINGS_JAVA)
594 add_subdirectory(test/java)
597 add_subdirectory(test/regress)
598 add_subdirectory(test/system)
600 if(ENABLE_UNIT_TESTING)
601 add_subdirectory(test/unit)
604 #-----------------------------------------------------------------------------#
605 # Print build configuration
606 if(CVC4_BUILD_PROFILE_PRODUCTION)
607 set(CVC4_BUILD_PROFILE_STRING "production")
608 elseif(CVC4_BUILD_PROFILE_DEBUG)
609 set(CVC4_BUILD_PROFILE_STRING "debug")
610 elseif(CVC4_BUILD_PROFILE_TESTING)
611 set(CVC4_BUILD_PROFILE_STRING "testing")
612 elseif(CVC4_BUILD_PROFILE_COMPETITION)
613 set(CVC4_BUILD_PROFILE_STRING "competition")
616 # Get all definitions added via add_definitions to print it below
617 get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
618 string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
620 # Print configuration of 2/3-valued option 'var' with prefix 'str'
621 macro(print_config str var)
622 if(${var} STREQUAL "ON")
623 set(OPT_VAL_STR "on")
624 elseif(${var} STREQUAL "OFF")
625 set(OPT_VAL_STR "off")
626 elseif(${var} STREQUAL "IGNORE")
627 set(OPT_VAL_STR "default")
629 message("${str} ${OPT_VAL_STR}")
632 message("CVC4 ${CVC4_RELEASE_STRING}")
634 message("Build profile : ${CVC4_BUILD_PROFILE_STRING}")
636 print_config("GPL :" ENABLE_GPL)
637 print_config("Best configuration :" ENABLE_BEST)
638 print_config("Optimized :" ENABLE_OPTIMIZED)
639 print_config("Optimization level :" OPTIMIZATION_LEVEL)
641 print_config("Assertions :" ENABLE_ASSERTIONS)
642 print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS)
643 print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
645 print_config("Dumping :" ENABLE_DUMPING)
646 print_config("Muzzle :" ENABLE_MUZZLE)
647 print_config("Proofs :" ENABLE_PROOFS)
648 print_config("Replay :" ENABLE_REPLAY)
649 print_config("Statistics :" ENABLE_STATISTICS)
650 print_config("Tracing :" ENABLE_TRACING)
652 print_config("Asan :" ENABLE_ASAN)
653 print_config("Coverage (gcov) :" ENABLE_COVERAGE)
654 print_config("Profiling (gprof) :" ENABLE_PROFILING)
655 print_config("Unit tests :" ENABLE_UNIT_TESTING)
656 print_config("Valgrind :" ENABLE_VALGRIND)
658 print_config("Shared libs :" ENABLE_SHARED)
659 print_config("Java bindings :" BUILD_BINDINGS_JAVA)
660 print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
662 print_config("Portfolio :" ENABLE_PORTFOLIO)
664 print_config("ABC :" USE_ABC)
665 print_config("CaDiCaL :" USE_CADICAL)
666 print_config("CryptoMiniSat :" USE_CRYPTOMINISAT)
667 print_config("GLPK :" USE_GLPK)
668 print_config("LFSC :" USE_LFSC)
671 message("MP library : cln")
673 message("MP library : gmp")
675 print_config("Readline :" ${USE_READLINE})
676 print_config("SymFPU :" ${USE_SYMFPU})
679 message("ABC dir : ${ABC_DIR}")
682 message("ANTLR dir : ${ANTLR_DIR}")
685 message("CADICAL dir : ${CADICAL_DIR}")
687 if(CRYPTOMINISAT_DIR)
688 message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}")
691 message("GLPK dir : ${GLPK_DIR}")
694 message("GMP dir : ${GMP_DIR}")
697 message("LFSC dir : ${LFSC_DIR}")
700 message("SYMFPU dir : ${SYMFPU_DIR}")
703 message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}")
704 message("CXXFLAGS : ${CMAKE_CXX_FLAGS}")
705 message("CFLAGS : ${CMAKE_C_FLAGS}")
706 #message("LIBS : ${LIBS}")
707 #message("LDFLAGS : ${LDFLAGS}")
709 #message("libcvc4 version : ${{CVC4_LIBRARY_VERSION}")
710 #message("libcvc4parser version : ${CVC4_PARSER_LIBRARY_VERSION}")
711 #message("libcvc4compat version : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}")
712 #message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}")
714 message("Install prefix : ${CMAKE_INSTALL_PREFIX}")
719 "CVC4 license : GPLv3 (due to optional libraries; see below)"
722 "Please note that CVC4 will be built against the following GPLed libraries:"
726 "As these libraries are covered under the GPLv3, so is this build of CVC4."
728 "CVC4 is also available to you under the terms of the (modified) BSD license."
730 "If you prefer to license CVC4 under those terms, please configure CVC4 to"
732 "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
736 "CVC4 license : modified BSD"
739 "Note that this configuration is NOT built against any GPL'ed libraries, so"
741 "it is covered by the (modified) BSD license. This is, however, not the best"
743 "performing configuration of CVC4. To build against GPL'ed libraries which"
745 "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
750 message("Now just type make, followed by make check or make install.")