Skip to content

Commit d143452

Browse files
tautschnigtautschnig
committed
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.
1 parent e78eacf commit d143452

File tree

3 files changed

+13
-145
lines changed

3 files changed

+13
-145
lines changed

‎scripts/glucose-syrup-patch

Lines changed: 4 additions & 139 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,3 @@
1-
diff -rupNw glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
2-
--- glucose-syrup/core/Solver.cc 2014-10-03 11:10:21.000000000 +0200
3-
+++ glucose-syrup-patched/core/Solver.cc 2018-04-21 16:58:22.950005391 +0200
4-
@@ -931,7 +931,6 @@ void Solver::uncheckedEnqueue(Lit p, CRe
5-
CRef Solver::propagate() {
6-
CRef confl = CRef_Undef;
7-
int num_props = 0;
8-
- int previousqhead = qhead;
9-
watches.cleanAll();
10-
watchesBin.cleanAll();
11-
unaryWatches.cleanAll();
12-
@@ -1405,7 +1404,9 @@ lbool Solver::search(int nof_conflicts)
13-
decisions++;
14-
next = pickBranchLit();
15-
if (next == lit_Undef) {
16-
+#if 0
17-
printf("c last restart ## conflicts : %d %d \n", conflictC, decisionLevel());
18-
+#endif
19-
// Model found:
20-
return l_True;
21-
}
221
diff -rupNw glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTypes.h
232
--- glucose-syrup/core/SolverTypes.h 2014-10-03 11:10:22.000000000 +0200
243
+++ 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
3211

3312
#include "mtl/IntTypes.h"
3413
#include "mtl/Alg.h"
35-
@@ -170,7 +172,10 @@ class Clause {
36-
unsigned lbd : BITS_LBD;
37-
} header;
38-
39-
+#include <util/pragma_push.def>
40-
+#include <util/pragma_wzero_length_array.def>
41-
union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
42-
+#include <util/pragma_pop.def>
43-
44-
friend class ClauseAllocator;
45-
46-
diff -rupNw glucose-syrup/mtl/Clone.h glucose-syrup-patched/mtl/Clone.h
47-
--- glucose-syrup/mtl/Clone.h 2014-10-03 11:10:22.000000000 +0200
48-
+++ glucose-syrup-patched/mtl/Clone.h 2018-05-10 12:35:25.150491249 +0200
49-
@@ -8,6 +8,6 @@ namespace Glucose {
50-
public:
51-
virtual Clone* clone() const = 0;
52-
};
53-
-};
54-
+}
55-
56-
#endif
57-
\ No newline at end of file
58-
diff -rupNw glucose-syrup/mtl/Clone.h~ glucose-syrup-patched/mtl/Clone.h~
59-
--- glucose-syrup/mtl/Clone.h~ 1970-01-01 01:00:00.000000000 +0100
60-
+++ glucose-syrup-patched/mtl/Clone.h~ 2018-04-21 16:58:22.950005391 +0200
61-
@@ -0,0 +1,13 @@
62-
+#ifndef Glucose_Clone_h
63-
+#define Glucose_Clone_h
64-
+
65-
+
66-
+namespace Glucose {
67-
+
68-
+ class Clone {
69-
+ public:
70-
+ virtual Clone* clone() const = 0;
71-
+ };
72-
+};
73-
+
74-
+#endif
75-
\ No newline at end of file
7614
diff -rupNw glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
7715
--- glucose-syrup/mtl/IntTypes.h 2014-10-03 11:10:22.000000000 +0200
7816
+++ 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
8624

8725
#endif
8826

