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.

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