cmake_minimum_required(VERSION 3.1)
-if(POLICY CMP0075)
- cmake_policy(SET CMP0075 NEW)
-endif()
-
#-----------------------------------------------------------------------------#
# Project configuration
project(cvc4)
set(CVC4_MAJOR 1) # Major component of the version of CVC4.
-set(CVC4_MINOR 7) # Minor component of the version of CVC4.
+set(CVC4_MINOR 8) # 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 5)
+set(CVC4_SOVERSION 6)
# Full release string for CVC4.
if(CVC4_RELEASE)
set(CMAKE_C_STANDARD 99)
set(CMAKE_CXX_STANDARD 11)
+# Generate compile_commands.json, which can be used for various code completion
+# plugins.
+set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+
+# 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.
+#
+# More information on RPATH in CMake:
+# https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling
+set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib")
+
#-----------------------------------------------------------------------------#
include(Helpers)
# 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_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")
# > 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_DRAT2ER "Include drat2er for making eager BV proofs")
option(USE_LFSC "Use LFSC proof checker")
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)")
# 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(LFSC_DIR "" CACHE STRING "Set LFSC 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")
+
# Supported language bindings
option(BUILD_BINDINGS_JAVA "Build Java bindings")
option(BUILD_BINDINGS_PYTHON "Build Python bindings")
set(OPTIMIZATION_LEVEL 3)
set(GPL_LIBS "")
+#-----------------------------------------------------------------------------#
+# Determine number of threads available, used to configure (default) parallel
+# execution of custom test targets (can be overriden with ARGS=-jN).
+
+include(ProcessorCount)
+ProcessorCount(CTEST_NTHREADS)
+if(CTEST_NTHREADS EQUAL 0)
+ set(CTEST_NTHREADS 1)
+endif()
+
#-----------------------------------------------------------------------------#
# Build types
# 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")
+# Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment'
+# cdlist.h warnings. Remove when fixed.
+add_check_cxx_flag("-Wno-class-memaccess")
+
#-----------------------------------------------------------------------------#
# 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_SHARED ON)
+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)
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)
endif()
-#-----------------------------------------------------------------------------#
-# Static libraries
+# Only enable unit testing if assertions are enabled. Otherwise, unit tests
+# that expect AssertionException to be thrown will fail.
+if(NOT ENABLE_ASSERTIONS)
+ 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")
+
+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()
+else()
+ set(CMAKE_FIND_LIBRARY_SUFFIXES .a ${CMAKE_FIND_LIBRARY_SUFFIXES})
set(BUILD_SHARED_LIBS OFF)
+ # This is required to force find_package(Boost) to use static libraries.
+ set(Boost_USE_STATIC_LIBS ON)
+ cvc4_set_option(ENABLE_STATIC_BINARY ON)
+
+ # 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()
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 3)
find_package(PythonInterp REQUIRED)
endif()
set(GMP_HOME ${GMP_DIR})
find_package(GMP REQUIRED)
-libcvc4_link_libraries(${GMP_LIBRARIES})
-libcvc4_include_directories(${GMP_INCLUDE_DIR})
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()
add_definitions(-DCVC4_ASSERTIONS)
else()
add_definitions(-DNDEBUG)
- # Only enable unit testing if assertions are enabled. Otherwise, unit tests
- # that expect AssertionException to be thrown will fail.
- set(ENABLE_UNIT_TESTING OFF)
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_TRACING)
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)
add_definitions(-DCVC4_STATISTICS_ON)
endif()
if(ENABLE_VALGRIND)
find_package(Valgrind REQUIRED)
- libcvc4_include_directories(${Valgrind_INCLUDE_DIR})
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()
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)
+ set(Drat2Er_HOME ${DRAT2ER_DIR})
+ 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()
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)
endif()
if(USE_READLINE)
+ set(GPL_LIBS "${GPL_LIBS} readline")
find_package(Readline REQUIRED)
set(HAVE_LIBREADLINE 1)
if(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR)
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()
# Generate CVC4's cvc4autoconfig.h header
include(ConfigureCVC4)
-configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h)
+configure_file(cvc4autoconfig.h.in cvc4autoconfig.h)
include_directories(${CMAKE_CURRENT_BINARY_DIR})
#-----------------------------------------------------------------------------#
print_config("Valgrind :" ENABLE_VALGRIND)
message("")
print_config("Shared libs :" ENABLE_SHARED)
+print_config("Static binary :" ENABLE_STATIC_BINARY)
print_config("Java bindings :" BUILD_BINDINGS_JAVA)
print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
print_config("Python2 :" USE_PYTHON2)
+print_config("Python3 :" USE_PYTHON3)
message("")
print_config("Portfolio :" ENABLE_PORTFOLIO)
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("LFSC :" USE_LFSC)
if(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}")
endif()
"\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(
projects / cvc5.git / blobdiff