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.
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
# 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()
# 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()
# 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()
--- /dev/null
+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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
+++ /dev/null
-#!/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
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 $<BUILD_INTERFACE:${CLN_INCLUDE_DIR}>)
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})
projects / cvc5.git / commitdiff