9 files changed, 267 insertions, 102 deletions
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 <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
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 $<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})