89-
diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
90-
--- glucose-syrup/mtl/Vec.h 2014-10-03 11:10:22.000000000 +0200
91-
+++ glucose-syrup-patched/mtl/Vec.h 2018-04-21 16:58:22.950005391 +0200
92-
@@ -103,7 +103,7 @@ template<class T>
93-
void vec<T>::capacity(int min_cap) {
94-
if (cap >= min_cap) return;
95-
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
96-
- if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
97-
+ if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
98-
throw OutOfMemoryException();
99-
}
100-
10127
diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
10228
--- glucose-syrup/mtl/Vec.h
10329
+++ glucose-syrup-patched/mtl/Vec.h
104-
@@ -103,8 +103,10 @@
30+
@@ -118,8 +118,10 @@
10531
void vec<T>::capacity(int min_cap) {
10632
if (cap >= min_cap) return;
10733
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
11541

11642

11743
diff -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
118-
--- glucose-syrup/simp/SimpSolver.cc 2014-10-03 11:10:22.000000000 +0200
119-
+++ glucose-syrup-patched/simp/SimpSolver.cc 2018-04-21 16:58:22.950005391 +0200
120-
@@ -319,10 +319,13 @@ bool SimpSolver::merge(const Clause& _ps
121-
if (var(qs[i]) != v){
122-
for (int j = 0; j < ps.size(); j++)
123-
if (var(ps[j]) == var(qs[i]))
124-
+ {
125-
if (ps[j] == ~qs[i])
126-
+
127-
return false;
128-
else
129-
goto next;
130-
+ }
131-
out_clause.push(qs[i]);
132-
}
133-
next:;
134-
@@ -353,10 +356,12 @@ bool SimpSolver::merge(const Clause& _ps
135-
if (var(__qs[i]) != v){
136-
for (int j = 0; j < ps.size(); j++)
137-
if (var(__ps[j]) == var(__qs[i]))
138-
+ {
139-
if (__ps[j] == ~__qs[i])
140-
return false;
141-
else
142-
goto next;
143-
+ }
144-
size++;
145-
}
146-
next:;
147-
@@ -687,11 +692,11 @@ bool SimpSolver::eliminate(bool turn_off
44+
--- glucose-syrup/simp/SimpSolver.cc 2014-10-03 11:10:22.000000000 +0200
45+
+++ glucose-syrup-patched/simp/SimpSolver.cc 2018-04-21 16:58:22.950005391 +0200
46+
@@ -713,11 +713,11 @@ bool SimpSolver::eliminate(bool turn_off
14847
//
14948

15049
int toPerform = clauses.size()<=4800000;
@@ -158,31 +57,6 @@ diff -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolv
15857
while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){
15958

16059
gatherTouchedClauses();
161-
@@ -760,10 +765,11 @@ bool SimpSolver::eliminate(bool turn_off
162-
checkGarbage();
163-
}
164-
165-
+#if 0
166-
if (verbosity >= 0 && elimclauses.size() > 0)
167-
printf("c | Eliminated clauses: %10.2f Mb |\n",
168-
double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
169-
-
170-
+#endif
171-
172-
return ok;
173-
174-
diff -rupNw glucose-syrup/utils/Options.h glucose-syrup-patched/utils/Options.h
175-
--- glucose-syrup/utils/Options.h 2014-10-03 11:10:22.000000000 +0200
176-
+++ glucose-syrup-patched/utils/Options.h 2018-04-21 16:58:22.950005391 +0200
177-
@@ -60,7 +60,7 @@ class Option
178-
struct OptionLt {
179-
bool operator()(const Option* x, const Option* y) {
180-
int test1 = strcmp(x->category, y->category);
181-
- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
182-
+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
183-
}
184-
};
185-
18660
diff -rupNw glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUtils.h
18761
--- glucose-syrup/utils/ParseUtils.h 2014-10-03 11:10:22.000000000 +0200
18862
+++ 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
21791

21892
int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
21993
void operator ++ () { pos++; assureLookahead(); }
220-
@@ -96,7 +96,7 @@
221-
if (*in != '.') printf("PARSE ERROR! Unexpected char: %c\n", *in),exit(3);
222-
++in; // skip dot
223-
currentExponent = 0.1;
224-
- while (*in >= '0' && *in <= '9')
225-
+ while (*in >= '0' && *in <= '9')
226-
accu = accu + currentExponent * ((double)(*in - '0')),
227-
currentExponent /= 10,
228-
++in;
22994
diff -rupNw glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
23095
--- glucose-syrup/utils/System.h 2014-10-03 11:10:22.000000000 +0200
23196
+++ glucose-syrup-patched/utils/System.h 2018-04-21 16:58:22.950005391 +0200

‎src/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -151,12 +151,12 @@ cudd-download:
151151

152152
glucose-download:
153153
@echo "Downloading glucose-syrup"
154-
@$(DOWNLOADER) http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
155-
@$(TAR) xfz glucose-syrup.tgz
154+
@$(DOWNLOADER) https://github.com/BrunoDutertre/glucose-syrup/archive/refs/heads/main.tar.gz
155+
@$(TAR) xfz main.tar.gz
156156
@rm -Rf ../glucose-syrup
157-
@mv glucose-syrup ../
157+
@mv glucose-syrup-main ../glucose-syrup
158158
@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
159-
@rm glucose-syrup.tgz
159+
@$(RM) main.tar.gz
160160

161161
cadical_release = rel-1.4.1
162162
cadical-download:

‎src/solvers/CMakeLists.txt

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -87,11 +87,14 @@ if("${sat_impl}" STREQUAL "minisat2")
8787
elseif("${sat_impl}" STREQUAL "glucose")
8888
message(STATUS "Building solvers with glucose")
8989

90+
# the below MD5 sum is for revision
91+
# 0bb2afd3b9baace6981cbb8b4a1c7683c44968b7; CI will fail if "main" receives
92+
# additional commits
9093
download_project(PROJ glucose
91-
URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
94+
URL https://github.com/BrunoDutertre/glucose-syrup/archive/refs/heads/main.tar.gz
9295
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch
9396
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
94-
URL_MD5 b6f040a6c28f011f3be994663338f548
97+
URL_MD5 89a5183dd9b9eb5296fd9fab2c968a50
9598
)
9699

97100
add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})

0 commit comments

Comments
 (0)