From 39ea1d8a1497a83d1efc649bd10da82916e5db5f Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 31 Mar 2021 22:00:54 +0200 Subject: [PATCH] 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. --- .github/workflows/ci.yml | 2 - cmake/FindCaDiCaL.cmake | 86 +++++++++++++++-- cmake/FindCryptoMiniSat.cmake | 92 +++++++++++++++++-- cmake/FindKissat.cmake | 67 ++++++++++++-- .../CryptoMiniSat-patch-ba6f76e3.patch | 41 +++++++++ contrib/get-cadical | 21 ----- contrib/get-cryptominisat | 27 ------ contrib/get-kissat | 24 ----- src/CMakeLists.txt | 9 +- 9 files changed, 267 insertions(+), 102 deletions(-) create mode 100644 cmake/deps-utils/CryptoMiniSat-patch-ba6f76e3.patch delete mode 100755 contrib/get-cadical delete mode 100755 contrib/get-cryptominisat delete mode 100755 contrib/get-kissat diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5ebdc30b8..21d8784ae 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -119,8 +119,6 @@ jobs: if: steps.restore-deps.outputs.cache-hit != 'true' run: | ./contrib/get-poly - ./contrib/get-cadical - ./contrib/get-cryptominisat ./contrib/get-lfsc-checker - name: List dependencies 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 /build + # avoid configure script, prepare the makefile manually + COMMAND + sed -e "s,@CXX@,${CMAKE_CXX_COMPILER}," -e "s,@CXXFLAGS@,${CXXFLAGS}," -e + "s,@MAKEFLAGS@,," /makefile.in > /build/makefile + # use $(MAKE) instead of "make" to allow for parallel builds + BUILD_COMMAND $(MAKE) -C /build libcadical.a + INSTALL_COMMAND ${CMAKE_COMMAND} -E copy /build/libcadical.a + /lib/libcadical.a + COMMAND ${CMAKE_COMMAND} -E copy /src/cadical.hpp + /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 /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= + -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 /lib/libcryptominisat5.a + ) + # remove unused stuff to keep folder small + ExternalProject_Add_Step( + CryptoMiniSat-EP cleanup + DEPENDEES install + COMMAND ${CMAKE_COMMAND} -E remove /cryptominisat5_simple + COMMAND ${CMAKE_COMMAND} -E remove /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 /configure -fPIC --quiet + CC=${CMAKE_C_COMPILER} + INSTALL_COMMAND ${CMAKE_COMMAND} -E copy /build/libkissat.a + /lib/libkissat.a + COMMAND ${CMAKE_COMMAND} -E copy /src/kissat.h + /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 +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 diff --git a/contrib/get-cadical b/contrib/get-cadical deleted file mode 100755 index bb3fab2fa..000000000 --- a/contrib/get-cadical +++ /dev/null @@ -1,21 +0,0 @@ -#!/usr/bin/env bash -# -source "$(dirname "$0")/get-script-header.sh" - -CADICAL_DIR="$DEPS_DIR/cadical" -version="rel-1.2.1" - -setup_dep \ - "https://github.com/arminbiere/cadical/archive/$version.tar.gz" "$CADICAL_DIR" -cd "$CADICAL_DIR" - -CXXFLAGS="-fPIC" ./configure && make -j$(nproc) - -install_lib build/libcadical.a -install_includes src/cadical.hpp - -echo -echo "Using CaDiCaL version $version" -echo -echo ===================== Now configure CVC4 with ===================== -echo ./configure.sh --cadical diff --git a/contrib/get-cryptominisat b/contrib/get-cryptominisat deleted file mode 100755 index 655a76eae..000000000 --- a/contrib/get-cryptominisat +++ /dev/null @@ -1,27 +0,0 @@ -#!/usr/bin/env bash -# -source "$(dirname "$0")/get-script-header.sh" - -CMS_DIR="$DEPS_DIR/cryptominisat5" -version="5.8.0" - -setup_dep \ - "https://github.com/msoos/cryptominisat/archive/$version.tar.gz" \ - "$CMS_DIR" -cd "$CMS_DIR" - -mkdir build -cd build -cmake -DENABLE_PYTHON_INTERFACE=OFF \ - -DSTATICCOMPILE=ON \ - -DNOM4RI=ON \ - -DNOSQLITE=ON \ - -DONLY_SIMPLE=ON \ - -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR" \ - .. - -make install -j$(nproc) - -echo -echo ===================== Now configure CVC4 with ===================== -echo ./configure.sh --cryptominisat diff --git a/contrib/get-kissat b/contrib/get-kissat deleted file mode 100755 index 2e21bb69b..000000000 --- a/contrib/get-kissat +++ /dev/null @@ -1,24 +0,0 @@ -#!/usr/bin/env bash - -set -e -o pipefail - -source "$(dirname "$0")/get-script-header.sh" - -KISSAT_DIR="${DEPS_DIR}/kissat" -version="sc2020-039805f2" - -# Download and build Kissat -setup_dep \ - "http://fmv.jku.at/kissat/kissat-$version.tar.xz" "$KISSAT_DIR" -cd "${KISSAT_DIR}" - -./configure -fPIC --quiet -make -j${NPROC} -install_lib build/libkissat.a -install_includes src/kissat.h kissat - -echo -echo "Using Kissat version $version" -echo -echo ===================== Now configure CVC4 with ===================== -echo ./configure.sh --kissat diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1a8c1964d..78236f989 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1131,20 +1131,17 @@ if(USE_ABC) target_include_directories(cvc4 PRIVATE ${ABC_INCLUDE_DIR}) endif() if(USE_CADICAL) - target_link_libraries(cvc4 PRIVATE ${CaDiCaL_LIBRARIES}) - target_include_directories(cvc4 PRIVATE ${CaDiCaL_INCLUDE_DIR}) + target_link_libraries(cvc4 PRIVATE CaDiCaL) endif() if(USE_CLN) target_link_libraries(cvc4 PRIVATE ${CLN_LIBRARIES}) target_include_directories(cvc4 PRIVATE $) endif() if(USE_CRYPTOMINISAT) - target_link_libraries(cvc4 PRIVATE ${CryptoMiniSat_LIBRARIES}) - target_include_directories(cvc4 PRIVATE ${CryptoMiniSat_INCLUDE_DIR}) + target_link_libraries(cvc4 PRIVATE CryptoMiniSat) endif() if(USE_KISSAT) - target_link_libraries(cvc4 PRIVATE ${Kissat_LIBRARIES}) - target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR}) + target_link_libraries(cvc4 PRIVATE Kissat) endif() if(USE_GLPK) target_link_libraries(cvc4 PRIVATE ${GLPK_LIBRARIES}) -- 2.30.2