1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 sls_engine.cpp
7
8 Abstract:
9
10 A Stochastic Local Search (SLS) engine
11
12 Author:
13
14 Christoph (cwinter) 2014-03-19
15
16 Notes:
17
18 --*/
19 #include<float.h> // Need DBL_MAX
20
21 #include "util/map.h"
22 #include "ast/ast_smt2_pp.h"
23 #include "ast/ast_pp.h"
24 #include "ast/rewriter/var_subst.h"
25 #include "model/model_pp.h"
26 #include "tactic/tactic.h"
27 #include "util/luby.h"
28
29 #include "tactic/sls/sls_params.hpp"
30 #include "tactic/sls/sls_engine.h"
31
32
sls_engine(ast_manager & m,params_ref const & p)33 sls_engine::sls_engine(ast_manager & m, params_ref const & p) :
34 m_manager(m),
35 m_powers(m_mpz_manager),
36 m_zero(m_mpz_manager.mk_z(0)),
37 m_one(m_mpz_manager.mk_z(1)),
38 m_two(m_mpz_manager.mk_z(2)),
39 m_bv_util(m),
40 m_tracker(m, m_bv_util, m_mpz_manager, m_powers),
41 m_evaluator(m, m_bv_util, m_tracker, m_mpz_manager, m_powers)
42 {
43 updt_params(p);
44 m_tracker.updt_params(p);
45 }
46
~sls_engine()47 sls_engine::~sls_engine() {
48 m_mpz_manager.del(m_zero);
49 m_mpz_manager.del(m_one);
50 m_mpz_manager.del(m_two);
51 }
52
updt_params(params_ref const & _p)53 void sls_engine::updt_params(params_ref const & _p) {
54 sls_params p(_p);
55 m_produce_models = _p.get_bool("model", false);
56 m_max_restarts = p.max_restarts();
57 m_tracker.set_random_seed(p.random_seed());
58 m_walksat = p.walksat();
59 m_walksat_repick = p.walksat_repick();
60 m_paws_sp = p.paws_sp();
61 m_paws = m_paws_sp < 1024;
62 m_wp = p.wp();
63 m_vns_mc = p.vns_mc();
64 m_vns_repick = p.vns_repick();
65
66 m_restart_base = p.restart_base();
67 m_restart_next = m_restart_base;
68 m_restart_init = p.restart_init();
69
70 m_early_prune = p.early_prune();
71 m_random_offset = p.random_offset();
72 m_rescore = p.rescore();
73
74 // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT.
75 if (m_walksat_repick && !m_walksat)
76 NOT_IMPLEMENTED_YET();
77 if (m_vns_repick && !m_walksat)
78 NOT_IMPLEMENTED_YET();
79 }
80
collect_statistics(statistics & st) const81 void sls_engine::collect_statistics(statistics& st) const {
82 double seconds = m_stats.m_stopwatch.get_current_seconds();
83 st.update("sls restarts", m_stats.m_restarts);
84 st.update("sls full evals", m_stats.m_full_evals);
85 st.update("sls incr evals", m_stats.m_incr_evals);
86 st.update("sls incr evals/sec", m_stats.m_incr_evals / seconds);
87 st.update("sls FLIP moves", m_stats.m_flips);
88 st.update("sls INC moves", m_stats.m_incs);
89 st.update("sls DEC moves", m_stats.m_decs);
90 st.update("sls INV moves", m_stats.m_invs);
91 st.update("sls moves", m_stats.m_moves);
92 st.update("sls moves/sec", m_stats.m_moves / seconds);
93 }
94
checkpoint()95 void sls_engine::checkpoint() {
96 tactic::checkpoint(m_manager);
97 }
98
full_eval(model & mdl)99 bool sls_engine::full_eval(model & mdl) {
100 model::scoped_model_completion _scm(mdl, true);
101 for (expr* a : m_assertions) {
102 checkpoint();
103 if (!mdl.is_true(a)) {
104 TRACE("sls", tout << "Evaluation: false\n";);
105 return false;
106 }
107 }
108 return true;
109 }
110
top_score()111 double sls_engine::top_score() {
112 double top_sum = 0.0;
113 for (expr* e : m_assertions) {
114 top_sum += m_tracker.get_score(e);
115 }
116
117 TRACE("sls_top", tout << "Score distribution:";
118 for (expr* e : m_assertions)
119 tout << " " << m_tracker.get_score(e);
120 tout << " AVG: " << top_sum / (double)m_assertions.size() << std::endl;);
121
122 m_tracker.set_top_sum(top_sum);
123
124 return top_sum;
125 }
126
rescore()127 double sls_engine::rescore() {
128 m_evaluator.update_all();
129 m_stats.m_full_evals++;
130 return top_score();
131 }
132
serious_score(func_decl * fd,const mpz & new_value)133 double sls_engine::serious_score(func_decl * fd, const mpz & new_value) {
134 m_evaluator.serious_update(fd, new_value);
135 m_stats.m_incr_evals++;
136 return m_tracker.get_top_sum();
137 }
138
incremental_score(func_decl * fd,const mpz & new_value)139 double sls_engine::incremental_score(func_decl * fd, const mpz & new_value) {
140 m_evaluator.update(fd, new_value);
141 m_stats.m_incr_evals++;
142 return m_tracker.get_top_sum();
143 }
144
incremental_score_prune(func_decl * fd,const mpz & new_value)145 double sls_engine::incremental_score_prune(func_decl * fd, const mpz & new_value) {
146 m_stats.m_incr_evals++;
147 if (m_evaluator.update_prune(fd, new_value))
148 return m_tracker.get_top_sum();
149 else
150 return -DBL_MAX;
151 }
152
153 // checks whether the score outcome of a given move is better than the previous score
what_if(func_decl * fd,const unsigned & fd_inx,const mpz & temp,double & best_score,unsigned & best_const,mpz & best_value)154 bool sls_engine::what_if(
155 func_decl * fd,
156 const unsigned & fd_inx,
157 const mpz & temp,
158 double & best_score,
159 unsigned & best_const,
160 mpz & best_value) {
161
162 #ifdef Z3DEBUG
163 mpz old_value;
164 m_mpz_manager.set(old_value, m_tracker.get_value(fd));
165 #endif
166
167 double r;
168 if (m_early_prune)
169 r = incremental_score_prune(fd, temp);
170 else
171 r = incremental_score(fd, temp);
172 #ifdef Z3DEBUG
173 TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
174 " --> " << r << std::endl;);
175
176 m_mpz_manager.del(old_value);
177 #endif
178
179 // Andreas: Had this idea on my last day. Maybe we could add a noise here similar to the one that worked so well for ucb assertion selection.
180 // r += 0.0001 * m_tracker.get_random_uint(8);
181
182 // Andreas: For some reason it is important to use > here instead of >=. Probably related to preferring the LSB.
183 if (r > best_score) {
184 best_score = r;
185 best_const = fd_inx;
186 m_mpz_manager.set(best_value, temp);
187 return true;
188 }
189
190 return false;
191 }
192
mk_add(unsigned bv_sz,const mpz & old_value,mpz & add_value,mpz & result)193 void sls_engine::mk_add(unsigned bv_sz, const mpz & old_value, mpz & add_value, mpz & result) {
194 mpz temp, mask, mask2;
195 m_mpz_manager.add(old_value, add_value, temp);
196 m_mpz_manager.set(mask, m_powers(bv_sz));
197 m_mpz_manager.bitwise_not(bv_sz, mask, mask2);
198 m_mpz_manager.bitwise_and(temp, mask2, result);
199 m_mpz_manager.del(temp);
200 m_mpz_manager.del(mask);
201 m_mpz_manager.del(mask2);
202
203 }
204
mk_inc(unsigned bv_sz,const mpz & old_value,mpz & incremented)205 void sls_engine::mk_inc(unsigned bv_sz, const mpz & old_value, mpz & incremented) {
206 unsigned shift;
207 m_mpz_manager.add(old_value, m_one, incremented);
208 if (m_mpz_manager.is_power_of_two(incremented, shift) && shift == bv_sz)
209 m_mpz_manager.set(incremented, m_zero);
210 }
211
mk_dec(unsigned bv_sz,const mpz & old_value,mpz & decremented)212 void sls_engine::mk_dec(unsigned bv_sz, const mpz & old_value, mpz & decremented) {
213 if (m_mpz_manager.is_zero(old_value)) {
214 m_mpz_manager.set(decremented, m_powers(bv_sz));
215 m_mpz_manager.dec(decremented);
216 }
217 else
218 m_mpz_manager.sub(old_value, m_one, decremented);
219 }
220
mk_inv(unsigned bv_sz,const mpz & old_value,mpz & inverted)221 void sls_engine::mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted) {
222 m_mpz_manager.bitwise_not(bv_sz, old_value, inverted);
223 }
224
mk_flip(sort * s,const mpz & old_value,unsigned bit,mpz & flipped)225 void sls_engine::mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped) {
226 m_mpz_manager.set(flipped, m_zero);
227
228 if (m_bv_util.is_bv_sort(s)) {
229 mpz mask;
230 m_mpz_manager.set(mask, m_powers(bit));
231 m_mpz_manager.bitwise_xor(old_value, mask, flipped);
232 m_mpz_manager.del(mask);
233 }
234 else if (m_manager.is_bool(s))
235 m_mpz_manager.set(flipped, (m_mpz_manager.is_zero(old_value)) ? m_one : m_zero);
236 else
237 NOT_IMPLEMENTED_YET();
238 }
239
mk_random_move(ptr_vector<func_decl> & unsat_constants)240 void sls_engine::mk_random_move(ptr_vector<func_decl> & unsat_constants)
241 {
242 unsigned rnd_mv = 0;
243 unsigned ucc = unsat_constants.size();
244 unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc;
245 func_decl * fd = unsat_constants[rc];
246
247 mpz new_value;
248
249 sort * srt = fd->get_range();
250 if (m_manager.is_bool(srt))
251 m_mpz_manager.set(new_value, (m_mpz_manager.is_zero(m_tracker.get_value(fd))) ? m_one : m_zero);
252 else
253 {
254 if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv = 2;
255 if (m_mpz_manager.is_one(m_tracker.get_random_bool())) rnd_mv++;
256
257 // Andreas: The other option would be to scale the probability for flips according to the bit-width.
258 /* unsigned bv_sz2 = m_bv_util.get_bv_size(srt);
259 rnd_mv = m_tracker.get_random_uint(16) % (bv_sz2 + 3);
260 if (rnd_mv > 3) rnd_mv = 0; */
261
262 move_type mt = (move_type)rnd_mv;
263
264 // Andreas: Christoph claimed inversion doesn't make sense, let's do a flip instead. Is this really true?
265 if (mt == MV_INV) mt = MV_FLIP;
266 unsigned bit = 0;
267
268 switch (mt)
269 {
270 case MV_FLIP: {
271 unsigned bv_sz = m_bv_util.get_bv_size(srt);
272 bit = (m_tracker.get_random_uint((bv_sz < 16) ? 4 : (bv_sz < 256) ? 8 : (bv_sz < 4096) ? 12 : (bv_sz < 65536) ? 16 : 32)) % bv_sz;
273 mk_flip(fd->get_range(), m_tracker.get_value(fd), bit, new_value);
274 break;
275 }
276 case MV_INC:
277 mk_inc(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
278 break;
279 case MV_DEC:
280 mk_dec(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
281 break;
282 case MV_INV:
283 mk_inv(m_bv_util.get_bv_size(fd->get_range()), m_tracker.get_value(fd), new_value);
284 break;
285 default:
286 NOT_IMPLEMENTED_YET();
287 }
288
289 TRACE("sls", tout << "Randomization candidates: ";
290 for (unsigned i = 0; i < unsat_constants.size(); i++)
291 tout << unsat_constants[i]->get_name() << ", ";
292 tout << std::endl;
293 tout << "Random move: ";
294 switch (mt) {
295 case MV_FLIP: tout << "Flip #" << bit << " in " << fd->get_name() << std::endl; break;
296 case MV_INC: tout << "+1 for " << fd->get_name() << std::endl; break;
297 case MV_DEC: tout << "-1 for " << fd->get_name() << std::endl; break;
298 case MV_INV: tout << "NEG for " << fd->get_name() << std::endl; break;
299 }
300 tout << "Locally randomized model: " << std::endl; m_tracker.show_model(tout););
301 }
302
303 m_evaluator.serious_update(fd, new_value);
304 m_mpz_manager.del(new_value);
305 }
306
307 // finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
find_best_move(ptr_vector<func_decl> & to_evaluate,double score,unsigned & best_const,mpz & best_value,unsigned & new_bit,move_type & move)308 double sls_engine::find_best_move(
309 ptr_vector<func_decl> & to_evaluate,
310 double score,
311 unsigned & best_const,
312 mpz & best_value,
313 unsigned & new_bit,
314 move_type & move)
315 {
316 mpz old_value, temp;
317 unsigned bv_sz;
318 double new_score = score;
319
320 // Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list.
321 unsigned sz = to_evaluate.size();
322 unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0;
323 for (unsigned j = 0; j < sz; j++) {
324 unsigned i = j + offset;
325 if (i >= sz) i -= sz;
326 //for (unsigned i = 0; i < to_evaluate.size(); i++) {
327 func_decl * fd = to_evaluate[i];
328 sort * srt = fd->get_range();
329 bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
330 m_mpz_manager.set(old_value, m_tracker.get_value(fd));
331
332 // first try to flip every bit
333 for (unsigned j = 0; j < bv_sz; j++) {
334 // What would happen if we flipped bit #i ?
335 mk_flip(srt, old_value, j, temp);
336
337 if (what_if(fd, i, temp, new_score, best_const, best_value)) {
338 new_bit = j;
339 move = MV_FLIP;
340 }
341 }
342
343 if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
344 if (!m_mpz_manager.is_even(old_value)) {
345 // for odd values, try +1
346 mk_inc(bv_sz, old_value, temp);
347 if (what_if(fd, i, temp, new_score, best_const, best_value))
348 move = MV_INC;
349 }
350 else {
351 // for even values, try -1
352 mk_dec(bv_sz, old_value, temp);
353 if (what_if(fd, i, temp, new_score, best_const, best_value))
354 move = MV_DEC;
355 }
356 // try inverting
357 mk_inv(bv_sz, old_value, temp);
358 if (what_if(fd, i, temp, new_score, best_const, best_value))
359 move = MV_INV;
360 }
361 // reset to what it was before
362 incremental_score(fd, old_value);
363 }
364
365 m_mpz_manager.del(old_value);
366 m_mpz_manager.del(temp);
367
368 return new_score;
369 }
370
371 // finds the move that increased score the most. returns best_const = -1, if no increasing move exists.
find_best_move_mc(ptr_vector<func_decl> & to_evaluate,double score,unsigned & best_const,mpz & best_value)372 double sls_engine::find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double score,
373 unsigned & best_const, mpz & best_value) {
374 mpz old_value, temp, temp2;
375 unsigned bv_sz;
376 double new_score = score;
377
378 // Andreas: Introducting a bit of randomization by using a random offset and a random direction to go through the candidate list.
379 unsigned sz = to_evaluate.size();
380 unsigned offset = (m_random_offset) ? m_tracker.get_random_uint(16) % sz : 0;
381 for (unsigned j = 0; j < sz; j++) {
382 unsigned i = j + offset;
383 if (i >= sz) i -= sz;
384 //for (unsigned i = 0; i < to_evaluate.size(); i++) {
385 func_decl * fd = to_evaluate[i];
386 sort * srt = fd->get_range();
387 bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
388 m_mpz_manager.set(old_value, m_tracker.get_value(fd));
389
390 if (m_bv_util.is_bv_sort(srt) && bv_sz > 2) {
391 for (unsigned j = 0; j < bv_sz; j++) {
392 mk_flip(srt, old_value, j, temp);
393 for (unsigned l = 0; l < m_vns_mc && l < bv_sz / 2; l++)
394 {
395 unsigned k = m_tracker.get_random_uint(16) % bv_sz;
396 while (k == j)
397 k = m_tracker.get_random_uint(16) % bv_sz;
398 mk_flip(srt, temp, k, temp2);
399 what_if(fd, i, temp2, new_score, best_const, best_value);
400 }
401 }
402 }
403 // reset to what it was before
404 incremental_score(fd, old_value);
405 }
406
407 m_mpz_manager.del(old_value);
408 m_mpz_manager.del(temp);
409 m_mpz_manager.del(temp2);
410
411 return new_score;
412 }
413
414 // main search loop
search()415 lbool sls_engine::search() {
416 lbool res = l_undef;
417 double score = 0.0, old_score = 0.0;
418 unsigned new_const = (unsigned)-1, new_bit;
419 mpz new_value;
420 move_type move;
421
422 score = rescore();
423 unsigned sz = m_assertions.size();
424
425 while (check_restart(m_stats.m_moves)) {
426 checkpoint();
427 m_stats.m_moves++;
428
429 // Andreas: Every base restart interval ...
430 if (m_stats.m_moves % m_restart_base == 0)
431 {
432 // ... potentially smooth the touched counters ...
433 m_tracker.ucb_forget(m_assertions);
434 // ... or normalize the top-level score.
435 if (m_rescore) score = rescore();
436 }
437
438 // get candidate variables
439 ptr_vector<func_decl> & to_evaluate = m_tracker.get_unsat_constants(m_assertions);
440 if (to_evaluate.empty())
441 {
442 res = l_true;
443 goto bailout;
444 }
445
446 // random walk with probability wp / 1024
447 if (m_wp && m_tracker.get_random_uint(10) < m_wp)
448 {
449 mk_random_move(to_evaluate);
450 score = m_tracker.get_top_sum();
451 continue;
452 }
453
454 old_score = score;
455 new_const = (unsigned)-1;
456
457 // find best increasing move
458 score = find_best_move(to_evaluate, score, new_const, new_value, new_bit, move);
459
460 // use Monte Carlo 2-bit-flip sampling if no increasing move was found previously
461 if (m_vns_mc && (new_const == static_cast<unsigned>(-1)))
462 score = find_best_move_mc(to_evaluate, score, new_const, new_value);
463
464 // repick assertion if no increasing move was found previously
465 if (m_vns_repick && (new_const == static_cast<unsigned>(-1)))
466 {
467 expr * q = m_tracker.get_new_unsat_assertion(m_assertions);
468 // only apply if another unsatisfied assertion actually exists
469 if (q)
470 {
471 ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(q);
472 score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move);
473
474 if (new_const != static_cast<unsigned>(-1)) {
475 func_decl * fd = to_evaluate2[new_const];
476 score = serious_score(fd, new_value);
477 continue;
478 }
479 }
480 }
481
482 // randomize if no increasing move was found
483 if (new_const == static_cast<unsigned>(-1)) {
484 score = old_score;
485 if (m_walksat_repick)
486 m_evaluator.randomize_local(m_assertions);
487 else
488 m_evaluator.randomize_local(to_evaluate);
489
490 score = m_tracker.get_top_sum();
491
492 // update assertion weights if a weighting is enabled (sp < 1024)
493 if (m_paws)
494 {
495 for (unsigned i = 0; i < sz; i++)
496 {
497 expr * q = m_assertions[i];
498 // smooth weights with probability sp / 1024
499 if (m_tracker.get_random_uint(10) < m_paws_sp)
500 {
501 if (m_mpz_manager.eq(m_tracker.get_value(q),m_one))
502 m_tracker.decrease_weight(q);
503 }
504 // increase weights otherwise
505 else
506 {
507 if (m_mpz_manager.eq(m_tracker.get_value(q),m_zero))
508 m_tracker.increase_weight(q);
509 }
510 }
511 }
512 }
513 // otherwise, apply most increasing move
514 else {
515 func_decl * fd = to_evaluate[new_const];
516 score = serious_score(fd, new_value);
517 }
518 }
519
520 bailout:
521 m_mpz_manager.del(new_value);
522
523 return res;
524 }
525
operator ()(goal_ref const & g,model_converter_ref & mc)526 void sls_engine::operator()(goal_ref const & g, model_converter_ref & mc) {
527 if (g->inconsistent()) {
528 mc = nullptr;
529 return;
530 }
531
532 m_produce_models = g->models_enabled();
533
534 for (unsigned i = 0; i < g->size(); i++)
535 assert_expr(g->form(i));
536
537 lbool res = operator()();
538
539 if (res == l_true) {
540 report_tactic_progress("Number of flips:", m_stats.m_moves);
541 for (unsigned i = 0; i < g->size(); i++)
542 if (!m_mpz_manager.is_one(m_tracker.get_value(g->form(i))))
543 {
544 verbose_stream() << "Terminated before all assertions were SAT!" << std::endl;
545 NOT_IMPLEMENTED_YET();
546 }
547
548 if (m_produce_models) {
549 model_ref mdl = m_tracker.get_model();
550 mc = model2model_converter(mdl.get());
551 TRACE("sls_model", mc->display(tout););
552 }
553 g->reset();
554 }
555 else
556 mc = nullptr;
557 }
558
operator ()()559 lbool sls_engine::operator()() {
560 m_tracker.initialize(m_assertions);
561 m_tracker.reset(m_assertions);
562 if (m_restart_init)
563 m_tracker.randomize(m_assertions);
564
565 lbool res = l_undef;
566
567 do {
568 checkpoint();
569
570 report_tactic_progress("Searching... restarts left:", m_max_restarts - m_stats.m_restarts);
571 res = search();
572
573 if (res == l_undef)
574 {
575 if (m_restart_init)
576 m_tracker.randomize(m_assertions);
577 else
578 m_tracker.reset(m_assertions);
579 }
580 } while (res != l_true && m_stats.m_restarts++ < m_max_restarts);
581
582 verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl;
583
584 return res;
585 }
586
587 /* Andreas: Needed for Armin's restart scheme if we don't want to use loops.
588 double sls_engine::get_restart_armin(unsigned cnt_restarts)
589 {
590 unsigned outer_id = (unsigned)(0.5 + sqrt(0.25 + 2 * cnt_restarts));
591 unsigned inner_id = cnt_restarts - (outer_id - 1) * outer_id / 2;
592 return pow((double) _RESTART_CONST_ARMIN_, (int) inner_id + 1);
593 }
594 */
595
check_restart(unsigned curr_value)596 unsigned sls_engine::check_restart(unsigned curr_value)
597 {
598 if (curr_value > m_restart_next)
599 {
600 /* Andreas: My own scheme (= 1) seems to work best. Other schemes are disabled so that we save one parameter.
601 I leave the other versions as comments in case you want to try it again somewhen.
602 #if _RESTART_SCHEME_ == 5
603 m_restart_next += (unsigned)(m_restart_base * pow(_RESTART_CONST_ARMIN_, m_stats.m_restarts));
604 #elif _RESTART_SCHEME_ == 4
605 m_restart_next += (m_stats.m_restarts & (m_stats.m_restarts + 1)) ? m_restart_base : (m_restart_base * m_stats.m_restarts + 1);
606 #elif _RESTART_SCHEME_ == 3
607 m_restart_next += (unsigned)get_restart_armin(m_stats.m_restarts + 1) * m_restart_base;
608 #elif _RESTART_SCHEME_ == 2
609 m_restart_next += get_luby(m_stats.m_restarts + 1) * m_restart_base;
610 #elif _RESTART_SCHEME_ == 1
611 if (m_stats.m_restarts & 1)
612 m_restart_next += m_restart_base;
613 else
614 m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base;
615 #else
616 m_restart_limit += m_restart_base;
617 #endif */
618 if (m_stats.m_restarts & 1)
619 m_restart_next += m_restart_base;
620 else
621 m_restart_next += (2 << (m_stats.m_restarts >> 1)) * m_restart_base;
622 return 0;
623 }
624 return 1;
625 }
626