|
Lines 136-145
struct clause_t
Link Here
|
| 136 |
#define clause_learnt(c) ((c)->size_learnt & 1) |
136 |
#define clause_learnt(c) ((c)->size_learnt & 1) |
| 137 |
|
137 |
|
| 138 |
#define clause_activity(c) \ |
138 |
#define clause_activity(c) \ |
| 139 |
(*((float*)&(c)->lits[(c)->size_learnt>>1])) |
139 |
(*((lit*)&(c)->lits[(c)->size_learnt>>1])) |
| 140 |
|
140 |
|
| 141 |
#define clause_setactivity(c, a) \ |
141 |
#define clause_setactivity(c, a) \ |
| 142 |
(void)(*((float*)&(c)->lits[(c)->size_learnt>>1]) = (a)) |
142 |
(void)(*((lit*)&(c)->lits[(c)->size_learnt>>1]) = (a)) |
| 143 |
|
143 |
|
| 144 |
/*====================================================================*/ |
144 |
/*====================================================================*/ |
| 145 |
/* Encode literals in clause pointers: */ |
145 |
/* Encode literals in clause pointers: */ |
|
Lines 313-326
static inline void act_clause_rescale(solver* s) {
Link Here
|
| 313 |
clause** cs = (clause**)vecp_begin(&s->learnts); |
313 |
clause** cs = (clause**)vecp_begin(&s->learnts); |
| 314 |
int i; |
314 |
int i; |
| 315 |
for (i = 0; i < vecp_size(&s->learnts); i++){ |
315 |
for (i = 0; i < vecp_size(&s->learnts); i++){ |
| 316 |
float a = clause_activity(cs[i]); |
316 |
float a = (float)clause_activity(cs[i]); |
| 317 |
clause_setactivity(cs[i], a * (float)1e-20); |
317 |
clause_setactivity(cs[i], a * (float)1e-20); |
| 318 |
} |
318 |
} |
| 319 |
s->cla_inc *= (float)1e-20; |
319 |
s->cla_inc *= (float)1e-20; |
| 320 |
} |
320 |
} |
| 321 |
|
321 |
|
| 322 |
static inline void act_clause_bump(solver* s, clause *c) { |
322 |
static inline void act_clause_bump(solver* s, clause *c) { |
| 323 |
float a = clause_activity(c) + s->cla_inc; |
323 |
float a = (float)clause_activity(c) + s->cla_inc; |
| 324 |
clause_setactivity(c,a); |
324 |
clause_setactivity(c,a); |
| 325 |
if (a > 1e20) act_clause_rescale(s); |
325 |
if (a > 1e20) act_clause_rescale(s); |
| 326 |
} |
326 |
} |
|
Lines 356-362
static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
Link Here
|
| 356 |
c->lits[i] = begin[i]; |
356 |
c->lits[i] = begin[i]; |
| 357 |
|
357 |
|
| 358 |
if (learnt) |
358 |
if (learnt) |
| 359 |
*((float*)&c->lits[size]) = 0.0; |
359 |
*((lit*)&c->lits[size]) = 0; |
| 360 |
|
360 |
|
| 361 |
assert(begin[0] >= 0); |
361 |
assert(begin[0] >= 0); |
| 362 |
assert(begin[0] < s->size*2); |
362 |
assert(begin[0] < s->size*2); |
| 363 |
- |
|
|
