From 151c8fe3f4a87c2ea84dc86ce6cb4b6d114aed39 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Dec 2021 10:24:54 +0000 Subject: [PATCH] Switch Glucose download source to GitHub www.labri.fr appears to be (temporarily?) offline, which already happened several weeks ago, when it was offline for about one day. To avoid spurious CI failures, switch to a GitHub source that hosts to Glucose source. The use of Bruno Dutertre's fork also reduces the number of patches that need to be applied, mostly leaving just Windows-specific bits to be patched. --- scripts/glucose-syrup-patch | 143 +----------------------------------- src/Makefile | 9 ++- src/solvers/CMakeLists.txt | 4 +- 3 files changed, 11 insertions(+), 145 deletions(-) diff --git a/scripts/glucose-syrup-patch b/scripts/glucose-syrup-patch index e8c24c54b0b..4d5960193ed 100644 --- a/scripts/glucose-syrup-patch +++ b/scripts/glucose-syrup-patch @@ -1,24 +1,3 @@ -diff -rupNw glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc ---- glucose-syrup/core/Solver.cc 2014-10-03 11:10:21.000000000 +0200 -+++ glucose-syrup-patched/core/Solver.cc 2018-04-21 16:58:22.950005391 +0200 -@@ -931,7 +931,6 @@ void Solver::uncheckedEnqueue(Lit p, CRe - CRef Solver::propagate() { - CRef confl = CRef_Undef; - int num_props = 0; -- int previousqhead = qhead; - watches.cleanAll(); - watchesBin.cleanAll(); - unaryWatches.cleanAll(); -@@ -1405,7 +1404,9 @@ lbool Solver::search(int nof_conflicts) - decisions++; - next = pickBranchLit(); - if (next == lit_Undef) { -+#if 0 - printf("c last restart ## conflicts : %d %d \n", conflictC, decisionLevel()); -+#endif - // Model found: - return l_True; - } diff -rupNw glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTypes.h --- glucose-syrup/core/SolverTypes.h 2014-10-03 11:10:22.000000000 +0200 +++ glucose-syrup-patched/core/SolverTypes.h 2018-04-21 16:58:22.950005391 +0200 @@ -32,47 +11,6 @@ diff -rupNw glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTy #include "mtl/IntTypes.h" #include "mtl/Alg.h" -@@ -170,7 +172,10 @@ class Clause { - unsigned lbd : BITS_LBD; - } header; - -+#include -+#include - union { Lit lit; float act; uint32_t abs; CRef rel; } data[0]; -+#include - - friend class ClauseAllocator; - -diff -rupNw glucose-syrup/mtl/Clone.h glucose-syrup-patched/mtl/Clone.h ---- glucose-syrup/mtl/Clone.h 2014-10-03 11:10:22.000000000 +0200 -+++ glucose-syrup-patched/mtl/Clone.h 2018-05-10 12:35:25.150491249 +0200 -@@ -8,6 +8,6 @@ namespace Glucose { - public: - virtual Clone* clone() const = 0; - }; --}; -+} - - #endif -\ No newline at end of file -diff -rupNw glucose-syrup/mtl/Clone.h~ glucose-syrup-patched/mtl/Clone.h~ ---- glucose-syrup/mtl/Clone.h~ 1970-01-01 01:00:00.000000000 +0100 -+++ glucose-syrup-patched/mtl/Clone.h~ 2018-04-21 16:58:22.950005391 +0200 -@@ -0,0 +1,13 @@ -+#ifndef Glucose_Clone_h -+#define Glucose_Clone_h -+ -+ -+namespace Glucose { -+ -+ class Clone { -+ public: -+ virtual Clone* clone() const = 0; -+ }; -+}; -+ -+#endif -\ No newline at end of file diff -rupNw glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h --- glucose-syrup/mtl/IntTypes.h 2014-10-03 11:10:22.000000000 +0200 +++ glucose-syrup-patched/mtl/IntTypes.h 2018-04-21 16:58:22.950005391 +0200 @@ -86,22 +24,10 @@ diff -rupNw glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h #endif -diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h ---- glucose-syrup/mtl/Vec.h 2014-10-03 11:10:22.000000000 +0200 -+++ glucose-syrup-patched/mtl/Vec.h 2018-04-21 16:58:22.950005391 +0200 -@@ -103,7 +103,7 @@ template - void vec::capacity(int min_cap) { - if (cap >= min_cap) return; - int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 -- if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM) -+ if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)) - throw OutOfMemoryException(); - } - diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h --- glucose-syrup/mtl/Vec.h +++ glucose-syrup-patched/mtl/Vec.h -@@ -103,8 +103,10 @@ +@@ -118,8 +118,10 @@ void vec::capacity(int min_cap) { if (cap >= min_cap) return; int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 @@ -115,36 +41,9 @@ diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h diff -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc ---- glucose-syrup/simp/SimpSolver.cc 2014-10-03 11:10:22.000000000 +0200 -+++ glucose-syrup-patched/simp/SimpSolver.cc 2018-04-21 16:58:22.950005391 +0200 -@@ -319,10 +319,13 @@ bool SimpSolver::merge(const Clause& _ps - if (var(qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) -+ { - if (ps[j] == ~qs[i]) -+ - return false; - else - goto next; -+ } - out_clause.push(qs[i]); - } - next:; -@@ -353,10 +356,12 @@ bool SimpSolver::merge(const Clause& _ps - if (var(__qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(__ps[j]) == var(__qs[i])) -+ { - if (__ps[j] == ~__qs[i]) - return false; - else - goto next; -+ } - size++; - } - next:; -@@ -687,11 +692,11 @@ bool SimpSolver::eliminate(bool turn_off +--- glucose-syrup/simp/SimpSolver.cc 2014-10-03 11:10:22.000000000 +0200 ++++ glucose-syrup-patched/simp/SimpSolver.cc 2018-04-21 16:58:22.950005391 +0200 +@@ -713,11 +713,11 @@ bool SimpSolver::eliminate(bool turn_off // int toPerform = clauses.size()<=4800000; @@ -158,31 +57,6 @@ diff -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolv while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){ gatherTouchedClauses(); -@@ -760,10 +765,11 @@ bool SimpSolver::eliminate(bool turn_off - checkGarbage(); - } - -+#if 0 - if (verbosity >= 0 && elimclauses.size() > 0) - printf("c | Eliminated clauses: %10.2f Mb |\n", - double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); -- -+#endif - - return ok; - -diff -rupNw glucose-syrup/utils/Options.h glucose-syrup-patched/utils/Options.h ---- glucose-syrup/utils/Options.h 2014-10-03 11:10:22.000000000 +0200 -+++ glucose-syrup-patched/utils/Options.h 2018-04-21 16:58:22.950005391 +0200 -@@ -60,7 +60,7 @@ class Option - struct OptionLt { - bool operator()(const Option* x, const Option* y) { - int test1 = strcmp(x->category, y->category); -- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; -+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0); - } - }; - diff -rupNw glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUtils.h --- glucose-syrup/utils/ParseUtils.h 2014-10-03 11:10:22.000000000 +0200 +++ glucose-syrup-patched/utils/ParseUtils.h 2018-04-21 16:58:22.950005391 +0200 @@ -217,15 +91,6 @@ diff -rupNw glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUt int operator * () const { return (pos >= size) ? EOF : buf[pos]; } void operator ++ () { pos++; assureLookahead(); } -@@ -96,7 +96,7 @@ - if (*in != '.') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3); - ++in; // skip dot - currentExponent = 0.1; -- while (*in >= '0' && *in <= '9') -+ while (*in >= '0' && *in <= '9') - accu = accu + currentExponent * ((double)(*in - '0')), - currentExponent /= 10, - ++in; diff -rupNw glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h --- glucose-syrup/utils/System.h 2014-10-03 11:10:22.000000000 +0200 +++ glucose-syrup-patched/utils/System.h 2018-04-21 16:58:22.950005391 +0200 diff --git a/src/Makefile b/src/Makefile index 10ce7f184a9..92afa0ba26b 100644 --- a/src/Makefile +++ b/src/Makefile @@ -149,14 +149,15 @@ cudd-download: @echo "Compiling Cudd 3.0.0" @(cd ../cudd-3.0.0; ./configure; $(MAKE)) +glucose_rev = 0bb2afd3b9baace6981cbb8b4a1c7683c44968b7 glucose-download: @echo "Downloading glucose-syrup" - @$(DOWNLOADER) http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz - @$(TAR) xfz glucose-syrup.tgz + @$(DOWNLOADER) https://github.com/BrunoDutertre/glucose-syrup/archive/$(glucose_rev).tar.gz + @$(TAR) xfz $(glucose_rev).tar.gz @rm -Rf ../glucose-syrup - @mv glucose-syrup ../ + @mv glucose-syrup-$(glucose_rev) ../glucose-syrup @(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch) - @rm glucose-syrup.tgz + @$(RM) $(glucose_rev).tar.gz cadical_release = rel-1.4.1 cadical-download: diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 35228291219..744def4861b 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -88,10 +88,10 @@ elseif("${sat_impl}" STREQUAL "glucose") message(STATUS "Building solvers with glucose") download_project(PROJ glucose - URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz + URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt - URL_MD5 b6f040a6c28f011f3be994663338f548 + URL_MD5 7c539c62c248b74210aef7414787323a ) add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})