From a0dcede017fa326e1dcf4b58bd7d4f9c5e5b9b0e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 12 Sep 2023 10:07:46 +0000 Subject: [PATCH] Update CaDiCaL from 1.5.3 to 1.7.2 Update to the latest release. The only remaining local patch is to add a file suffix to CaDiCaL's VERSION file. --- scripts/cadical-1.5.3-patch | 45 ------------------------------------- scripts/cadical-1.7.2-patch | 22 ++++++++++++++++++ src/Makefile | 4 ++-- src/solvers/CMakeLists.txt | 12 +++++----- 4 files changed, 30 insertions(+), 53 deletions(-) delete mode 100644 scripts/cadical-1.5.3-patch create mode 100644 scripts/cadical-1.7.2-patch diff --git a/scripts/cadical-1.5.3-patch b/scripts/cadical-1.5.3-patch deleted file mode 100644 index 85adca52f56..00000000000 --- a/scripts/cadical-1.5.3-patch +++ /dev/null @@ -1,45 +0,0 @@ -diff --git a/scripts/make-build-header.sh b/scripts/make-build-header.sh -index e8f6746..1290024 100755 ---- a/scripts/make-build-header.sh -+++ b/scripts/make-build-header.sh -@@ -20,7 +20,7 @@ warning () { - - #--------------------------------------------------------------------------# - --[ ! -f VERSION -a ! -f ../VERSION ] && \ -+[ ! -f VERSION.txt -a ! -f ../VERSION.txt ] && \ - die "needs to be called from build sub-directory" - - [ -f makefile ] || \ -@@ -29,7 +29,7 @@ warning "could not find 'makefile'" - #--------------------------------------------------------------------------# - # The version. - # --VERSION="`cat ../VERSION`" -+VERSION="`cat ../VERSION.txt`" - if [ x"$VERSION" = x ] - then - warning "could not determine 'VERSION'" -diff --git a/src/lookahead.cpp b/src/lookahead.cpp -index 9e8a16b..3d5721a 100644 ---- a/src/lookahead.cpp -+++ b/src/lookahead.cpp -@@ -390,6 +390,7 @@ int Internal::lookahead_probing() { - CubesWithStatus Internal::generate_cubes(int depth, int min_depth) { - if (!active() || depth == 0) { - CubesWithStatus cubes; -+ cubes.status = 0; - cubes.cubes.push_back(std::vector()); - return cubes; - } -diff -urN cadical-rel-1.5.3/src/solver.cpp cadical-rel-1.5.3.patched/src/solver.cpp ---- cadical-rel-1.5.3/src/solver.cpp 2023-02-13 09:11:26.000000000 +0000 -+++ cadical-rel-1.5.3.patched/src/solver.cpp 2023-05-29 09:42:55.871965742 +0000 -@@ -258,7 +258,6 @@ - - #define TRACE(...) \ - do { \ -- if ((this == 0)) break; \ - if ((internal == 0)) break; \ - LOG_API_CALL_BEGIN (__VA_ARGS__); \ - if (!trace_api_file) break; \ diff --git a/scripts/cadical-1.7.2-patch b/scripts/cadical-1.7.2-patch new file mode 100644 index 00000000000..f77e7a9d16b --- /dev/null +++ b/scripts/cadical-1.7.2-patch @@ -0,0 +1,22 @@ +diff --git a/scripts/make-build-header.sh b/scripts/make-build-header.sh +index e8f6746..1290024 100755 +--- a/scripts/make-build-header.sh ++++ b/scripts/make-build-header.sh +@@ -20,7 +20,7 @@ warning () { + + #--------------------------------------------------------------------------# + +-[ ! -f VERSION -a ! -f ../VERSION ] && \ ++[ ! -f VERSION.txt -a ! -f ../VERSION.txt ] && \ + die "needs to be called from build sub-directory" + + [ -f makefile ] || \ +@@ -29,7 +29,7 @@ warning "could not find 'makefile'" + #--------------------------------------------------------------------------# + # The version. + # +-VERSION="`cat ../VERSION`" ++VERSION="`cat ../VERSION.txt`" + if [ x"$VERSION" = x ] + then + warning "could not determine 'VERSION'" diff --git a/src/Makefile b/src/Makefile index dae2d361cf2..33895f29688 100644 --- a/src/Makefile +++ b/src/Makefile @@ -181,14 +181,14 @@ glucose-download: @(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch) @$(RM) $(glucose_rev).tar.gz -cadical_release = rel-1.5.3 +cadical_release = rel-1.7.2 cadical-download: @echo "Downloading CaDiCaL $(cadical_release)" @$(DOWNLOADER) https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz @$(TAR) xfz $(cadical_release).tar.gz @rm -Rf ../cadical @mv cadical-$(cadical_release) ../cadical - @(cd ../cadical; patch -p1 < ../scripts/cadical-1.5.3-patch) + @(cd ../cadical; patch -p1 < ../scripts/cadical-1.7.2-patch) @(cd ../cadical && ./configure) # Need to rename VERSION so that it isn't picked up by `#include` on # macOS which is case insensitive diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 8bfcf4d13c2..daa0853a573 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -124,11 +124,11 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building solvers with cadical") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.5.3.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.5.3-patch + URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt COMMAND ./configure - URL_MD5 265b1a715000ed3c5b6de36ddd1278a0 + URL_MD5 be646831a017f81b300664e58deba1b5 ) add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR}) @@ -147,10 +147,10 @@ foreach(SOLVER ${sat_impl}) message(STATUS "Building with IPASIR solver linking against: CaDiCaL") download_project(PROJ cadical - URL https://github.com/arminbiere/cadical/archive/rel-1.5.3.tar.gz - PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.5.3-patch + URL https://github.com/arminbiere/cadical/archive/rel-1.7.2.tar.gz + PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-1.7.2-patch COMMAND ./configure - URL_MD5 265b1a715000ed3c5b6de36ddd1278a0 + URL_MD5 be646831a017f81b300664e58deba1b5 ) message(STATUS "Building CaDiCaL")