1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
Stolen from Fedora:
https://src.fedoraproject.org/rpms/glpk/raw/rawhide/f/glpk-4.65-alias.patch
diff -urN glpk-4.65.orig/src/minisat/minisat.c glpk-4.65/src/minisat/minisat.c
--- glpk-4.65.orig/src/minisat/minisat.c 2018-02-16 00:00:00.000000000 -0700
+++ glpk-4.65/src/minisat/minisat.c 2018-05-20 18:54:25.106624859 -0600
@@ -135,11 +135,11 @@ struct clause_t
#define clause_learnt(c) ((c)->size_learnt & 1)
-#define clause_activity(c) \
- (*((float*)&(c)->lits[(c)->size_learnt>>1]))
+#define clause_activity(c, a) \
+ memcpy(&(a), &(c)->lits[(c)->size_learnt>>1], sizeof(float))
#define clause_setactivity(c, a) \
- (void)(*((float*)&(c)->lits[(c)->size_learnt>>1]) = (a))
+ memcpy(&(c)->lits[(c)->size_learnt>>1], &(a), sizeof(float))
/*====================================================================*/
/* Encode literals in clause pointers: */
@@ -313,14 +313,18 @@ static inline void act_clause_rescale(so
clause** cs = (clause**)vecp_begin(&s->learnts);
int i;
for (i = 0; i < vecp_size(&s->learnts); i++){
- float a = clause_activity(cs[i]);
- clause_setactivity(cs[i], a * (float)1e-20);
+ float a;
+ clause_activity(cs[i], a);
+ a *= (float)1e-20;
+ clause_setactivity(cs[i], a);
}
s->cla_inc *= (float)1e-20;
}
static inline void act_clause_bump(solver* s, clause *c) {
- float a = clause_activity(c) + s->cla_inc;
+ float a;
+ clause_activity(c, a);
+ a += s->cla_inc;
clause_setactivity(c,a);
if (a > 1e20) act_clause_rescale(s);
}
@@ -356,7 +360,7 @@ static clause* clause_new(solver* s, lit
c->lits[i] = begin[i];
if (learnt)
- *((float*)&c->lits[size]) = 0.0;
+ memset(&c->lits[size], 0, sizeof(float));
assert(begin[0] >= 0);
assert(begin[0] < s->size*2);
@@ -850,10 +854,17 @@ clause* solver_propagate(solver* s)
}
static inline int clause_cmp (const void* x, const void* y) {
- return clause_size((clause*)x) > 2
- && (clause_size((clause*)y) == 2
- || clause_activity((clause*)x)
- < clause_activity((clause*)y)) ? -1 : 1; }
+ clause *cx = (clause *)x;
+ clause *cy = (clause *)y;
+ float fx, fy;
+ if (clause_size(cx) <= 2)
+ return 1;
+ if (clause_size(cy) == 2)
+ return -1;
+ clause_activity(cx, fx);
+ clause_activity(cy, fy);
+ return fx < fy ? -1 : 1;
+}
void solver_reducedb(solver* s)
{
@@ -874,10 +885,12 @@ void solver_reducedb(solver* s)
learnts[j++] = learnts[i];
}
for (; i < vecp_size(&s->learnts); i++){
+ float f;
+ clause_activity(learnts[i], f);
if (clause_size(learnts[i]) > 2
&& reasons[lit_var(*clause_begin(learnts[i]))]
!= learnts[i]
- && clause_activity(learnts[i]) < extra_lim)
+ && f < extra_lim)
clause_remove(s,learnts[i]);
else
learnts[j++] = learnts[i];
|
GitWeb