Skip to content

Commit 151c8fe

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 b466503 commit 151c8fe

File tree

3 files changed

+11
-145
lines changed

3 files changed

+11
-145
lines changed

‎scripts/glucose-syrup-patch

+4-139
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

+5-4
Original file line numberDiff line numberDiff line change
@@ -149,14 +149,15 @@ cudd-download:
149149
@echo "Compiling Cudd 3.0.0"
150150
@(cd ../cudd-3.0.0; ./configure; $(MAKE))
151151

152+
glucose_rev = 0bb2afd3b9baace6981cbb8b4a1c7683c44968b7
152153
glucose-download:
153154
@echo "Downloading glucose-syrup"
154-
@$(DOWNLOADER) http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz
155-
@$(TAR) xfz glucose-syrup.tgz
155+
@$(DOWNLOADER) https://github.com/BrunoDutertre/glucose-syrup/archive/$(glucose_rev).tar.gz
156+
@$(TAR) xfz $(glucose_rev).tar.gz
156157
@rm -Rf ../glucose-syrup
157-
@mv glucose-syrup ../
158+
@mv glucose-syrup-$(glucose_rev) ../glucose-syrup
158159
@(cd ../glucose-syrup; patch -p1 < ../scripts/glucose-syrup-patch)
159-
@rm glucose-syrup.tgz
160+
@$(RM) $(glucose_rev).tar.gz
160161

161162
cadical_release = rel-1.4.1
162163
cadical-download:

‎src/solvers/CMakeLists.txt

+2-2
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/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.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 7c539c62c248b74210aef7414787323a
9595
)
9696

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

0 commit comments

Comments
 (0)