-cmake_minimum_required(VERSION 3.4)
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+## Mathias Preiner, Aina Niemetz, Gereon Kremer
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2021 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)
+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.
set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
set(CMAKE_C_STANDARD 99)
-set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_STANDARD 17)
set(CMAKE_CXX_EXTENSIONS OFF)
+set(CMAKE_CXX_STANDARD_REQUIRED ON)
+set(CMAKE_CXX_VISIBILITY_PRESET hidden)
+set(CMAKE_VISIBILITY_INLINES_HIDDEN 1)
# Generate compile_commands.json, which can be used for various code completion
# plugins.
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()
# By default the contrib/get-* scripts install dependencies to deps/install.
list(APPEND CMAKE_PREFIX_PATH "${PROJECT_SOURCE_DIR}/deps/install")
#-----------------------------------------------------------------------------#
-set(INCLUDE_INSTALL_DIR include)
-set(LIBRARY_INSTALL_DIR lib)
-set(RUNTIME_INSTALL_DIR bin)
-
-#-----------------------------------------------------------------------------#
-
include(Helpers)
#-----------------------------------------------------------------------------#
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(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_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 "Prefer using Python 2 (for Python bindings)")
-option(USE_PYTHON3 "Prefer using Python 3 (for Python bindings)")
+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
# check the intalled system version. If the user provides a directory we
# immediately fail if the dependency was not found at the specified location.
set(ABC_DIR "" CACHE STRING "Set ABC install directory")
-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")
# Prepend binaries with prefix on make install
set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install")
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
add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
add_check_c_cxx_flag("-Wall")
+add_check_c_cxx_flag("-Wno-unused-private-field")
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")
endif()
#-----------------------------------------------------------------------------#
-# Set options for best configuration
-
-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_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()
message(WARNING "Disabling static binary since shared build is enabled.")
endif()
+ # Set visibility to default if unit tests are enabled
+ if(ENABLE_UNIT_TESTING)
+ set(CMAKE_CXX_VISIBILITY_PRESET default)
+ set(CMAKE_VISIBILITY_INLINES_HIDDEN 0)
+ endif()
+
# 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
#
# More information on RPATH in CMake:
# https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
- set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${LIBRARY_INSTALL_DIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
+ set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib")
else()
- set(CMAKE_FIND_LIBRARY_SUFFIXES .a ${CMAKE_FIND_LIBRARY_SUFFIXES})
+ # 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)
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()
#-----------------------------------------------------------------------------#
# 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(USE_PYTHON2)
find_package(PythonInterp 2.7 REQUIRED)
-elseif(USE_PYTHON3)
- find_package(PythonInterp 3 REQUIRED)
else()
- find_package(PythonInterp REQUIRED)
+ find_package(PythonInterp 3 REQUIRED)
endif()
-find_package(GMP REQUIRED)
+find_package(GMP 6.2 REQUIRED)
if(ENABLE_ASAN)
# -fsanitize=address requires CMAKE_REQUIRED_FLAGS to be explicitely set,
add_check_c_cxx_flag("-pg")
endif()
-if(ENABLE_PROOFS)
- set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --enable-proof)
- add_definitions(-DCVC4_PROOF)
-endif()
-
if(ENABLE_TRACING)
add_definitions(-DCVC4_TRACING)
endif()
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")
find_package(GLPK REQUIRED)
add_definitions(-DCVC4_USE_KISSAT)
endif()
-if(USE_LFSC)
- set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
- find_package(LFSC REQUIRED)
- add_definitions(-DCVC4_USE_LFSC)
-endif()
-
if(USE_POLY)
find_package(Poly REQUIRED)
add_definitions(-DCVC4_USE_POLY)
set(CVC4_GPL_DEPS 1)
endif()
+#-----------------------------------------------------------------------------#
+# Provide targets to inspect iwyu suggestions
+
+include(IWYU)
+
#-----------------------------------------------------------------------------#
# Generate CVC4's cvc4autoconfig.h header
include(ConfigureCVC4)
+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)
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)
- message(FATAL_ERROR
- "Java bindings for the new API are not implemented yet.")
+ add_subdirectory(src/api/java)
+ message(WARNING "Java API is currently under development.")
endif()
#-----------------------------------------------------------------------------#
# 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
+# (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)
install(EXPORT cvc4-targets
FILE CVC4Targets.cmake
NAMESPACE CVC4::
- DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/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 ${LIBRARY_INSTALL_DIR}/cmake/CVC4
- PATH_VARS LIBRARY_INSTALL_DIR
+ INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4
+ PATH_VARS CMAKE_INSTALL_LIBDIR
)
write_basic_package_version_file(
install(FILES
${CMAKE_BINARY_DIR}/cmake/CVC4Config.cmake
${CMAKE_BINARY_DIR}/CVC4ConfigVersion.cmake
- DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4
+ DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/CVC4
)
#-----------------------------------------------------------------------------#
# Print build configuration
+# Set colors.
+if(NOT WIN32)
+ string(ASCII 27 Esc)
+ set(Green "${Esc}[32m")
+ set(Blue "${Esc}[1;34m")
+ set(ResetColor "${Esc}[m")
+endif()
+
# Convert build type to lower case.
string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING)
get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS)
string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
-message("CVC4 ${CVC4_RELEASE_STRING}")
+message("")
+print_info("CVC4 ${CVC4_RELEASE_STRING}")
message("")
if(ENABLE_COMP_INC_TRACK)
- message("Build profile : ${CVC4_BUILD_PROFILE_STRING} (incremental)")
+ print_config("Build profile " "${CVC4_BUILD_PROFILE_STRING} (incremental)")
else()
- message("Build profile : ${CVC4_BUILD_PROFILE_STRING}")
+ print_config("Build profile " "${CVC4_BUILD_PROFILE_STRING}")
endif()
message("")
-print_config("GPL :" ENABLE_GPL)
-print_config("Best configuration :" ENABLE_BEST)
-print_config("Optimization level :" OPTIMIZATION_LEVEL)
+print_config("GPL " ${ENABLE_GPL})
+print_config("Best configuration " ${ENABLE_BEST})
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("Statistics :" ENABLE_STATISTICS)
-print_config("Tracing :" ENABLE_TRACING)
+print_config("Dumping " ${ENABLE_DUMPING})
+print_config("Muzzle " ${ENABLE_MUZZLE})
+print_config("Statistics " ${ENABLE_STATISTICS})
+print_config("Tracing " ${ENABLE_TRACING})
message("")
-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)
+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("Static binary :" ENABLE_STATIC_BINARY)
-print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
-print_config("Java bindings :" BUILD_BINDINGS_JAVA)
-print_config("Python2 :" USE_PYTHON2)
-print_config("Python3 :" USE_PYTHON3)
+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("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)
+print_config("ABC " ${USE_ABC})
+print_config("CaDiCaL " ${USE_CADICAL})
+print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT})
+print_config("GLPK " ${USE_GLPK})
+print_config("Kissat " ${USE_KISSAT})
+print_config("LibPoly " ${USE_POLY})
+message("")
+print_config("Build libcvc4 only " ${BUILD_LIB_ONLY})
if(CVC4_USE_CLN_IMP)
- message("MP library : cln")
+ print_config("MP library " "cln")
else()
- message("MP library : gmp")
+ print_config("MP library " "gmp")
endif()
-print_config("Editline :" ${USE_EDITLINE})
-print_config("SymFPU :" ${USE_SYMFPU})
+print_config("Editline " ${USE_EDITLINE})
+print_config("SymFPU " ${USE_SYMFPU})
message("")
if(ABC_DIR)
- message("ABC dir : ${ABC_DIR}")
-endif()
-if(ANTLR_DIR)
- message("ANTLR dir : ${ANTLR_DIR}")
-endif()
-if(CADICAL_DIR)
- message("CADICAL dir : ${CADICAL_DIR}")
-endif()
-if(CRYPTOMINISAT_DIR)
- message("CRYPTOMINISAT dir : ${CRYPTOMINISAT_DIR}")
-endif()
-if(DRAT2ER_DIR)
- message("DRAT2ER dir : ${DRAT2ER_DIR}")
+ print_config("ABC dir " ${ABC_DIR})
endif()
if(GLPK_DIR)
- message("GLPK dir : ${GLPK_DIR}")
-endif()
-if(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}")
-endif()
-if(POLY_DIR)
- message("LibPoly dir : ${POLY_DIR}")
-endif()
-if(SYMFPU_DIR)
- message("SYMFPU dir : ${SYMFPU_DIR}")
+ print_config("GLPK dir " ${GLPK_DIR})
endif()
message("")
-message("CPPLAGS (-D...) : ${CVC4_DEFINITIONS}")
-message("CXXFLAGS : ${CMAKE_CXX_FLAGS}")
-message("CFLAGS : ${CMAKE_C_FLAGS}")
-message("Linker flags : ${CMAKE_EXE_LINKER_FLAGS}")
+print_config("CPPLAGS (-D...)" "${CVC4_DEFINITIONS}")
+print_config("CXXFLAGS " "${CMAKE_CXX_FLAGS}")
+print_config("CFLAGS " "${CMAKE_C_FLAGS}")
+print_config("Linker flags " "${CMAKE_EXE_LINKER_FLAGS}")
message("")
-message("Install prefix : ${CMAKE_INSTALL_PREFIX}")
+print_config("Install prefix " "${CMAKE_INSTALL_PREFIX}")
message("")
if(GPL_LIBS)
message(
- "CVC4 license : GPLv3 (due to optional libraries; see below)"
+ "${Blue}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:"
)
else()
message(
- "CVC4 license : modified BSD"
+ "${Blue}CVC4 license:${ResetColor} modified BSD"
"\n"
"\n"
"Note that this configuration is NOT built against any GPL'ed libraries, so"
projects / cvc5.git / blobdiff