Skip to content

Commit c00319e

Browse files
TGWDBTGWDB
authored
Merge pull request #6539 from tautschnig/glucose-github
Switch Glucose download source to GitHub
2 parents b466503 + 151c8fe commit c00319e

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)