set(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
set(CMAKE_C_STANDARD 99)
set(CMAKE_CXX_STANDARD 11)
+set(CMAKE_CXX_EXTENSIONS OFF)
# Generate compile_commands.json, which can be used for various code completion
# plugins.
set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+#-----------------------------------------------------------------------------#
+# Policies
+
+# Required for FindGLPK since it sets CMAKE_REQUIRED_LIBRARIES
+if(POLICY CMP0075)
+ cmake_policy(SET CMP0075 NEW)
+endif()
+
+#-----------------------------------------------------------------------------#
+# Tell CMake where to find our dependencies
+
+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(LFSC_DIR)
+ list(APPEND CMAKE_PREFIX_PATH "${LFSC_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)
+
+#-----------------------------------------------------------------------------#
+
# 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
#
# 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")
+set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${LIBRARY_INSTALL_DIR}")
#-----------------------------------------------------------------------------#
# >> 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 "Suppress 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
# >> 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_GLPK "Use GLPK simplex solver")
+cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
+cvc4_option(USE_READLINE "Use readline 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_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)")
+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
# 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")
+# Supported SWIG language bindings
+option(BUILD_SWIG_BINDINGS_JAVA "Build Java bindings with SWIG")
+option(BUILD_SWIG_BINDINGS_PYTHON "Build Python bindings with SWIG")
+
+# Supprted language bindings based on new C++ API
+option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ")
#-----------------------------------------------------------------------------#
# Internal cmake variables
# to cmake standards (first letter uppercase).
set(BUILD_TYPES Production Debug Testing Competition)
-if(ENABLE_ASAN)
+if(ENABLE_ASAN OR ENABLE_UBSAN OR ENABLE_TSAN)
set(CMAKE_BUILD_TYPE Debug)
endif()
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(...)))
#
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
find_package(PythonInterp REQUIRED)
endif()
-set(GMP_HOME ${GMP_DIR})
find_package(GMP REQUIRED)
if(ENABLE_ASAN)
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_check_c_cxx_flag("-ggdb3")
endif()
-if(ENABLE_MUZZLE)
- add_definitions(-DCVC4_MUZZLE)
+if(ENABLE_COMP_INC_TRACK)
+ add_definitions(-DCVC4_SMTCOMP_APPLICATION_TRACK)
endif()
-# This check needs to come before the USE_CLN check.
-if(ENABLE_PORTFOLIO)
- find_package(Boost 1.50.0 REQUIRED COMPONENTS thread)
- if (ENABLE_DUMPING)
- message(FATAL_ERROR "Dumping not supported with a portfolio build.")
- endif()
- # Disable CLN for portfolio builds since it is not thread safe (uses an
- # unlocked hash table internally).
- if(USE_CLN)
- message(WARNING "Disabling CLN support since portfolio is enabled.")
- set(USE_CLN OFF)
- endif()
- 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_MUZZLE)
+ add_definitions(-DCVC4_MUZZLE)
endif()
-# This has to be processed after ENABLE_PORTFOLIO (disables dumping support).
if(ENABLE_DUMPING)
add_definitions(-DCVC4_DUMPING)
endif()
add_definitions(-DCVC4_PROOF)
endif()
-if(ENABLE_REPLAY)
- add_definitions(-DCVC4_REPLAY)
-endif()
-
if(ENABLE_TRACING)
add_definitions(-DCVC4_TRACING)
endif()
endif()
if(USE_ABC)
- set(ABC_HOME "${ABC_DIR}")
find_package(ABC REQUIRED)
add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS})
endif()
if(USE_CADICAL)
- set(CaDiCaL_HOME ${CADICAL_DIR})
find_package(CaDiCaL REQUIRED)
add_definitions(-DCVC4_USE_CADICAL)
endif()
if(THREADS_HAVE_PTHREAD_ARG)
add_c_cxx_flag(-pthread)
endif()
- set(CryptoMiniSat_HOME ${CRYPTOMINISAT_DIR})
find_package(CryptoMiniSat REQUIRED)
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)
add_definitions(-DCVC4_USE_GLPK)
endif()
if(USE_LFSC)
set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
- set(LFSC_HOME ${LFSC_DIR})
find_package(LFSC REQUIRED)
add_definitions(-DCVC4_USE_LFSC)
endif()
endif()
if(USE_SYMFPU)
- set(SymFPU_HOME ${SYMFPU_DIR})
find_package(SymFPU REQUIRED)
add_definitions(-DCVC4_USE_SYMFPU)
set(CVC4_USE_SYMFPU 1)
endif()
add_subdirectory(doc)
-add_subdirectory(examples EXCLUDE_FROM_ALL) # excluded from all target
add_subdirectory(src)
add_subdirectory(test)
-if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
+if(BUILD_SWIG_BINDINGS_JAVA OR BUILD_SWIG_BINDINGS_PYTHON)
add_subdirectory(src/bindings)
endif()
+if(BUILD_BINDINGS_PYTHON)
+ add_subdirectory(src/api/python)
+endif()
+
+#-----------------------------------------------------------------------------#
+# Package configuration
+#
+# Export CVC4 targets to support find_package(CVC4) in other cmake projects.
+
+include(CMakePackageConfigHelpers)
+
+install(EXPORT cvc4-targets
+ FILE CVC4Targets.cmake
+ NAMESPACE CVC4::
+ DESTINATION ${LIBRARY_INSTALL_DIR}/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
+)
+
+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 ${LIBRARY_INSTALL_DIR}/cmake/CVC4
+)
+
+
#-----------------------------------------------------------------------------#
# Print build configuration
message("CVC4 ${CVC4_RELEASE_STRING}")
message("")
-message("Build profile : ${CVC4_BUILD_PROFILE_STRING}")
-message("")
-print_config("GPL :" ENABLE_GPL)
-print_config("Best configuration :" ENABLE_BEST)
-print_config("Optimized :" ENABLE_OPTIMIZED)
-print_config("Optimization level :" OPTIMIZATION_LEVEL)
+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("Assertions :" ENABLE_ASSERTIONS)
-print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS)
-print_config("Debug context mem mgr:" ENABLE_DEBUG_CONTEXT_MM)
+print_config("GPL :" ENABLE_GPL)
+print_config("Best configuration :" ENABLE_BEST)
+print_config("Optimization level :" OPTIMIZATION_LEVEL)
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("Assertions :" ENABLE_ASSERTIONS)
+print_config("Debug symbols :" ENABLE_DEBUG_SYMBOLS)
+print_config("Debug context mem mgr :" ENABLE_DEBUG_CONTEXT_MM)
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("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("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)
+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("Portfolio :" ENABLE_PORTFOLIO)
+print_config("Shared libs :" ENABLE_SHARED)
+print_config("Static binary :" ENABLE_STATIC_BINARY)
+print_config("Java SWIG bindings :" BUILD_SWIG_BINDINGS_JAVA)
+print_config("Python SWIG bindings :" BUILD_SWIG_BINDINGS_PYTHON)
+print_config("Python bindings :" BUILD_BINDINGS_PYTHON)
+print_config("Python2 :" USE_PYTHON2)
+print_config("Python3 :" USE_PYTHON3)
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)
+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(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("Readline :" ${USE_READLINE})
+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}")
+ 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(LFSC_DIR)
- message("LFSC dir : ${LFSC_DIR}")
+ message("LFSC dir : ${LFSC_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("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("Install prefix : ${CMAKE_INSTALL_PREFIX}")
message("")
if(GPL_LIBS)
message(
- "CVC4 license : GPLv3 (due to optional libraries; see below)"
+ "CVC4 license : GPLv3 (due to optional libraries; see below)"
"\n"
"\n"
"Please note that CVC4 will be built against the following GPLed libraries:"
)
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"