Skip to content

Commit aa3caa3

Browse files
author
Matthias Güdemann
committed
Fix CMake build for Glucose Syrup
1 parent 290feb4 commit aa3caa3

File tree

2 files changed

+84
-20
lines changed

2 files changed

+84
-20
lines changed

‎scripts/glucose-syrup-patch‎

Lines changed: 82 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
diff -rupN glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
2-
--- glucose-syrup/core/Solver.cc 2014-10-03 10:10:21.000000000 +0100
3-
+++ glucose-syrup-patched/core/Solver.cc 2016-07-08 13:06:02.772186004 +0100
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
44
@@ -931,7 +931,6 @@ void Solver::uncheckedEnqueue(Lit p, CRe
55
CRef Solver::propagate() {
66
CRef confl = CRef_Undef;
@@ -19,9 +19,9 @@ diff -rupN glucose-syrup/core/Solver.cc glucose-syrup-patched/core/Solver.cc
1919
// Model found:
2020
return l_True;
2121
}
22-
diff -rupN glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTypes.h
23-
--- glucose-syrup/core/SolverTypes.h 2014-10-03 10:10:22.000000000 +0100
24-
+++ glucose-syrup-patched/core/SolverTypes.h 2016-07-08 13:06:02.772186004 +0100
22+
diff -rupNw glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTypes.h
23+
--- glucose-syrup/core/SolverTypes.h 2014-10-03 11:10:22.000000000 +0200
24+
+++ glucose-syrup-patched/core/SolverTypes.h 2018-04-21 16:58:22.950005391 +0200
2525
@@ -53,7 +53,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
2626

2727
#include <assert.h>
@@ -32,9 +32,20 @@ diff -rupN glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTyp
3232

3333
#include "mtl/IntTypes.h"
3434
#include "mtl/Alg.h"
35-
diff -rupN glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
36-
--- glucose-syrup/mtl/IntTypes.h 2014-10-03 10:10:22.000000000 +0100
37-
+++ glucose-syrup-patched/mtl/IntTypes.h 2016-07-08 13:06:02.772186004 +0100
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/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
47+
--- glucose-syrup/mtl/IntTypes.h 2014-10-03 11:10:22.000000000 +0200
48+
+++ glucose-syrup-patched/mtl/IntTypes.h 2018-04-21 16:58:22.950005391 +0200
3849
@@ -31,7 +31,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
3950
#else
4051

@@ -45,10 +56,49 @@ diff -rupN glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
4556

4657
#endif
4758

48-
diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
49-
--- glucose-syrup/simp/SimpSolver.cc 2014-10-03 10:10:22.000000000 +0100
50-
+++ glucose-syrup-patched/simp/SimpSolver.cc 2016-07-08 13:07:00.396187548 +0100
51-
@@ -687,11 +687,11 @@ bool SimpSolver::eliminate(bool turn_off
59+
diff -rupNw glucose-syrup/mtl/Vec.h glucose-syrup-patched/mtl/Vec.h
60+
--- glucose-syrup/mtl/Vec.h 2014-10-03 11:10:22.000000000 +0200
61+
+++ glucose-syrup-patched/mtl/Vec.h 2018-04-21 16:58:22.950005391 +0200
62+
@@ -103,7 +103,7 @@ template<class T>
63+
void vec<T>::capacity(int min_cap) {
64+
if (cap >= min_cap) return;
65+
int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2
66+
- if (add > INT_MAX - cap || ((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)
67+
+ if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM))
68+
throw OutOfMemoryException();
69+
}
70+
71+
diff -rupNw glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolver.cc
72+
--- glucose-syrup/simp/SimpSolver.cc 2014-10-03 11:10:22.000000000 +0200
73+
+++ glucose-syrup-patched/simp/SimpSolver.cc 2018-04-21 16:58:22.950005391 +0200
74+
@@ -319,10 +319,13 @@ bool SimpSolver::merge(const Clause& _ps
75+
if (var(qs[i]) != v){
76+
for (int j = 0; j < ps.size(); j++)
77+
if (var(ps[j]) == var(qs[i]))
78+
+ {
79+
if (ps[j] == ~qs[i])
80+
+
81+
return false;
82+
else
83+
goto next;
84+
+ }
85+
out_clause.push(qs[i]);
86+
}
87+
next:;
88+
@@ -353,10 +356,12 @@ bool SimpSolver::merge(const Clause& _ps
89+
if (var(__qs[i]) != v){
90+
for (int j = 0; j < ps.size(); j++)
91+
if (var(__ps[j]) == var(__qs[i]))
92+
+ {
93+
if (__ps[j] == ~__qs[i])
94+
return false;
95+
else
96+
goto next;
97+
+ }
98+
size++;
99+
}
100+
next:;
101+
@@ -687,11 +692,11 @@ bool SimpSolver::eliminate(bool turn_off
52102
//
53103

54104
int toPerform = clauses.size()<=4800000;
@@ -62,7 +112,7 @@ diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolve
62112
while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){
63113

64114
gatherTouchedClauses();
65-
@@ -760,10 +760,11 @@ bool SimpSolver::eliminate(bool turn_off
115+
@@ -760,10 +765,11 @@ bool SimpSolver::eliminate(bool turn_off
66116
checkGarbage();
67117
}
68118

@@ -75,9 +125,21 @@ diff -rupN glucose-syrup/simp/SimpSolver.cc glucose-syrup-patched/simp/SimpSolve
75125

76126
return ok;
77127

78-
diff -rupN glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUtils.h
79-
--- glucose-syrup/utils/ParseUtils.h 2014-10-03 10:10:22.000000000 +0100
80-
+++ glucose-syrup-patched/utils/ParseUtils.h 2016-07-08 13:06:02.772186004 +0100
128+
diff -rupNw glucose-syrup/utils/Options.h glucose-syrup-patched/utils/Options.h
129+
--- glucose-syrup/utils/Options.h 2014-10-03 11:10:22.000000000 +0200
130+
+++ glucose-syrup-patched/utils/Options.h 2018-04-21 16:58:22.950005391 +0200
131+
@@ -60,7 +60,7 @@ class Option
132+
struct OptionLt {
133+
bool operator()(const Option* x, const Option* y) {
134+
int test1 = strcmp(x->category, y->category);
135+
- return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0;
136+
+ return test1 < 0 || (test1 == 0 && strcmp(x->type_name, y->type_name) < 0);
137+
}
138+
};
139+
140+
diff -rupNw glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUtils.h
141+
--- glucose-syrup/utils/ParseUtils.h 2014-10-03 11:10:22.000000000 +0200
142+
+++ glucose-syrup-patched/utils/ParseUtils.h 2018-04-21 16:58:22.950005391 +0200
81143
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR
82144
#include <stdio.h>
83145
#include <math.h>
@@ -109,9 +171,9 @@ diff -rupN glucose-syrup/utils/ParseUtils.h glucose-syrup-patched/utils/ParseUti
109171

110172
int operator * () const { return (pos >= size) ? EOF : buf[pos]; }
111173
void operator ++ () { pos++; assureLookahead(); }
112-
diff -rupN glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
113-
--- glucose-syrup/utils/System.h 2014-10-03 10:10:22.000000000 +0100
114-
+++ glucose-syrup-patched/utils/System.h 2016-07-08 13:06:02.776186005 +0100
174+
diff -rupNw glucose-syrup/utils/System.h glucose-syrup-patched/utils/System.h
175+
--- glucose-syrup/utils/System.h 2014-10-03 11:10:22.000000000 +0200
176+
+++ glucose-syrup-patched/utils/System.h 2018-04-21 16:58:22.950005391 +0200
115177
@@ -60,8 +60,11 @@ static inline double Glucose::cpuTime(vo
116178

117179
// Laurent: I know that this will not compile directly under Windows... sorry for that

‎scripts/glucose_CMakeLists.txt‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,3 +18,5 @@ target_include_directories(glucose-condensed
1818
PUBLIC
1919
${CMAKE_CURRENT_SOURCE_DIR}
2020
)
21+
22+
target_link_libraries(glucose-condensed util)

0 commit comments

Comments
 (0)