include(CheckIPOSupported)
include(GNUInstallDirs)
+set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
-set(CVC5_MAJOR 1) # Major component of the version of cvc5.
-set(CVC5_MINOR 0) # Minor component of the version of cvc5.
-set(CVC5_RELEASE 0) # Release component of the version of cvc5.
-
-# Extraversion component of the version of cvc5.
-set(CVC5_EXTRAVERSION "-prerelease")
-
-# Shared library versioning. Increment SOVERSION for every new cvc5 release.
-set(CVC5_SOVERSION 1)
+include(version)
-# Full release string for cvc5.
-if(CVC5_RELEASE)
- set(CVC5_RELEASE_STRING
- "${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}${CVC5_EXTRAVERSION}")
-else()
- set(CVC5_RELEASE_STRING "${CVC5_MAJOR}.${CVC5_MINOR}${CVC5_EXTRAVERSION}")
-endif()
-
-set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
set(CMAKE_C_STANDARD 99)
set(CMAKE_CXX_STANDARD 17)
set(CMAKE_CXX_EXTENSIONS OFF)
#-----------------------------------------------------------------------------#
# Tell CMake where to find our dependencies
-if(ABC_DIR)
- list(APPEND CMAKE_PREFIX_PATH "${ABC_DIR}")
-endif()
if(GLPK_DIR)
list(APPEND CMAKE_PREFIX_PATH "${GLPK_DIR}")
endif()
# >> 3-valued: IGNORE ON OFF
# > allows to detect if set by user (default: IGNORE)
# > only necessary for options set for build types
+option(BUILD_SHARED_LIBS "Build shared libraries and binary")
cvc5_option(ENABLE_ASAN "Enable ASAN build")
cvc5_option(ENABLE_UBSAN "Enable UBSan build")
cvc5_option(ENABLE_TSAN "Enable TSan build")
cvc5_option(ENABLE_COMP_INC_TRACK
"Enable optimizations for incremental SMT-COMP tracks")
cvc5_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
-cvc5_option(ENABLE_DUMPING "Enable dumping")
cvc5_option(ENABLE_MUZZLE "Suppress ALL non-result output")
cvc5_option(ENABLE_STATISTICS "Enable statistics")
cvc5_option(ENABLE_TRACING "Enable tracing")
cvc5_option(ENABLE_UNIT_TESTING "Enable unit testing")
cvc5_option(ENABLE_VALGRIND "Enable valgrind instrumentation")
-cvc5_option(ENABLE_STATIC_LIBRARY "Enable building static library")
-cvc5_option(ENABLE_STATIC_BINARY
- "Build static binaries with statically linked system libraries")
cvc5_option(ENABLE_AUTO_DOWNLOAD "Enable automatic download of dependencies")
cvc5_option(ENABLE_IPO "Enable interprocedural optimization")
# >> 2-valued: ON OFF
# >> 3-valued: IGNORE ON OFF
# > allows to detect if set by user (default: IGNORE)
# > only necessary for options set for ENABLE_BEST
-cvc5_option(USE_ABC "Use ABC for AIG bit-blasting")
cvc5_option(USE_CLN "Use CLN instead of GMP")
cvc5_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
cvc5_option(USE_GLPK "Use GLPK simplex solver")
# installed via the corresponding contrib/get-* script and if not found, we
# 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(GLPK_DIR "" CACHE STRING "Set GLPK install directory")
# Prepend binaries with prefix on make install
option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ")
# Api documentation
-cvc5_option(BUILD_DOCS "Build Api documentation")
+option(BUILD_DOCS "Build Api documentation")
+
+# Link against static system libraries
+cvc5_option(STATIC_BINARY "Link against static system libraries \
+(enabled by default for static builds)")
#-----------------------------------------------------------------------------#
# 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_cxx_supression_flag("-Wno-unused-private-field")
add_check_c_flag("-fexceptions")
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")
+add_check_cxx_supression_flag("-Wno-class-memaccess")
if (WIN32)
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000")
set(CMAKE_INTERPROCEDURAL_OPTIMIZATION TRUE)
endif()
-
-#-----------------------------------------------------------------------------#
-# Option defaults (three-valued options (cvc5_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.
-
-if(ENABLE_STATIC_BINARY)
- message(STATUS "Enable static library for static binary build.")
- cvc5_set_option(ENABLE_STATIC_LIBRARY ON)
-endif()
-
#-----------------------------------------------------------------------------#
# Only enable unit testing if assertions are enabled. Otherwise, unit tests
#-----------------------------------------------------------------------------#
# Shared/static libraries
+
+# Embed the installation prefix as an RPATH in the executable such that the
+# linker can find our libraries (such as libcvc5parser) when executing the
+# cvc5 binary. This is for example useful when installing cvc5 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 cvc5.
+#
+# 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.
#
-# This needs to be set before any find_package(...) command since we want to
-# search for static libraries with suffix .a.
-
-if(NOT ENABLE_STATIC_BINARY)
- # Embed the installation prefix as an RPATH in the executable such that the
- # linker can find our libraries (such as libcvc5parser) when executing the
- # cvc5 binary. This is for example useful when installing cvc5 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 cvc5.
- #
- # 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")
-endif()
-
-# Set visibility to default if unit tests are enabled
+# 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")
+
+# Set visibility to default if unit tests are enabled. If unit tests are
+# enabled, we also check if we can execute white box unit tests (some versions
+# of Clang have issues with the required flag).
+set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
if(ENABLE_UNIT_TESTING)
set(CMAKE_CXX_VISIBILITY_PRESET default)
set(CMAKE_VISIBILITY_INLINES_HIDDEN 0)
+
+ # Check if Clang version has the bug that was fixed in
+ # https://reviews.llvm.org/D93104
+ set(ENABLE_WHITEBOX_UNIT_TESTING ON)
+ check_cxx_compiler_flag("-faccess-control" HAVE_CXX_FLAGfaccess_control)
+ if(NOT HAVE_CXX_FLAGfaccess_control)
+ set(ENABLE_WHITEBOX_UNIT_TESTING OFF)
+ message(STATUS "Disabling white box unit tests")
+ endif()
endif()
#-----------------------------------------------------------------------------#
#-----------------------------------------------------------------------------#
# Check options, find packages and configure build.
+if(BUILD_SHARED_LIBS)
+ if (WIN32)
+ set(CMAKE_FIND_LIBRARY_SUFFIXES .dll .lib .a)
+ else()
+ set(CMAKE_FIND_LIBRARY_SUFFIXES .so .dylib .a)
+ endif()
+else()
+ if (WIN32)
+ set(CMAKE_FIND_LIBRARY_SUFFIXES .lib .a .dll)
+ else()
+ set(CMAKE_FIND_LIBRARY_SUFFIXES .a .so .dylib)
+ endif()
+endif()
+
if(USE_PYTHON2)
find_package(PythonInterp 2.7 REQUIRED)
else()
if(ENABLE_COVERAGE)
include(CodeCoverage)
- APPEND_COVERAGE_COMPILER_FLAGS()
+ append_coverage_compiler_flags()
add_definitions(-DCVC5_COVERAGE)
- # 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-test
- EXECUTABLE
- ctest -j${CTEST_NTHREADS} -LE "example"
- --output-on-failure $$ARGS || exit 0
- DEPENDS
- build-tests)
-
- # Adds targets `coverage` and `coverage-reset` for manually generating
- # coverage reports for specific executions.
- #
- # Target coverage-reset resets all the coverage counters to zero, while
- # target coverage will generate a coverage report for all executions since
- # the last coverage-reset.
- setup_target_for_coverage_lcov_no_executable(
+ setup_code_coverage_fastcov(
NAME coverage
- DEPENDENCIES cvc5-bin)
+ PATH "${PROJECT_SOURCE_DIR}"
+ EXCLUDE "${CMAKE_BINARY_DIR}/deps/*"
+ DEPENDENCIES cvc5-bin
+ )
endif()
if(ENABLE_DEBUG_CONTEXT_MM)
add_definitions(-DCVC5_MUZZLE)
endif()
-if(ENABLE_DUMPING)
- add_definitions(-DCVC5_DUMPING)
-endif()
-
if(ENABLE_PROFILING)
add_definitions(-DCVC5_PROFILING)
add_check_c_cxx_flag("-pg")
add_definitions(-DCVC5_VALGRIND)
endif()
-if(USE_ABC)
- find_package(ABC REQUIRED)
- add_definitions(-DCVC5_USE_ABC ${ABC_ARCH_FLAGS})
-endif()
-
find_package(CaDiCaL REQUIRED)
if(USE_CLN)
# Provide targets to inspect iwyu suggestions
include(IWYU)
+include(fuzzing-murxla)
#-----------------------------------------------------------------------------#
include(ConfigureCvc5)
-if(ENABLE_STATIC_BINARY)
+if(BUILD_SHARED_LIBS)
+ set(CVC5_STATIC_BUILD OFF)
+else()
set(CVC5_STATIC_BUILD ON)
+ if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+ cvc5_set_option(STATIC_BINARY ON)
+ endif()
endif()
#-----------------------------------------------------------------------------#
add_subdirectory(src)
+if(BUILD_BINDINGS_PYTHON AND NOT BUILD_SHARED_LIBS)
+ message(STATUS "Python bindings can only be built in a shared build.")
+ set(BUILD_BINDINGS_PYTHON OFF)
+endif()
if(BUILD_BINDINGS_PYTHON)
set(BUILD_BINDINGS_PYTHON_VERSION ${PYTHON_VERSION_MAJOR})
add_subdirectory(src/api/python)
if(BUILD_BINDINGS_JAVA)
add_subdirectory(src/api/java)
- message(WARNING "Java API is currently under development.")
endif()
if(BUILD_DOCS)
add_subdirectory(test)
+include(target-graphs)
+
#-----------------------------------------------------------------------------#
# Package configuration
#
# (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)
+if(BUILD_SHARED_LIBS)
# Get the libraries that cvc5 links against
- get_target_property(libs cvc5-shared INTERFACE_LINK_LIBRARIES)
+ get_target_property(libs cvc5 INTERFACE_LINK_LIBRARIES)
set(LIBS_SHARED_FROM_DEPS "")
foreach(lib ${libs})
# Filter out those that are linked dynamically and come from deps/install
write_basic_package_version_file(
${CMAKE_CURRENT_BINARY_DIR}/cvc5ConfigVersion.cmake
- VERSION ${CVC5_RELEASE_STRING}
+ VERSION ${CVC5_VERSION}
COMPATIBILITY ExactVersion
)
string(REPLACE ";" " " CVC5_DEFINITIONS "${CVC5_DEFINITIONS}")
message("")
-print_info("cvc5 ${CVC5_RELEASE_STRING}")
+print_info("cvc5 ${CVC5_VERSION}")
message("")
if(ENABLE_COMP_INC_TRACK)
print_config("Build profile " "${CVC5_BUILD_PROFILE_STRING} (incremental)")
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("Statistics " ${ENABLE_STATISTICS})
print_config("Tracing " ${ENABLE_TRACING})
print_config("Unit tests " ${ENABLE_UNIT_TESTING})
print_config("Valgrind " ${ENABLE_VALGRIND})
message("")
-print_config("Static library " ${ENABLE_STATIC_LIBRARY})
-print_config("Static binary " ${ENABLE_STATIC_BINARY})
+print_config("Shared build " ${BUILD_SHARED_LIBS})
print_config("Python bindings " ${BUILD_BINDINGS_PYTHON})
print_config("Java bindings " ${BUILD_BINDINGS_JAVA})
print_config("Python2 " ${USE_PYTHON2})
print_config("Interprocedural opt. " ${ENABLE_IPO})
message("")
-print_config("ABC " ${USE_ABC})
print_config("CryptoMiniSat " ${USE_CRYPTOMINISAT} FOUND_SYSTEM ${CryptoMiniSat_FOUND_SYSTEM})
print_config("GLPK " ${USE_GLPK})
print_config("Kissat " ${USE_KISSAT} FOUND_SYSTEM ${Kissat_FOUND_SYSTEM})
message("")
print_config("Api docs " ${BUILD_DOCS})
message("")
-if(ABC_DIR)
- print_config("ABC dir " ${ABC_DIR})
-endif()
if(GLPK_DIR)
print_config("GLPK dir " ${GLPK_DIR})
endif()
"\n"
"Note that this configuration is NOT built against any GPL'ed libraries, so"
"\n"
- "it is covered by the (modified) BSD license. This is, however, not the best"
+ "it is covered by the (modified) BSD license. To build against GPL'ed"
"\n"
- "performing configuration of cvc5. To build against GPL'ed libraries which"
+ "libraries which can improve cvc5's performance on arithmetic and bitvector"
"\n"
- "improve cvc5's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
+ "logics, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
)
endif()
projects / cvc5.git / blobdiff