diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-31 22:00:54 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 20:00:54 +0000 |
commit | 39ea1d8a1497a83d1efc649bd10da82916e5db5f (patch) | |
tree | 3fb701819277f3683f0baf40147a5eb94789009d /cmake | |
parent | b7210ed60d517aebb25c23a2f407ee59562587dd (diff) |
Refactor dependencies for external SAT solvers (#6215)
This PR refactors how we obtain, build and use the external SAT solvers used by CVC4: CaDiCaL, CryptoMiniSat and Kissat.
All three contrib scripts are removed and instead an external project is integrated into the cmake find scripts.
Diffstat (limited to 'cmake')
-rw-r--r-- | cmake/FindCaDiCaL.cmake | 86 | ||||
-rw-r--r-- | cmake/FindCryptoMiniSat.cmake | 92 | ||||
-rw-r--r-- | cmake/FindKissat.cmake | 67 | ||||
-rw-r--r-- | cmake/deps-utils/CryptoMiniSat-patch-ba6f76e3.patch | 41 |
4 files changed, 264 insertions, 22 deletions
diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index cb6768fa3..b9894a16d 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -13,15 +13,87 @@ # CaDiCaL_INCLUDE_DIR - the CaDiCaL include directory # CaDiCaL_LIBRARIES - Libraries needed to use CaDiCaL +include(deps-helper) + find_path(CaDiCaL_INCLUDE_DIR NAMES cadical.hpp) find_library(CaDiCaL_LIBRARIES NAMES cadical) -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(CaDiCaL - DEFAULT_MSG - CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES) +set(CaDiCaL_FOUND_SYSTEM FALSE) +if(CaDiCaL_INCLUDE_DIR AND CaDiCaL_LIBRARIES) + set(CaDiCaL_FOUND_SYSTEM TRUE) + + # Unfortunately it is not part of the headers + find_library(CaDiCaL_BINARY NAMES cadical) + if(CaDiCaL_BINARY) + execute_process( + COMMAND ${CaDiCaL_BINARY} --version OUTPUT_VARIALE CaDiCaL_VERSION + ) + else() + set(CaDiCaL_VERSION "") + endif() + + check_system_version("CaDiCaL") +endif() + +if(NOT CaDiCaL_FOUND_SYSTEM) + include(CheckSymbolExists) + include(ExternalProject) + + fail_if_include_missing("sys/resource.h" "CaDiCaL") + + set(CaDiCaL_VERSION "1.2.1") + + # avoid configure script and instantiate the makefile manually the configure + # scripts unnecessarily fails for cross compilation thus we do the bare + # minimum from the configure script here + set(CXXFLAGS "-fPIC -O3 -DNDEBUG -DQUIET -std=c++11") + # check for getc_unlocked + check_symbol_exists("getc_unlocked" "cstdio" HAVE_UNLOCKED_IO) + if(NOT HAVE_UNLOCKED_IO) + set(CXXFLAGS "${CXXFLAGS} -DNUNLOCKED") + endif() + + ExternalProject_Add( + CaDiCaL-EP + PREFIX ${DEPS_PREFIX} + BUILD_IN_SOURCE ON + URL https://github.com/arminbiere/cadical/archive/refs/tags/rel-${CaDiCaL_VERSION}.tar.gz + URL_HASH SHA1=9de1176737b74440921ba86395fe5edbb3b131eb + CONFIGURE_COMMAND mkdir -p <SOURCE_DIR>/build + # avoid configure script, prepare the makefile manually + COMMAND + sed -e "s,@CXX@,${CMAKE_CXX_COMPILER}," -e "s,@CXXFLAGS@,${CXXFLAGS}," -e + "s,@MAKEFLAGS@,," <SOURCE_DIR>/makefile.in > <SOURCE_DIR>/build/makefile + # use $(MAKE) instead of "make" to allow for parallel builds + BUILD_COMMAND $(MAKE) -C <SOURCE_DIR>/build libcadical.a + INSTALL_COMMAND ${CMAKE_COMMAND} -E copy <SOURCE_DIR>/build/libcadical.a + <INSTALL_DIR>/lib/libcadical.a + COMMAND ${CMAKE_COMMAND} -E copy <SOURCE_DIR>/src/cadical.hpp + <INSTALL_DIR>/include/cadical.hpp + ) + + set(CaDiCaL_INCLUDE_DIR "${DEPS_BASE}/include/") + set(CaDiCaL_LIBRARIES "${DEPS_BASE}/lib/libcadical.a") +endif() + +set(CaDiCaL_FOUND TRUE) + +add_library(CaDiCaL STATIC IMPORTED GLOBAL) +set_target_properties( + CaDiCaL PROPERTIES IMPORTED_LOCATION "${CaDiCaL_LIBRARIES}" +) +set_target_properties( + CaDiCaL PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${CaDiCaL_INCLUDE_DIR}" +) + +mark_as_advanced(CaDiCaL_FOUND) +mark_as_advanced(CaDiCaL_FOUND_SYSTEM) +mark_as_advanced(CaDiCaL_INCLUDE_DIR) +mark_as_advanced(CaDiCaL_LIBRARIES) -mark_as_advanced(CaDiCaL_INCLUDE_DIR CaDiCaL_LIBRARIES) -if(CaDiCaL_LIBRARIES) - message(STATUS "Found CaDiCaL libs: ${CaDiCaL_LIBRARIES}") +if(CaDiCaL_FOUND_SYSTEM) + message(STATUS "Found CaDiCaL ${CaDiCaL_VERSION}: ${CaDiCaL_LIBRARIES}") +else() + message(STATUS "Building CaDiCaL ${CaDiCaL_VERSION}: ${CaDiCaL_LIBRARIES}") + add_dependencies(CaDiCaL CaDiCaL-EP) endif() diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake index 821511fdd..318907797 100644 --- a/cmake/FindCryptoMiniSat.cmake +++ b/cmake/FindCryptoMiniSat.cmake @@ -13,16 +13,90 @@ # CryptoMiniSat_INCLUDE_DIR - the CryptoMiniSat include directory # CryptoMiniSat_LIBRARIES - Libraries needed to use CryptoMiniSat +include(deps-helper) -find_path(CryptoMiniSat_INCLUDE_DIR NAMES cryptominisat5/cryptominisat.h) -find_library(CryptoMiniSat_LIBRARIES NAMES cryptominisat5) +find_package(cryptominisat5 ${CryptoMiniSat_FIND_VERSION} QUIET) -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(CryptoMiniSat - DEFAULT_MSG - CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES) +set(CryptoMiniSat_FOUND_SYSTEM FALSE) +if(cryptominisat5_FOUND) + set(CryptoMiniSat_FOUND_SYSTEM TRUE) + add_library(CryptoMiniSat INTERFACE IMPORTED GLOBAL) + target_link_libraries(CryptoMiniSat INTERFACE cryptominisat5) + # TODO(gereon): remove this when + # https://github.com/msoos/cryptominisat/pull/645 is merged + set_target_properties( + CryptoMiniSat PROPERTIES INTERFACE_INCLUDE_DIRECTORIES + "${CRYPTOMINISAT5_INCLUDE_DIRS}" + ) -mark_as_advanced(CryptoMiniSat_INCLUDE_DIR CryptoMiniSat_LIBRARIES) -if(CryptoMiniSat_LIBRARIES) - message(STATUS "Found CryptoMiniSat libs: ${CryptoMiniSat_LIBRARIES}") +endif() + +if(NOT CryptoMiniSat_FOUND_SYSTEM) + include(ExternalProject) + + set(CryptoMiniSat_VERSION "5.8.0") + + ExternalProject_Add( + CryptoMiniSat-EP + PREFIX ${DEPS_PREFIX} + URL https://github.com/msoos/cryptominisat/archive/refs/tags/${CryptoMiniSat_VERSION}.tar.gz + URL_HASH SHA1=f79dfa1ffc6c9c75b3a33f76d3a89a3df2b3f4c2 + PATCH_COMMAND + patch <SOURCE_DIR>/src/packedmatrix.h + ${CMAKE_CURRENT_LIST_DIR}/deps-utils/CryptoMiniSat-patch-ba6f76e3.patch + CMAKE_ARGS -DCMAKE_BUILD_TYPE=Release + # make sure not to register with cmake + -DCMAKE_EXPORT_NO_PACKAGE_REGISTRY=ON + -DCMAKE_INSTALL_PREFIX=<INSTALL_DIR> + -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE} + -DENABLE_ASSERTIONS=OFF + -DENABLE_PYTHON_INTERFACE=OFF + # disable what is not needed + -DNOBREAKID=ON + -DNOM4RI=ON + -DNOSQLITE=ON + -DNOZLIB=ON + -DONLY_SIMPLE=ON + -DSTATICCOMPILE=ON + BUILD_BYPRODUCTS <INSTALL_DIR>/lib/libcryptominisat5.a + ) + # remove unused stuff to keep folder small + ExternalProject_Add_Step( + CryptoMiniSat-EP cleanup + DEPENDEES install + COMMAND ${CMAKE_COMMAND} -E remove <BINARY_DIR>/cryptominisat5_simple + COMMAND ${CMAKE_COMMAND} -E remove <INSTALL_DIR>/bin/cryptominisat5_simple + ) + + set(CryptoMiniSat_INCLUDE_DIR "${DEPS_BASE}/include/") + set(CryptoMiniSat_LIBRARIES "${DEPS_BASE}/lib/libcryptominisat5.a") + + add_library(CryptoMiniSat STATIC IMPORTED GLOBAL) + set_target_properties( + CryptoMiniSat PROPERTIES IMPORTED_LOCATION "${CryptoMiniSat_LIBRARIES}" + ) + set_target_properties( + CryptoMiniSat PROPERTIES INTERFACE_INCLUDE_DIRECTORIES + "${CryptoMiniSat_INCLUDE_DIR}" + ) +endif() + +set(CryptoMiniSat_FOUND TRUE) + +mark_as_advanced(CryptoMiniSat_FOUND) +mark_as_advanced(CryptoMiniSat_FOUND_SYSTEM) +mark_as_advanced(CryptoMiniSat_INCLUDE_DIR) +mark_as_advanced(CryptoMiniSat_LIBRARIES) + +if(CryptoMiniSat_FOUND_SYSTEM) + message( + STATUS + "Found CryptoMiniSat ${CryptoMiniSat_VERSION}: ${CryptoMiniSat_LIBRARIES}" + ) +else() + message( + STATUS + "Building CryptoMiniSat ${CryptoMiniSat_VERSION}: ${CryptoMiniSat_LIBRARIES}" + ) + add_dependencies(CryptoMiniSat CryptoMiniSat-EP) endif() diff --git a/cmake/FindKissat.cmake b/cmake/FindKissat.cmake index 66cd983f5..e71a64eea 100644 --- a/cmake/FindKissat.cmake +++ b/cmake/FindKissat.cmake @@ -13,15 +13,70 @@ # Kissat_INCLUDE_DIR - the Kissat include directory # Kissat_LIBRARIES - Libraries needed to use Kissat +include(deps-helper) + find_path(Kissat_INCLUDE_DIR NAMES kissat/kissat.h) find_library(Kissat_LIBRARIES NAMES kissat) -include(FindPackageHandleStandardArgs) -find_package_handle_standard_args(Kissat - DEFAULT_MSG Kissat_INCLUDE_DIR Kissat_LIBRARIES) +set(Kissat_FOUND_SYSTEM FALSE) +if(Kissat_INCLUDE_DIR AND Kissat_LIBRARIES) + set(Kissat_FOUND_SYSTEM TRUE) + + # Unfortunately it is not part of the headers + find_library(Kissat_BINARY NAMES kissat) + if(Kissat_BINARY) + execute_process( + COMMAND ${Kissat_BINARY} --version OUTPUT_VARIALE Kissat_VERSION + ) + else() + set(Kissat_VERSION "") + endif() + + check_system_version("Kissat") +endif() + +if(NOT Kissat_FOUND_SYSTEM) + include(ExternalProject) + + fail_if_include_missing("sys/resource.h" "Kissat") -mark_as_advanced(Kissat_INCLUDE_DIR Kissat_LIBRARIES) -if(Kissat_LIBRARIES) - message(STATUS "Found Kissat library: ${Kissat_LIBRARIES}") + # TODO(mpreiner): use the version from github? + set(Kissat_VERSION "sc2020-039805f2") + + ExternalProject_Add( + Kissat-EP + PREFIX ${DEPS_PREFIX} + BUILD_IN_SOURCE ON + URL http://fmv.jku.at/kissat/kissat-${Kissat_VERSION}.tar.xz + URL_HASH SHA1=5125efa17d383c7e7c1e6d803e3422b17cebcedb + CONFIGURE_COMMAND <SOURCE_DIR>/configure -fPIC --quiet + CC=${CMAKE_C_COMPILER} + INSTALL_COMMAND ${CMAKE_COMMAND} -E copy <SOURCE_DIR>/build/libkissat.a + <INSTALL_DIR>/lib/libkissat.a + COMMAND ${CMAKE_COMMAND} -E copy <SOURCE_DIR>/src/kissat.h + <INSTALL_DIR>/include/kissat/kissat.h + ) + + set(Kissat_INCLUDE_DIR "${DEPS_BASE}/include/") + set(Kissat_LIBRARIES "${DEPS_BASE}/lib/libkissat.a") endif() +set(Kissat_FOUND TRUE) + +add_library(Kissat STATIC IMPORTED GLOBAL) +set_target_properties(Kissat PROPERTIES IMPORTED_LOCATION "${Kissat_LIBRARIES}") +set_target_properties( + Kissat PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${Kissat_INCLUDE_DIR}" +) + +mark_as_advanced(Kissat_FOUND) +mark_as_advanced(Kissat_FOUND_SYSTEM) +mark_as_advanced(Kissat_INCLUDE_DIR) +mark_as_advanced(Kissat_LIBRARIES) + +if(Kissat_FOUND_SYSTEM) + message(STATUS "Found Kissat ${Kissat_VERSION}: ${Kissat_LIBRARIES}") +else() + message(STATUS "Building Kissat ${Kissat_VERSION}: ${Kissat_LIBRARIES}") + add_dependencies(Kissat Kissat-EP) +endif() diff --git a/cmake/deps-utils/CryptoMiniSat-patch-ba6f76e3.patch b/cmake/deps-utils/CryptoMiniSat-patch-ba6f76e3.patch new file mode 100644 index 000000000..da41dc122 --- /dev/null +++ b/cmake/deps-utils/CryptoMiniSat-patch-ba6f76e3.patch @@ -0,0 +1,41 @@ +https://github.com/msoos/cryptominisat/commit/ba6f76e353c2b235131f0357eeea057b597c9d08 +From ba6f76e353c2b235131f0357eeea057b597c9d08 Mon Sep 17 00:00:00 2001 +From: Yevgeny Kazakov <yevgeny.kazakov@uni-ulm.de> +Date: Sat, 1 Aug 2020 17:53:39 +0200 +Subject: [PATCH] Fix compilation under mingw32; address #625 + +--- + src/packedmatrix.h | 6 +++--- + 1 file changed, 3 insertions(+), 3 deletions(-) + +diff --git a/src/packedmatrix.h b/src/packedmatrix.h +index 486dda706..221dd9d5a 100644 +--- a/src/packedmatrix.h ++++ b/src/packedmatrix.h +@@ -50,7 +50,7 @@ class PackedMatrix + + ~PackedMatrix() + { +- #ifdef _MSC_VER ++ #ifdef _WIN32 + _aligned_free((void*)mp); + #else + free(mp); +@@ -62,7 +62,7 @@ class PackedMatrix + num_cols = num_cols / 64 + (bool)(num_cols % 64); + if (numRows*(numCols+1) < (int)num_rows*((int)num_cols+1)) { + size_t size = sizeof(int64_t) * num_rows*(num_cols+1); +- #ifdef _MSC_VER ++ #ifdef _WIN32 + _aligned_free((void*)mp); + mp = (int64_t*)_aligned_malloc(size, 16); + #else +@@ -85,7 +85,7 @@ class PackedMatrix + { + if (numRows*(numCols+1) < b.numRows*(b.numCols+1)) { + size_t size = sizeof(int64_t) * b.numRows*(b.numCols+1); +- #ifdef _MSC_VER ++ #ifdef _WIN32 + _aligned_free((void*)mp); + mp = (int64_t*)_aligned_malloc(size, 16); + #else |