Skip to content

Commit b196bdd

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 95d8c91 commit b196bdd

File tree

3 files changed

+10
-145
lines changed

3 files changed

+10
-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
@@ -114,36 +40,9 @@ diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
11440
}
11541

11642

117-
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:;
43+
-diff -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
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
14746
@@ -687,11 +692,11 @@ bool SimpSolver::eliminate(bool turn_off
14847
//
14948

@@ -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
@@ -149,12 +149,12 @@ cudd-download:
149149

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

159159
cadical_release = rel-1.4.1
160160
cadical-download:

‎src/solvers/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -88,10 +88,10 @@ elseif("${sat_impl}" STREQUAL "glucose")
8888
message(STATUS "Building solvers with glucose")
8989

9090
download_project(PROJ glucose
91-
URL http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
91+
URL https://github.com/BrunoDutertre/glucose-syrup/archive/refs/heads/main.tar.gz
9292
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/glucose-syrup-patch
9393
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/glucose_CMakeLists.txt CMakeLists.txt
94-
URL_MD5 b6f040a6c28f011f3be994663338f548
94+
URL_MD5 89a5183dd9b9eb5296fd9fab2c968a50
9595
)
9696

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

0 commit comments

Comments
 (0)