-cmake_minimum_required (VERSION 3.0.1)
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+## Mathias Preiner, Aina Niemetz, Gereon Kremer
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved. See the file COPYING in the top-level source
+## directory for licensing information.
+##
+cmake_minimum_required(VERSION 3.9)
#-----------------------------------------------------------------------------#
+# Project configuration
project(cvc4)
-# Major component of the version of CVC4.
-set(CVC4_MAJOR 1)
-# Minor component of the version of CVC4.
-set(CVC4_MINOR 7)
-# Release component of the version of CVC4.
-set(CVC4_RELEASE 0)
+include(GNUInstallDirs)
+
+set(CVC4_MAJOR 1) # Major component of the version of CVC4.
+set(CVC4_MINOR 9) # Minor component of the version of CVC4.
+set(CVC4_RELEASE 0) # Release component of the version of CVC4.
+
# Extraversion component of the version of CVC4.
set(CVC4_EXTRAVERSION "-prerelease")
+# Shared library versioning. Increment SOVERSION for every new CVC4 release.
+set(CVC4_SOVERSION 7)
+
# Full release string for CVC4.
if(CVC4_RELEASE)
- set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
+ set(CVC4_RELEASE_STRING
+ "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}")
else()
set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}")
endif()
-# Define to the full name of this package.
-set(PACKAGE_NAME "${PROJECT_NAME}")
+set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
+set(CMAKE_C_STANDARD 99)
+set(CMAKE_CXX_STANDARD 17)
+set(CMAKE_CXX_EXTENSIONS OFF)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
-# Shared library versioning. Increment SOVERSION for every new CVC4 release.
-set(CVC4_VERSION "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}")
-set(CVC4_SOVERSION 5)
-
-#### These defines are only use in autotools make files, will likely be
-#### replaced with corresponding CPack stuff
-## Define to the full name and version of this package.
-#set(PACKAGE_STRING "${PROJECT_NAME} ${CVC4_RELEASE_STRING}")
-## Define to the one symbol short name of this package.
-#set(PACKAGE_TARNAME "${PROJECT_NAME}")
-## Define to the home page for this package.
-#set(PACKAGE_URL "")
-## Define to the version of this package.
-#set(PACKAGE_VERSION "${CVC4_RELEASE_STRING}")
-## Define to the address where bug reports for this package should be sent.
-#set(PACKAGE_BUGREPORT "cvc4-bugs@cs.stanford.edu")
+# Generate compile_commands.json, which can be used for various code completion
+# plugins.
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
#-----------------------------------------------------------------------------#
+# Policies
-set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
-set(CMAKE_C_STANDARD 99)
-set(CMAKE_CXX_STANDARD 11)
+# Required for FindGLPK since it sets CMAKE_REQUIRED_LIBRARIES
+if(POLICY CMP0075)
+ cmake_policy(SET CMP0075 NEW)
+endif()
#-----------------------------------------------------------------------------#
-# Macros
-
-include(CheckCCompilerFlag)
-include(CheckCXXCompilerFlag)
+# Tell CMake where to find our dependencies
-macro(add_c_flag flag)
- if(CMAKE_C_FLAGS)
- set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${flag}")
- else()
- set(CMAKE_C_FLAGS "${flag}")
- endif()
- message(STATUS "Configuring with C flag '${flag}'")
-endmacro()
+if(ABC_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${ABC_DIR}")
+endif()
+if(ANTLR_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${ANTLR_DIR}")
+endif()
+if(CADICAL_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${CADICAL_DIR}")
+endif()
+if(CRYPTOMINISAT_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${CRYPTOMINISAT_DIR}")
+endif()
+if(CXXTEST_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${CXXTEST_DIR}")
+endif()
+if(DRAT2ER_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${DRAT2ER_DIR}")
+endif()
+if(GLPK_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}")
+endif()
+if(GMP_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${GMP_DIR}")
+endif()
+if(KISSAT_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${KISSAT_DIR}")
+endif()
+if(LFSC_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}")
+endif()
+if(POLY_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${POLY_DIR}")
+endif()
+if(SYMFPU_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${SYMFPU_DIR}")
+endif()
-macro(add_cxx_flag flag)
- if(CMAKE_CXX_FLAGS)
- set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${flag}")
- else()
- set(CMAKE_CXX_FLAGS "${flag}")
- endif()
- message(STATUS "Configuring with CXX flag '${flag}'")
-endmacro()
-
-macro(add_c_cxx_flag flag)
- add_c_flag(${flag})
- add_cxx_flag(${flag})
-endmacro()
-
-macro(add_check_c_flag flag)
- string(REGEX REPLACE "[-=]" "_" flagname ${flag})
- check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
- if(HAVE_FLAG${flagname})
- add_c_flag(${flag})
- endif()
-endmacro()
+# By default the contrib/get-* scripts install dependencies to deps/install.
+list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps/install")
-macro(add_check_cxx_flag flag)
- string(REGEX REPLACE "[-=]" "_" flagname ${flag})
- check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
- if(HAVE_FLAG${flagname})
- add_cxx_flag(${flag})
- endif()
-endmacro()
-
-macro(add_check_c_cxx_flag flag)
- add_check_c_flag(${flag})
- add_check_cxx_flag(${flag})
-endmacro()
-
-macro(add_required_cxx_flag flag)
- string(REGEX REPLACE "[-=]" "_" flagnamename ${flag})
- check_cxx_compiler_flag("${flag}" HAVE_FLAG${flagname})
- if (NOT HAVE_FLAG${flagname})
- message(FATAL_ERROR "Required compiler flag ${flag} not supported")
- endif()
- add_cxx_flag(${flag})
-endmacro()
-
-macro(add_required_c_flag flag)
- string(REGEX REPLACE "[-=]" "_" flagname ${flag})
- check_c_compiler_flag("${flag}" HAVE_FLAG${flagname})
- if (NOT HAVE_FLAG${flagname})
- message(FATAL_ERROR "Required compiler flag ${flag} not supported")
- endif()
- add_c_flag(${flag})
-endmacro()
-
-macro(add_required_c_cxx_flag flag)
- add_required_c_flag(${flag})
- add_required_cxx_flag(${flag})
-endmacro()
-
-# Collect all libraries that must be linked against libcvc4. These will be
-# actually linked in src/CMakeLists.txt with target_link_libaries(...).
-macro(libcvc4_link_libraries library)
- set(LIBCVC4_LIBRARIES ${LIBCVC4_LIBRARIES} ${library})
-endmacro()
-
-# Collect all include directories that are required for libcvc4. These will be
-# actually included in src/CMakeLists.txt with target_include_directories(...).
-macro(libcvc4_include_directories dirs)
- set(LIBCVC4_INCLUDES ${LIBCVC4_INCLUDES} ${dirs})
-endmacro()
-
-# CVC4 Boolean options are three-valued to detect if an option was set by the
-# user. The available values are: IGNORE (default), ON, OFF
-# Default options do not override options that were set by the user, i.e.,
-# cvc4_set_option only sets an option if it's value is still IGNORE.
-# This e.g., allows the user to disable proofs for debug builds (where proofs
-# are enabled by default).
-macro(cvc4_option var description)
- set(${var} IGNORE CACHE STRING "${description}")
- # Provide drop down menu options in cmake-gui
- set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF)
-endmacro()
+#-----------------------------------------------------------------------------#
-# Only set option if the user did not set an option.
-macro(cvc4_set_option var value)
- if(${var} STREQUAL "IGNORE")
- set(${var} ${value})
- endif()
-endmacro()
+include(Helpers)
#-----------------------------------------------------------------------------#
# User options
# General build options
#
-# >> 3-valued: INGORE ON OFF
+# >> 3-valued: IGNORE ON OFF
# > allows to detect if set by user (default: IGNORE)
# > only necessary for options set for build types
-cvc4_option(ENABLE_ASAN "Enable ASAN build")
-cvc4_option(ENABLE_ASSERTIONS "Enable assertions")
-cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
-cvc4_option(ENABLE_DUMPING "Enable dumping")
-cvc4_option(ENABLE_MUZZLE "Supress ALL non-result output")
-cvc4_option(ENABLE_OPTIMIZED "Enable optimization")
-cvc4_option(ENABLE_PORTFOLIO "Enable portfolio support")
-cvc4_option(ENABLE_PROOFS "Enable proof support")
-cvc4_option(ENABLE_REPLAY "Enable the replay feature")
-cvc4_option(ENABLE_STATISTICS "Enable statistics")
-cvc4_option(ENABLE_TRACING "Enable tracing")
-cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing")
-cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation")
-cvc4_option(ENABLE_SHARED "Build as shared library")
+cvc4_option(ENABLE_ASAN "Enable ASAN build")
+cvc4_option(ENABLE_UBSAN "Enable UBSan build")
+cvc4_option(ENABLE_TSAN "Enable TSan build")
+cvc4_option(ENABLE_ASSERTIONS "Enable assertions")
+cvc4_option(ENABLE_COMP_INC_TRACK
+ "Enable optimizations for incremental SMT-COMP tracks")
+cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
+cvc4_option(ENABLE_DUMPING "Enable dumping")
+cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output")
+cvc4_option(ENABLE_PROOFS "Enable proof support")
+cvc4_option(ENABLE_STATISTICS "Enable statistics")
+cvc4_option(ENABLE_TRACING "Enable tracing")
+cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing")
+cvc4_option(ENABLE_VALGRIND "Enable valgrind instrumentation")
+cvc4_option(ENABLE_SHARED "Build as shared library")
+cvc4_option(ENABLE_STATIC_BINARY
+ "Build static binaries with statically linked system libraries")
# >> 2-valued: ON OFF
# > for options where we don't need to detect if set by user (default: OFF)
option(ENABLE_BEST "Enable dependencies known to give best performance")
# Optional dependencies
#
-# >> 3-valued: INGORE ON OFF
+# >> 3-valued: IGNORE ON OFF
# > allows to detect if set by user (default: IGNORE)
# > only necessary for options set for ENABLE_BEST
-cvc4_option(USE_ABC "Use ABC for AIG bit-blasting")
-cvc4_option(USE_CLN "Use CLN instead of GMP")
-cvc4_option(USE_GLPK "Use GLPK simplex solver")
-cvc4_option(USE_READLINE "Use readline for better interactive support")
+cvc4_option(USE_ABC "Use ABC for AIG bit-blasting")
+cvc4_option(USE_CADICAL "Use CaDiCaL SAT solver")
+cvc4_option(USE_CLN "Use CLN instead of GMP")
+cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
+cvc4_option(USE_GLPK "Use GLPK simplex solver")
+cvc4_option(USE_KISSAT "Use Kissat SAT solver")
+cvc4_option(USE_EDITLINE "Use Editline for better interactive support")
# >> 2-valued: ON OFF
# > for options where we don't need to detect if set by user (default: OFF)
-option(USE_CADICAL "Use CaDiCaL SAT solver")
-option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
-option(USE_LFSC "Use LFSC proof checker")
-option(USE_SYMFPU "Use SymFPU for floating point support")
+option(USE_DRAT2ER "Include drat2er for making eager BV proofs")
+option(USE_LFSC "Use LFSC proof checker")
+option(USE_POLY "Use LibPoly for polynomial arithmetic")
+option(USE_SYMFPU "Use SymFPU for floating point support")
+option(USE_PYTHON2 "Force Python 2 (deprecated)")
# Custom install directories for dependencies
# If no directory is provided by the user, we first check if the dependency was
set(ANTLR_DIR "" CACHE STRING "Set ANTLR3 install directory")
set(CADICAL_DIR "" CACHE STRING "Set CaDiCaL install directory")
set(CRYPTOMINISAT_DIR "" CACHE STRING "Set CryptoMiniSat install directory")
+set(CXXTEST_DIR "" CACHE STRING "Set CxxTest install directory")
+set(DRAT2ER_DIR "" CACHE STRING "Set drat2er install directory")
set(GLPK_DIR "" CACHE STRING "Set GLPK install directory")
set(GMP_DIR "" CACHE STRING "Set GMP install directory")
+set(KISSAT_DIR "" CACHE STRING "Set Kissat install directory")
set(LFSC_DIR "" CACHE STRING "Set LFSC install directory")
+set(POLY_DIR "" CACHE STRING "Set LibPoly install directory")
set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory")
-# Supported language bindings
-option(BUILD_BINDINGS_JAVA "Build Java bindings")
-option(BUILD_BINDINGS_PYTHON "Build Python bindings")
+# Prepend binaries with prefix on make install
+set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install")
-# All bindings: c,java,csharp,perl,php,python,ruby,tcl,ocaml
+# Supprted language bindings based on new C++ API
+option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ")
+option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ")
+# Build limitations
+option(BUILD_LIB_ONLY "Only build the library")
#-----------------------------------------------------------------------------#
# Internal cmake variables
-set(OPT_LEVEL 3)
+set(OPTIMIZATION_LEVEL 3)
set(GPL_LIBS "")
-set(BUILD_TYPES Production Debug Testing Competition)
-
-#-----------------------------------------------------------------------------#
-# CVC4 build variables
-
-set(CVC4_DEBUG 0)
-set(CVC4_BUILD_PROFILE_PRODUCTION 0)
-set(CVC4_BUILD_PROFILE_DEBUG 0)
-set(CVC4_BUILD_PROFILE_TESTING 0)
-set(CVC4_BUILD_PROFILE_COMPETITION 0)
-
#-----------------------------------------------------------------------------#
-# Compiler flags
+# Determine number of threads available, used to configure (default) parallel
+# execution of custom test targets (can be overriden with ARGS=-jN).
-add_check_c_cxx_flag("-O${OPT_LEVEL}")
-add_check_c_flag("-fexceptions")
-add_check_c_cxx_flag("-Wno-deprecated")
-add_check_cxx_flag("-Wsuggest-override")
-add_check_cxx_flag("-Wnon-virtual-dtor")
+include(ProcessorCount)
+ProcessorCount(CTEST_NTHREADS)
+if(CTEST_NTHREADS EQUAL 0)
+ set(CTEST_NTHREADS 1)
+endif()
#-----------------------------------------------------------------------------#
# Build types
-if(ENABLE_ASAN)
+# Note: Module CodeCoverage requires the name of the debug build to conform
+# to cmake standards (first letter uppercase).
+set(BUILD_TYPES Production Debug Testing Competition)
+
+if(ENABLE_ASAN OR ENABLE_UBSAN OR ENABLE_TSAN)
set(CMAKE_BUILD_TYPE Debug)
endif()
# Set the default build type to Production
if(NOT CMAKE_BUILD_TYPE)
- set(CMAKE_BUILD_TYPE Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
+ set(CMAKE_BUILD_TYPE
+ Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
# Provide drop down menu options in cmake-gui
set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
endif()
-message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
-if(CMAKE_BUILD_TYPE STREQUAL "Debug")
- include(ConfigDebug)
-elseif(CMAKE_BUILD_TYPE STREQUAL "Production")
- include(ConfigProduction)
-elseif(CMAKE_BUILD_TYPE STREQUAL "Testing")
- include(ConfigTesting)
-elseif(CMAKE_BUILD_TYPE STREQUAL "Competition")
- include(ConfigCompetition)
- # enable_static=yes
- #TODO
- # enable_static_binary=yes
- #TODO
+# Check if specified build type is valid.
+list(FIND BUILD_TYPES ${CMAKE_BUILD_TYPE} FOUND_BUILD_TYPE)
+if(${FOUND_BUILD_TYPE} EQUAL -1)
+ message(FATAL_ERROR
+ "'${CMAKE_BUILD_TYPE}' is not a valid build type. "
+ "Available builds are: ${BUILD_TYPES}")
endif()
+message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
+include(Config${CMAKE_BUILD_TYPE})
+
+#-----------------------------------------------------------------------------#
+# Compiler flags
+
+add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
+add_check_c_cxx_flag("-Wall")
+add_check_c_flag("-fexceptions")
+add_check_c_cxx_flag("-Wno-deprecated")
+add_check_cxx_flag("-Wsuggest-override")
+add_check_cxx_flag("-Wnon-virtual-dtor")
+add_check_c_cxx_flag("-Wimplicit-fallthrough")
+add_check_c_cxx_flag("-Wshadow")
+
+# Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
+# cdlist.h warnings. Remove when fixed.
+add_check_cxx_flag("-Wno-class-memaccess")
+
+if (WIN32)
+ set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000")
+endif ()
+
+#-----------------------------------------------------------------------------#
+# Use ld.gold if available
+
+execute_process(COMMAND ${CMAKE_C_COMPILER}
+ -fuse-ld=gold
+ -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION)
+if ("${LD_VERSION}" MATCHES "GNU gold")
+ string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold")
+ string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold")
+ string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold")
+ message(STATUS "Using GNU gold linker.")
+endif ()
+
#-----------------------------------------------------------------------------#
# Option defaults (three-valued options (cvc4_option(...)))
+#
+# These options are only set if their value is IGNORE. Otherwise, the user
+# already set the option, which we don't want to overwrite.
-cvc4_set_option(ENABLE_PORTFOLIO OFF)
-cvc4_set_option(ENABLE_SHARED ON)
-cvc4_set_option(ENABLE_VALGRIND OFF)
-cvc4_set_option(USE_ABC OFF)
-cvc4_set_option(USE_GLPK OFF)
-cvc4_set_option(USE_READLINE OFF)
+if(ENABLE_STATIC_BINARY)
+ cvc4_set_option(ENABLE_SHARED OFF)
+else()
+ cvc4_set_option(ENABLE_SHARED ON)
+endif()
#-----------------------------------------------------------------------------#
# Set options for best configuration
-if (ENABLE_BEST)
+if(ENABLE_BEST)
cvc4_set_option(USE_ABC ON)
+ cvc4_set_option(USE_CADICAL ON)
cvc4_set_option(USE_CLN ON)
+ cvc4_set_option(USE_CRYPTOMINISAT ON)
cvc4_set_option(USE_GLPK ON)
- cvc4_set_option(USE_READLINE ON)
+ cvc4_set_option(USE_EDITLINE ON)
endif()
-#-----------------------------------------------------------------------------#
+# Only enable unit testing if assertions are enabled. Otherwise, unit tests
+# that expect AssertionException to be thrown will fail.
+if(NOT ENABLE_ASSERTIONS)
+ message(WARNING "Disabling unit tests since assertions are disabled.")
+ set(ENABLE_UNIT_TESTING OFF)
+endif()
+#-----------------------------------------------------------------------------#
+# Shared/static libraries
+#
# This needs to be set before any find_package(...) command since we want to
# search for static libraries with suffix .a.
-if(NOT ENABLE_SHARED)
- set(CMAKE_FIND_LIBRARY_SUFFIXES ".a")
- set(CMAKE_EXE_LINKER_FLAGS "-static")
- set(BUILD_SHARED_LIBS OFF)
-endif()
-find_package(PythonInterp REQUIRED)
-
-set(ANTLR_HOME ${ANTLR_DIR})
-find_package(ANTLR REQUIRED)
+if(ENABLE_SHARED)
+ set(BUILD_SHARED_LIBS ON)
+ if(ENABLE_STATIC_BINARY)
+ set(ENABLE_STATIC_BINARY OFF)
+ message(WARNING "Disabling static binary since shared build is enabled.")
+ endif()
-# Java runtime is required for ANTLR
-find_package(Java COMPONENTS Runtime REQUIRED)
+ # Embed the installation prefix as an RPATH in the executable such that the
+ # linker can find our libraries (such as libcvc4parser) when executing the
+ # cvc4 binary. This is for example useful when installing CVC4 with a custom
+ # prefix on macOS (e.g. when using homebrew in a non-standard directory). If
+ # we do not set this option, then the linker will not be able to find the
+ # required libraries when trying to run CVC4.
+ #
+ # Also embed the installation prefix of the installed contrib libraries as an
+ # RPATH. This allows to install a dynamically linked binary that depends on
+ # dynamically linked libraries. This is dangerous, as the installed binary
+ # breaks if the contrib library is removed or changes in other ways, we thus
+ # print a big warning and only allow if installing to a custom installation
+ # prefix.
+ #
+ # More information on RPATH in CMake:
+ # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
+ set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
+else()
+ # When building statically, we *only* want static archives/libraries
+ if (WIN32)
+ set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a)
+ else()
+ set(CMAKE_FIND_LIBRARY_SUFFIXES .a)
+ endif()
+ set(BUILD_SHARED_LIBS OFF)
+ cvc4_set_option(ENABLE_STATIC_BINARY ON)
-set(GMP_HOME ${GMP_DIR})
-find_package(GMP REQUIRED)
-libcvc4_link_libraries(${GMP_LIBRARIES})
-libcvc4_include_directories(${GMP_INCLUDE_DIR})
+ # Never build unit tests as static binaries, otherwise we'll end up with
+ # ~300MB per unit test.
+ if(ENABLE_UNIT_TESTING)
+ message(WARNING "Disabling unit tests since static build is enabled.")
+ set(ENABLE_UNIT_TESTING OFF)
+ endif()
+ if (BUILD_BINDINGS_PYTHON)
+ message(FATAL_ERROR "Building Python bindings is not possible "
+ "when building statically")
+ endif()
+endif()
#-----------------------------------------------------------------------------#
# Enable the ctest testing framework
+# This needs to be enabled here rather than in subdirectory test in order to
+# allow calling ctest from the root build directory.
enable_testing()
#-----------------------------------------------------------------------------#
+# Check GCC version.
+#
+# GCC version 4.5.1 builds MiniSat incorrectly with -O2, which results in
+# incorrect answers.
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
+ execute_process(
+ COMMAND ${CMAKE_CXX_COMPILER} -dumpversion
+ OUTPUT_VARIABLE GCC_VERSION
+ OUTPUT_STRIP_TRAILING_WHITESPACE)
+ if(GCC_VERSION VERSION_EQUAL "4.5.1")
+ message(FATAL_ERROR
+ "GCC 4.5.1's optimizer is known to build MiniSat incorrectly "
+ "(and by extension CVC4).")
+ endif()
+endif()
+
+#-----------------------------------------------------------------------------#
+# Check options, find packages and configure build.
-if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
- set(BUILD_BINDINGS TRUE)
+if(USE_PYTHON2)
+ find_package(PythonInterp 2.7 REQUIRED)
+else()
+ find_package(PythonInterp 3 REQUIRED)
endif()
+find_package(GMP REQUIRED)
+
if(ENABLE_ASAN)
- set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address)
+ # -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
+ # otherwise the -fsanitize=address check will fail while linking.
+ set(CMAKE_REQUIRED_FLAGS -fsanitize=address)
add_required_c_cxx_flag("-fsanitize=address")
- unset(CMAKE_REQUIRED_LIBRARIES)
+ unset(CMAKE_REQUIRED_FLAGS)
add_required_c_cxx_flag("-fno-omit-frame-pointer")
add_check_c_cxx_flag("-fsanitize-recover=address")
endif()
+if(ENABLE_UBSAN)
+ add_required_c_cxx_flag("-fsanitize=undefined")
+ add_definitions(-DCVC4_USE_UBSAN)
+endif()
+
+if(ENABLE_TSAN)
+ # -fsanitize=thread requires CMAKE_REQUIRED_FLAGS to be explicitely set,
+ # otherwise the -fsanitize=thread check will fail while linking.
+ set(CMAKE_REQUIRED_FLAGS -fsanitize=thread)
+ add_required_c_cxx_flag("-fsanitize=thread")
+ unset(CMAKE_REQUIRED_FLAGS)
+endif()
+
if(ENABLE_ASSERTIONS)
add_definitions(-DCVC4_ASSERTIONS)
+else()
+ add_definitions(-DNDEBUG)
endif()
if(ENABLE_COVERAGE)
include(CodeCoverage)
APPEND_COVERAGE_COMPILER_FLAGS()
add_definitions(-DCVC4_COVERAGE)
- setup_target_for_coverage_lcov(
+ # Note: The ctest command returns a non-zero exit code if tests fail or run
+ # into a timeout. As a consequence, the coverage report is not generated. To
+ # prevent this we always return with exit code 0 after the ctest command has
+ # finished.
+ setup_target_for_coverage_gcovr_html(
NAME coverage
- EXECUTABLE ctest $(ARGS)
- DEPENDENCIES cvc4-bin)
+ EXECUTABLE
+ ctest -j${CTEST_NTHREADS} -LE "example"
+ --output-on-failure $$ARGS || exit 0
+ DEPENDS
+ build-tests)
endif()
if(ENABLE_DEBUG_CONTEXT_MM)
add_definitions(-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER)
endif()
-if(ENABLE_DUMPING)
- add_definitions(-DCVC4_DUMPING)
-else()
- add_definitions(-DNDEBUG)
-endif()
-
if(ENABLE_DEBUG_SYMBOLS)
add_check_c_cxx_flag("-ggdb3")
endif()
+if(ENABLE_COMP_INC_TRACK)
+ add_definitions(-DCVC4_SMTCOMP_APPLICATION_TRACK)
+endif()
+
if(ENABLE_MUZZLE)
add_definitions(-DCVC4_MUZZLE)
endif()
-if(ENABLE_PORTFOLIO)
- find_package(Boost 1.50.0 REQUIRED COMPONENTS thread)
- # Disable CLN for portfolio builds since it is not thread safe (uses an
- # unlocked hash table internally).
- set(USE_CLN OFF)
- set(THREADS_PREFER_PTHREAD_FLAG ON)
- find_package(Threads REQUIRED)
- if(THREADS_HAVE_PTHREAD_ARG)
- add_c_cxx_flag(-pthread)
- endif()
- add_definitions(-DCVC4_PORTFOLIO)
- set(BOOST_HAS_THREAD_ATTR 1)
+if(ENABLE_DUMPING)
+ add_definitions(-DCVC4_DUMPING)
endif()
if(ENABLE_PROFILING)
if(ENABLE_PROOFS)
set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
add_definitions(-DCVC4_PROOF)
- set(CVC4_PROOF 1)
- libcvc4_link_libraries(signatures)
-endif()
-
-if(ENABLE_REPLAY)
- add_definitions(-DCVC4_REPLAY)
endif()
if(ENABLE_TRACING)
add_definitions(-DCVC4_TRACING)
- set(CVC4_TRACING 1)
-endif()
-
-if(ENABLE_UNIT_TESTING)
- find_package(CxxTest REQUIRED)
- # Force shared libs for unit tests, static libs with unit tests are not
- # working right now.
- set(ENABLE_SHARED ON)
-endif()
-
-if(ENABLE_SHARED)
- set(BUILD_SHARED_LIBS ON)
endif()
if(ENABLE_STATISTICS)
endif()
if(ENABLE_VALGRIND)
- #TODO check if valgrind available
+ find_package(Valgrind REQUIRED)
add_definitions(-DCVC4_VALGRIND)
endif()
if(USE_ABC)
- set(ABC_HOME "${ABC_DIR}")
find_package(ABC REQUIRED)
- libcvc4_link_libraries(${ABC_LIBRARIES})
- libcvc4_include_directories(${ABC_INCLUDE_DIR})
add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
endif()
if(USE_CADICAL)
- set(CaDiCaL_HOME ${CADICAL_DIR})
find_package(CaDiCaL REQUIRED)
- libcvc4_link_libraries(${CaDiCaL_LIBRARIES})
- libcvc4_include_directories(${CaDiCaL_INCLUDE_DIR})
add_definitions(-DCVC4_USE_CADICAL)
endif()
if(USE_CLN)
set(GPL_LIBS "${GPL_LIBS} cln")
find_package(CLN 1.2.2 REQUIRED)
- libcvc4_link_libraries(${CLN_LIBRARIES})
- libcvc4_include_directories(${CLN_INCLUDE_DIR})
set(CVC4_USE_CLN_IMP 1)
set(CVC4_USE_GMP_IMP 0)
else()
if(THREADS_HAVE_PTHREAD_ARG)
add_c_cxx_flag(-pthread)
endif()
- set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
find_package(CryptoMiniSat REQUIRED)
- libcvc4_link_libraries(${CryptoMiniSat_LIBRARIES})
- libcvc4_include_directories(${CryptoMiniSat_INCLUDE_DIR})
add_definitions(-DCVC4_USE_CRYPTOMINISAT)
endif()
+if(USE_DRAT2ER)
+ find_package(Drat2Er REQUIRED)
+ add_definitions(-DCVC4_USE_DRAT2ER)
+endif()
+
if(USE_GLPK)
set(GPL_LIBS "${GPL_LIBS} glpk")
- set(GLPK_HOME ${GLPK_DIR})
find_package(GLPK REQUIRED)
- libcvc4_link_libraries(${GLPK_LIBRARIES})
- libcvc4_include_directories(${GLPK_INCLUDE_DIR})
add_definitions(-DCVC4_USE_GLPK)
endif()
+if(USE_KISSAT)
+ find_package(Kissat REQUIRED)
+ add_definitions(-DCVC4_USE_KISSAT)
+endif()
+
if(USE_LFSC)
set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
- set(LFSC_HOME ${LFSC_DIR})
find_package(LFSC REQUIRED)
- libcvc4_link_libraries(${LFSC_LIBRARIES})
- libcvc4_include_directories(${LFSC_INCLUDE_DIR})
add_definitions(-DCVC4_USE_LFSC)
- set(CVC4_USE_LFSC 1)
+endif()
+
+if(USE_POLY)
+ find_package(Poly REQUIRED)
+ add_definitions(-DCVC4_USE_POLY)
+ set(CVC4_USE_POLY_IMP 1)
else()
- set(CVC4_USE_LFSC 0)
+ set(CVC4_USE_POLY_IMP 0)
endif()
-if(USE_READLINE)
- find_package(Readline REQUIRED)
- set(HAVE_LIBREADLINE 1)
- if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
- set(READLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
+if(USE_EDITLINE)
+ find_package(Editline REQUIRED)
+ set(HAVE_LIBEDITLINE 1)
+ if(Editline_COMPENTRY_FUNC_RETURNS_CHARPTR)
+ set(EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP 1)
endif()
endif()
if(USE_SYMFPU)
- set(SymFPU_HOME ${SYMFPU_DIR})
find_package(SymFPU REQUIRED)
- libcvc4_include_directories(${SymFPU_INCLUDE_DIR})
add_definitions(-DCVC4_USE_SYMFPU)
set(CVC4_USE_SYMFPU 1)
else()
endif()
#-----------------------------------------------------------------------------#
-
-set(VERSION "1.6.0-prerelease")
-string(TIMESTAMP MAN_DATE "%Y-%m-%d")
-
-#-----------------------------------------------------------------------------#
-
-include(GetGitRevisionDescription)
-get_git_head_revision(GIT_REFSPEC GIT_SHA1)
-git_local_changes(GIT_IS_DIRTY)
-if(${GIT_IS_DIRTY} STREQUAL "DIRTY")
- set(GIT_IS_DIRTY "true")
-else()
- set(GIT_IS_DIRTY "false")
-endif()
-
-execute_process(
- COMMAND "${GIT_EXECUTABLE}" rev-parse --abbrev-ref HEAD
- OUTPUT_VARIABLE GIT_BRANCH
- OUTPUT_STRIP_TRAILING_WHITESPACE
-)
-
-#-----------------------------------------------------------------------------#
+# Generate CVC4's cvc4autoconfig.h header
include(ConfigureCVC4)
-
-# Defined if using the CLN multi-precision arithmetic library.
-set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP})
-# Defined if using the GMP multi-precision arithmetic library.
-set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP})
-
-configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
+if(NOT ENABLE_SHARED)
+ set(CVC4_STATIC_BUILD ON)
+endif()
+configure_file(cvc4autoconfig.h.in cvc4autoconfig.h)
+unset(CVC4_STATIC_BUILD)
include_directories(${CMAKE_CURRENT_BINARY_DIR})
#-----------------------------------------------------------------------------#
+# Add subdirectories
+
+# signatures needs to come before src since it adds source files to libcvc4.
+if(ENABLE_PROOFS)
+ add_subdirectory(proofs/signatures)
+endif()
add_subdirectory(doc)
add_subdirectory(src)
-if(BUILD_BINDINGS)
- add_subdirectory(src/bindings)
+add_subdirectory(test)
+
+if(BUILD_BINDINGS_PYTHON)
+ set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR})
+ add_subdirectory(src/api/python)
endif()
+
if(BUILD_BINDINGS_JAVA)
- add_subdirectory(test/java)
-endif()
-add_subdirectory(test/regress)
-add_subdirectory(test/system)
-if(ENABLE_UNIT_TESTING)
- add_subdirectory(test/unit)
+ message(FATAL_ERROR
+ "Java bindings for the new API are not implemented yet.")
endif()
-if(ENABLE_PROOFS)
- add_subdirectory(proofs/signatures)
+#-----------------------------------------------------------------------------#
+# Package configuration
+#
+# Export CVC4 targets to support find_package(CVC4) in other cmake projects.
+
+include(CMakePackageConfigHelpers)
+
+# If we install a dynamically linked binary that also uses dynamically used
+# libraries from deps/install/lib, we need to be cautious. Changing these
+# shared libraries from deps/install/lib most probably breaks the binary.
+# We only allow such an installation for custom installation prefixes
+# (in the assumption that only reasonably experienced users use this and
+# also that custom installation prefixes are not used for longer periods of
+# time anyway). Also, we print a big warning with further instructions.
+if(NOT ENABLE_STATIC_BINARY)
+ # Get the libraries that cvc4 links against
+ get_target_property(libs cvc4 INTERFACE_LINK_LIBRARIES)
+ set(LIBS_SHARED_FROM_DEPS "")
+ foreach(lib ${libs})
+ # Filter out those that are linked dynamically and come from deps/install
+ if(lib MATCHES ".*/deps/install/lib/.*\.so")
+ list(APPEND LIBS_SHARED_FROM_DEPS ${lib})
+ endif()
+ endforeach()
+ list(LENGTH LIBS_SHARED_FROM_DEPS list_len)
+ # Check if we actually use such "dangerous" libraries
+ if(list_len GREATER 0)
+ # Print a generic warning
+ install(CODE "message(WARNING \"You are installing a dynamically linked \
+ binary of CVC4 which may be a problem if you are using any dynamically \
+ linked third-party library that you obtained through one of the \
+ contrib/get-xxx scripts. The binary uses the rpath mechanism to find these \
+ locally, hence executing such a contrib script removing the \
+ \\\"deps/install\\\" folder most probably breaks the installed binary! \
+ Consider installing the dynamically linked dependencies on your system \
+ manually or link cvc4 statically.\")")
+ # Print the libraries in question
+ foreach(lib ${LIBS_SHARED_FROM_DEPS})
+ install(CODE "message(WARNING \"The following library is used by the cvc4 binary: ${lib}\")")
+ endforeach()
+ # Check if we use a custom installation prefix
+ if(CMAKE_INSTALL_PREFIX STREQUAL "/usr/local")
+ install(CODE "message(FATAL_ERROR \"To avoid installing a \
+ soon-to-be-broken binary, system-wide installation is disabled if the \
+ binary depends on locally-built shared libraries.\")")
+ else()
+ install(CODE "message(WARNING \"You have selected a custom install \
+ directory ${CMAKE_INSTALL_PREFIX}, so we expect you understood the \
+ previous warning and know what you are doing.\")")
+ endif()
+ endif()
endif()
+install(EXPORT cvc4-targets
+ FILE CVC4Targets.cmake
+ NAMESPACE CVC4::
+ DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4)
+
+configure_package_config_file(
+ ${CMAKE_SOURCE_DIR}/cmake/CVC4Config.cmake.in
+ ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
+ INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4
+ PATH_VARS CMAKE_INSTALL_LIBDIR
+)
+
+write_basic_package_version_file(
+ ${CMAKE_CURRENT_BINARY_DIR}/CVC4ConfigVersion.cmake
+ VERSION ${CVC4_RELEASE_STRING}
+ COMPATIBILITY ExactVersion
+)
+
+install(FILES
+ ${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
+ ${CMAKE_BINARY_DIR}/CVC4ConfigVersion.cmake
+ DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4
+)
+
+
#-----------------------------------------------------------------------------#
# Print build configuration
-if(CVC4_BUILD_PROFILE_PRODUCTION)
- set(CVC4_BUILD_PROFILE_STRING "production")
-elseif(CVC4_BUILD_PROFILE_DEBUG)
- set(CVC4_BUILD_PROFILE_STRING "debug")
-elseif(CVC4_BUILD_PROFILE_TESTING)
- set(CVC4_BUILD_PROFILE_STRING "testing")
-elseif(CVC4_BUILD_PROFILE_COMPETITION)
- set(CVC4_BUILD_PROFILE_STRING "competition")
-endif()
-# Get all definitions added via add_definitions to print it below
+# Convert build type to lower case.
+string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING)
+
+# Get all definitions added via add_definitions.
get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
-# Print configuration of 2/3-valued option 'var' with prefix 'str'
-macro(print_config str var)
- if(${var} STREQUAL "ON")
- set(OPT_VAL_STR "on")
- elseif(${var} STREQUAL "OFF")
- set(OPT_VAL_STR "off")
- elseif(${var} STREQUAL "IGNORE")
- set(OPT_VAL_STR "default")
- endif()
- message("${str} ${OPT_VAL_STR}")
-endmacro()
-
message("CVC4 ${CVC4_RELEASE_STRING}")
message("")
-message("Build profile : ${CVC4_BUILD_PROFILE_STRING}")
+if(ENABLE_COMP_INC_TRACK)
+ message("Build profile : ${CVC4_BUILD_PROFILE_STRING} (incremental)")
+else()
+ message("Build profile : ${CVC4_BUILD_PROFILE_STRING}")
+endif()
message("")
-print_config("GPL :" ENABLE_GPL)
-print_config("Best configuration :" ENABLE_BEST)
-print_config("Optimized :" ENABLE_OPTIMIZED)
-print_config("Optimization level :" OPTIMIZATION_LEVEL)
+print_config("GPL :" ENABLE_GPL)
+print_config("Best configuration :" ENABLE_BEST)
+print_config("Optimization level :" OPTIMIZATION_LEVEL)
message("")
-print_config("Assertions :" ENABLE_ASSERTIONS)
-print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS)
-print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
+print_config("Assertions :" ENABLE_ASSERTIONS)
+print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS)
+print_config("Debug context mem mgr :" ENABLE_DEBUG_CONTEXT_MM)
message("")
-print_config("Dumping :" ENABLE_DUMPING)
-print_config("Muzzle :" ENABLE_MUZZLE)
-print_config("Proofs :" ENABLE_PROOFS)
-print_config("Replay :" ENABLE_REPLAY)
-print_config("Statistics :" ENABLE_STATISTICS)
-print_config("Tracing :" ENABLE_TRACING)
+print_config("Dumping :" ENABLE_DUMPING)
+print_config("Muzzle :" ENABLE_MUZZLE)
+print_config("Proofs :" ENABLE_PROOFS)
+print_config("Statistics :" ENABLE_STATISTICS)
+print_config("Tracing :" ENABLE_TRACING)
message("")
-print_config("Asan :" ENABLE_ASAN)
-print_config("Coverage (gcov) :" ENABLE_COVERAGE)
-print_config("Profiling (gprof) :" ENABLE_PROFILING)
-print_config("Unit tests :" ENABLE_UNIT_TESTING)
-print_config("Valgrind :" ENABLE_VALGRIND)
+print_config("ASan :" ENABLE_ASAN)
+print_config("UBSan :" ENABLE_UBSAN)
+print_config("TSan :" ENABLE_TSAN)
+print_config("Coverage (gcov) :" ENABLE_COVERAGE)
+print_config("Profiling (gprof) :" ENABLE_PROFILING)
+print_config("Unit tests :" ENABLE_UNIT_TESTING)
+print_config("Valgrind :" ENABLE_VALGRIND)
message("")
-print_config("Shared libs :" ENABLE_SHARED)
-print_config("Java bindings :" BUILD_BINDINGS_JAVA)
-print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
+print_config("Shared libs :" ENABLE_SHARED)
+print_config("Static binary :" ENABLE_STATIC_BINARY)
+print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
+print_config("Java bindings :" BUILD_BINDINGS_JAVA)
+print_config("Python2 :" USE_PYTHON2)
message("")
-print_config("Portfolio :" ENABLE_PORTFOLIO)
+print_config("ABC :" USE_ABC)
+print_config("CaDiCaL :" USE_CADICAL)
+print_config("CryptoMiniSat :" USE_CRYPTOMINISAT)
+print_config("drat2er :" USE_DRAT2ER)
+print_config("GLPK :" USE_GLPK)
+print_config("Kissat :" USE_KISSAT)
+print_config("LFSC :" USE_LFSC)
+print_config("LibPoly :" USE_POLY)
message("")
-print_config("ABC :" USE_ABC)
-print_config("CaDiCaL :" USE_CADICAL)
-print_config("CryptoMiniSat :" USE_CRYPTOMINISAT)
-print_config("GLPK :" USE_GLPK)
-print_config("LFSC :" USE_LFSC)
+print_config("BUILD_LIB_ONLY :" BUILD_LIB_ONLY)
if(CVC4_USE_CLN_IMP)
- message("MP library : cln")
+ message("MP library : cln")
else()
- message("MP library : gmp")
+ message("MP library : gmp")
endif()
-print_config("Readline :" ${USE_READLINE})
-print_config("SymFPU :" ${USE_SYMFPU})
+print_config("Editline :" ${USE_EDITLINE})
+print_config("SymFPU :" ${USE_SYMFPU})
message("")
if(ABC_DIR)
- message("ABC dir : ${ABC_DIR}")
+ message("ABC dir : ${ABC_DIR}")
endif()
if(ANTLR_DIR)
- message("ANTLR dir : ${ANTLR_DIR}")
+ message("ANTLR dir : ${ANTLR_DIR}")
endif()
if(CADICAL_DIR)
- message("CADICAL dir : ${CADICAL_DIR}")
+ message("CADICAL dir : ${CADICAL_DIR}")
endif()
if(CRYPTOMINISAT_DIR)
- message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}")
+ message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}")
+endif()
+if(DRAT2ER_DIR)
+ message("DRAT2ER dir : ${DRAT2ER_DIR}")
endif()
if(GLPK_DIR)
- message("GLPK dir : ${GLPK_DIR}")
+ message("GLPK dir : ${GLPK_DIR}")
endif()
if(GMP_DIR)
- message("GMP dir : ${GMP_DIR}")
+ message("GMP dir : ${GMP_DIR}")
+endif()
+if(KISSAT_DIR)
+ message("KISSAT dir : ${KISSAT_DIR}")
endif()
if(LFSC_DIR)
- message("LFSC dir : ${LFSC_DIR}")
+ message("LFSC dir : ${LFSC_DIR}")
+endif()
+if(POLY_DIR)
+ message("LibPoly dir : ${POLY_DIR}")
endif()
if(SYMFPU_DIR)
- message("SYMFPU dir : ${SYMFPU_DIR}")
+ message("SYMFPU dir : ${SYMFPU_DIR}")
endif()
message("")
-message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}")
-message("CXXFLAGS : ${CMAKE_CXX_FLAGS}")
-message("CFLAGS : ${CMAKE_C_FLAGS}")
-#message("LIBS : ${LIBS}")
-#message("LDFLAGS : ${LDFLAGS}")
-#message("")
-#message("libcvc4 version : ${{CVC4_LIBRARY_VERSION}")
-#message("libcvc4parser version : ${CVC4_PARSER_LIBRARY_VERSION}")
-#message("libcvc4compat version : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}")
-#message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}")
-#message("")
-message("Install prefix : ${CMAKE_INSTALL_PREFIX}")
+message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}")
+message("CXXFLAGS : ${CMAKE_CXX_FLAGS}")
+message("CFLAGS : ${CMAKE_C_FLAGS}")
+message("Linker flags : ${CMAKE_EXE_LINKER_FLAGS}")
+message("")
+message("Install prefix : ${CMAKE_INSTALL_PREFIX}")
message("")
if(GPL_LIBS)
message(
- "CVC4 license : GPLv3 (due to optional libraries; see below)"
+ "CVC4 license : ${Yellow}GPLv3 (due to optional libraries; see below)${ResetColor}"
"\n"
"\n"
"Please note that CVC4 will be built against the following GPLed libraries:"
"\n"
"If you prefer to license CVC4 under those terms, please configure CVC4 to"
"\n"
- "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
+ "disable all optional GPLed library dependencies (-DENABLE_BSD_ONLY=ON)."
)
else()
message(
- "CVC4 license : modified BSD"
+ "CVC4 license : modified BSD"
"\n"
"\n"
"Note that this configuration is NOT built against any GPL'ed libraries, so"
)
endif()
+if("${CMAKE_GENERATOR}" STREQUAL "Ninja")
+ set(BUILD_COMMAND_NAME "ninja")
+else()
+ set(BUILD_COMMAND_NAME "make")
+endif()
+
message("")
-message("Now just type make, followed by make check or make install.")
+message("Now just type '${BUILD_COMMAND_NAME}', "
+ "followed by '${BUILD_COMMAND_NAME} check' "
+ "or '${BUILD_COMMAND_NAME} install'.")
message("")
projects / cvc5.git / blobdiff