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)
# 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)
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")
# > 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)")
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")
# 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
set(ENABLE_UNIT_TESTING OFF)
endif()
-# Never build unit tests as static binaries, otherwise we'll end up with
-# ~300MB per unit test.
-if(ENABLE_UNIT_TESTING)
- if(NOT ENABLE_SHARED)
- message(WARNING "Disabling static build since unit testing is enabled.")
- endif()
- set(ENABLE_SHARED ON)
-endif()
-
#-----------------------------------------------------------------------------#
# Shared/static libraries
#
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(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()
#-----------------------------------------------------------------------------#
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})
# 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("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()
projects / cvc5.git / blobdiff