1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #include "btorslvsls.h"
10
11 #include "btorabort.h"
12 #include "btorbv.h"
13 #include "btorclone.h"
14 #include "btorcore.h"
15 #include "btordbg.h"
16 #include "btorlog.h"
17 #include "btorlsutils.h"
18 #include "btormodel.h"
19 #include "btorprintmodel.h"
20 #include "btorproputils.h"
21 #include "btorslsutils.h"
22 #include "utils/btorhashint.h"
23 #include "utils/btorhashptr.h"
24 #include "utils/btornodeiter.h"
25 #include "utils/btornodemap.h"
26 #include "utils/btorutil.h"
27
28 #include <math.h>
29
30 /* same restart scheme as in Z3 */
31 #define BTOR_SLS_MAXSTEPS_CFACT 100 /* same as in Z3 (c4) */
32 #define BTOR_SLS_MAXSTEPS(i) \
33 (BTOR_SLS_MAXSTEPS_CFACT * ((i) &1u ? 1 : 1 << ((i) >> 1)))
34
35 #define BTOR_SLS_SELECT_CFACT 20 /* same as in Z3 (c2) */
36
37 #define BTOR_SLS_PROB_SCORE_F 50 /* = 0.05 (same as in Z3 (sp)) */
38
39 /* choose move with one candidate rather than group-wise move
40 * for random walk (prob=0.05) */
41 #define BTOR_SLS_PROB_SINGLE_VS_GW 50
42 /* randomize all candidates rather than one only (prob=0.5) */
43 #define BTOR_SLS_PROB_RAND_ALL_VS_ONE 500
44 /* start ranges from MSB rather than LSB (prob=0.5) */
45 #define BTOR_SLS_PROB_RANGE_MSB_VS_LSB 500
46 /* start segments from MSB rather than LSB (prob=0.5) */
47 #define BTOR_SLS_PROB_SEG_MSB_VS_LSB 500
48
49 /*------------------------------------------------------------------------*/
50
51 static double
compute_sls_score_formula(Btor * btor,BtorIntHashTable * score,bool * done)52 compute_sls_score_formula (Btor *btor, BtorIntHashTable *score, bool *done)
53 {
54 assert (btor);
55 assert (score);
56
57 double res, sc, weight;
58 int32_t id;
59 BtorSLSSolver *slv;
60 BtorIntHashTableIterator it;
61
62 slv = BTOR_SLS_SOLVER (btor);
63 assert (slv);
64 assert (slv->roots);
65 assert (slv->weights);
66
67 res = 0.0;
68 if (done) *done = true;
69
70 btor_iter_hashint_init (&it, slv->weights);
71 while (btor_iter_hashint_has_next (&it))
72 {
73 weight =
74 (double) ((BtorSLSConstrData *) slv->weights->data[it.cur_pos].as_ptr)
75 ->weight;
76 id = btor_iter_hashint_next (&it);
77 sc = btor_hashint_map_get (score, id)->as_dbl;
78 assert (sc >= 0.0 && sc <= 1.0);
79 if (done && sc < 1.0) *done = false;
80 res += weight * sc;
81 }
82 return res;
83 }
84
85 static BtorNode *
select_candidate_constraint(Btor * btor,uint32_t nmoves)86 select_candidate_constraint (Btor *btor, uint32_t nmoves)
87 {
88 assert (btor);
89
90 double score;
91 int32_t id;
92 BtorNode *res;
93 BtorSLSSolver *slv;
94 BtorIntHashTableIterator it;
95
96 slv = BTOR_SLS_SOLVER (btor);
97 assert (slv);
98 assert (slv->roots);
99 assert (slv->score);
100
101 res = 0;
102
103 if (btor_opt_get (btor, BTOR_OPT_SLS_USE_BANDIT))
104 {
105 double value, max_value;
106 BtorSLSConstrData *d;
107
108 max_value = 0.0;
109 btor_iter_hashint_init (&it, slv->roots);
110 while (btor_iter_hashint_has_next (&it))
111 {
112 id = btor_iter_hashint_next (&it);
113 assert (!btor_node_is_bv_const (btor_node_get_by_id (btor, id))
114 || !btor_bv_is_zero (
115 btor_model_get_bv (btor, btor_node_get_by_id (btor, id))));
116 assert (btor_hashint_map_contains (slv->weights, id));
117 d = btor_hashint_map_get (slv->weights, id)->as_ptr;
118 assert (d);
119 assert (btor_hashint_map_contains (slv->score, id));
120 score = btor_hashint_map_get (slv->score, id)->as_dbl;
121 assert (score < 1.0);
122 value = score + BTOR_SLS_SELECT_CFACT * sqrt (log (d->selected) / nmoves);
123 if (!res || value > max_value)
124 {
125 res = btor_node_get_by_id (btor, id);
126 max_value = value;
127 d->selected += 1;
128 }
129 }
130 }
131 else
132 {
133 uint32_t r;
134 BtorNode *cur;
135 BtorNodePtrStack stack;
136
137 BTOR_INIT_STACK (btor->mm, stack);
138 btor_iter_hashint_init (&it, slv->roots);
139 while (btor_iter_hashint_has_next (&it))
140 {
141 id = btor_iter_hashint_next (&it);
142 cur = btor_node_get_by_id (btor, id);
143 assert (!btor_node_is_bv_const (cur)
144 || !btor_bv_is_zero (btor_model_get_bv (btor, cur)));
145 assert (btor_hashint_map_contains (slv->score, id));
146 score = btor_hashint_map_get (slv->score, id)->as_dbl;
147 assert (score < 1.0);
148 BTOR_PUSH_STACK (stack, cur);
149 }
150 assert (BTOR_COUNT_STACK (stack));
151 r = btor_rng_pick_rand (&btor->rng, 0, BTOR_COUNT_STACK (stack) - 1);
152 res = stack.start[r];
153 BTOR_RELEASE_STACK (stack);
154 }
155
156 assert (res);
157
158 BTORLOG (1, "");
159 BTORLOG (
160 1, "*** select candidate constraint: %s", btor_util_node2string (res));
161
162 return res;
163 }
164
165 static void
select_candidates(Btor * btor,BtorNode * root,BtorNodePtrStack * candidates)166 select_candidates (Btor *btor, BtorNode *root, BtorNodePtrStack *candidates)
167 {
168 assert (btor);
169 assert (root);
170 assert (candidates);
171
172 uint32_t i;
173 BtorNode *cur, *real_cur, *e;
174 BtorNodePtrStack stack, controlling;
175 const BtorBitVector *bv;
176 BtorIntHashTable *mark;
177 BtorMemMgr *mm;
178
179 BTORLOG (1, "");
180 BTORLOG (1, "*** select candidates");
181
182 mm = btor->mm;
183 BTOR_INIT_STACK (mm, stack);
184 BTOR_INIT_STACK (mm, controlling);
185
186 BTOR_RESET_STACK (*candidates);
187 mark = btor_hashint_table_new (mm);
188
189 BTOR_PUSH_STACK (stack, root);
190 while (!BTOR_EMPTY_STACK (stack))
191 {
192 cur = BTOR_POP_STACK (stack);
193 real_cur = btor_node_real_addr (cur);
194 if (btor_hashint_table_contains (mark, real_cur->id)) continue;
195 btor_hashint_table_add (mark, real_cur->id);
196
197 if (btor_node_is_bv_var (real_cur))
198 {
199 BTOR_PUSH_STACK (*candidates, real_cur);
200 BTORLOG (1, " %s", btor_util_node2string (real_cur));
201 continue;
202 }
203
204 /* push children */
205 if (btor_opt_get (btor, BTOR_OPT_SLS_JUST) && btor_node_is_bv_and (real_cur)
206 && btor_node_bv_get_width (btor, real_cur) == 1)
207 {
208 bv = btor_model_get_bv (btor, real_cur);
209 if (!btor_bv_is_zero (bv)) /* push all */
210 goto PUSH_CHILDREN;
211 else /* push one controlling input */
212 {
213 BTOR_RESET_STACK (controlling);
214 for (i = 0; i < real_cur->arity; i++)
215 {
216 e = real_cur->e[i];
217 if (btor_bv_is_zero (btor_model_get_bv (btor, e)))
218 BTOR_PUSH_STACK (controlling, real_cur->e[i]);
219 }
220 assert (BTOR_COUNT_STACK (controlling));
221 BTOR_PUSH_STACK (
222 stack,
223 BTOR_PEEK_STACK (
224 controlling,
225 btor_rng_pick_rand (
226 &btor->rng, 0, BTOR_COUNT_STACK (controlling) - 1)));
227 }
228 }
229 else
230 {
231 PUSH_CHILDREN:
232 for (i = 0; i < real_cur->arity; i++)
233 BTOR_PUSH_STACK (stack, real_cur->e[i]);
234 }
235 }
236
237 BTOR_RELEASE_STACK (stack);
238 BTOR_RELEASE_STACK (controlling);
239 btor_hashint_table_delete (mark);
240 }
241
242 #if 0
243 static void *
244 same_node (BtorMemMgr * mm, const void * map, const void * key)
245 {
246 assert (mm);
247 assert (key);
248
249 (void) mm;
250 (void) map;
251 return (BtorNode *) key;
252 }
253 #endif
254
255 static inline void
update_assertion_weights(Btor * btor)256 update_assertion_weights (Btor *btor)
257 {
258 assert (btor);
259
260 int32_t id;
261 BtorSLSConstrData *d;
262 BtorIntHashTableIterator it;
263 BtorSLSSolver *slv;
264
265 slv = BTOR_SLS_SOLVER (btor);
266
267 if (btor_rng_pick_with_prob (&btor->rng, BTOR_SLS_PROB_SCORE_F))
268 {
269 /* decrease the weight of all satisfied assertions */
270 btor_iter_hashint_init (&it, slv->weights);
271 while (btor_iter_hashint_has_next (&it))
272 {
273 d = (BtorSLSConstrData *) slv->weights->data[it.cur_pos].as_ptr;
274 id = btor_iter_hashint_next (&it);
275 assert (btor_hashint_table_contains (slv->score, id));
276 if (btor_hashint_map_get (slv->score, id)->as_dbl == 0.0) continue;
277 if (d->weight > 1) d->weight -= 1;
278 }
279 }
280 else
281 {
282 /* increase the weight of all unsatisfied assertions */
283 btor_iter_hashint_init (&it, slv->weights);
284 while (btor_iter_hashint_has_next (&it))
285 {
286 d = (BtorSLSConstrData *) slv->weights->data[it.cur_pos].as_ptr;
287 id = btor_iter_hashint_next (&it);
288 assert (btor_hashint_table_contains (slv->score, id));
289 if (btor_hashint_map_get (slv->score, id)->as_dbl == 1.0) continue;
290 d->weight += 1;
291 }
292 }
293 }
294
295 static inline double
try_move(Btor * btor,BtorIntHashTable * bv_model,BtorIntHashTable * score,BtorIntHashTable * cans,bool * done)296 try_move (Btor *btor,
297 BtorIntHashTable *bv_model,
298 BtorIntHashTable *score,
299 BtorIntHashTable *cans,
300 bool *done)
301 {
302 assert (btor);
303 assert (bv_model);
304 assert (score);
305 assert (cans);
306 assert (cans->count);
307 assert (done);
308
309 BtorSLSSolver *slv;
310
311 slv = BTOR_SLS_SOLVER (btor);
312 assert (slv);
313 if (slv->nflips && slv->stats.flips >= slv->nflips)
314 {
315 slv->terminate = true;
316 return 0.0;
317 }
318 slv->stats.flips += 1;
319
320 #ifndef NBTORLOG
321 char *a;
322 BtorNode *can;
323 BtorBitVector *prev_ass, *new_ass;
324 BtorIntHashTableIterator iit;
325
326 BTORLOG (2, "");
327 BTORLOG (2, " * try move:");
328 btor_iter_hashint_init (&iit, cans);
329 while (btor_iter_hashint_has_next (&iit))
330 {
331 new_ass = (BtorBitVector *) cans->data[iit.cur_pos].as_ptr;
332 can = btor_node_get_by_id (btor, btor_iter_hashint_next (&iit));
333 prev_ass = (BtorBitVector *) btor_model_get_bv (btor, can);
334 BTORLOG (2,
335 " candidate: %s%s",
336 btor_node_is_regular (can) ? "" : "-",
337 btor_util_node2string (can));
338 a = btor_bv_to_char (btor->mm, prev_ass);
339 BTORLOG (2, " prev. assignment: %s", a);
340 btor_mem_freestr (btor->mm, a);
341 a = btor_bv_to_char (btor->mm, new_ass);
342 BTORLOG (2, " new assignment: %s", a);
343 btor_mem_freestr (btor->mm, a);
344 }
345 #endif
346
347 btor_lsutils_update_cone (btor,
348 bv_model,
349 slv->roots,
350 score,
351 cans,
352 false,
353 &slv->stats.updates,
354 &slv->time.update_cone,
355 &slv->time.update_cone_reset,
356 &slv->time.update_cone_model_gen,
357 &slv->time.update_cone_compute_score);
358
359 return compute_sls_score_formula (btor, score, done);
360 }
361
362 static int32_t
cmp_sls_moves_qsort(const void * move1,const void * move2)363 cmp_sls_moves_qsort (const void *move1, const void *move2)
364 {
365 BtorSLSMove *m1, *m2;
366
367 m1 = *((BtorSLSMove **) move1);
368 m2 = *((BtorSLSMove **) move2);
369 if (m1->sc > m2->sc) return 1;
370 if (m1->sc < m2->sc) return -1;
371 return 0;
372 }
373
374 #define BTOR_SLS_DELETE_CANS(cans) \
375 do \
376 { \
377 btor_iter_hashint_init (&iit, cans); \
378 while (btor_iter_hashint_has_next (&iit)) \
379 { \
380 assert (cans->data[iit.cur_pos].as_ptr); \
381 btor_bv_free (btor->mm, btor_iter_hashint_next_data (&iit)->as_ptr); \
382 } \
383 btor_hashint_map_delete (cans); \
384 } while (0)
385
386 #define BTOR_SLS_SELECT_MOVE_CHECK_SCORE(sc) \
387 do \
388 { \
389 if (done \
390 || (sls_strat != BTOR_SLS_STRAT_RAND_WALK \
391 && ((sc) > slv->max_score \
392 || (sls_strat == BTOR_SLS_STRAT_BEST_SAME_MOVE \
393 && (sc) == slv->max_score)))) \
394 { \
395 slv->max_score = (sc); \
396 slv->max_move = mk; \
397 slv->max_gw = gw; \
398 if (slv->max_cans->count) \
399 { \
400 btor_iter_hashint_init (&iit, slv->max_cans); \
401 while (btor_iter_hashint_has_next (&iit)) \
402 { \
403 assert (slv->max_cans->data[iit.cur_pos].as_ptr); \
404 btor_bv_free (btor->mm, btor_iter_hashint_next_data (&iit)->as_ptr); \
405 } \
406 } \
407 btor_hashint_map_delete (slv->max_cans); \
408 slv->max_cans = cans; \
409 if (done || sls_strat == BTOR_SLS_STRAT_FIRST_BEST_MOVE) goto DONE; \
410 } \
411 else if (sls_strat == BTOR_SLS_STRAT_RAND_WALK) \
412 { \
413 BTOR_NEW (btor->mm, m); \
414 m->cans = cans; \
415 m->sc = (sc); \
416 BTOR_PUSH_STACK (slv->moves, m); \
417 slv->sum_score += m->sc; \
418 } \
419 else \
420 { \
421 BTOR_SLS_DELETE_CANS (cans); \
422 } \
423 } while (0)
424
425 static inline bool
select_inc_dec_not_move(Btor * btor,BtorBitVector * (* fun)(BtorMemMgr *,const BtorBitVector *),BtorNodePtrStack * candidates,int32_t gw)426 select_inc_dec_not_move (Btor *btor,
427 BtorBitVector *(*fun) (BtorMemMgr *,
428 const BtorBitVector *),
429 BtorNodePtrStack *candidates,
430 int32_t gw)
431 {
432 size_t i;
433 uint32_t sls_strat;
434 bool done;
435 double sc;
436 BtorSLSMove *m;
437 BtorSLSMoveKind mk;
438 BtorBitVector *ass, *max_neigh;
439 BtorNode *can;
440 BtorIntHashTable *cans, *bv_model, *score;
441 BtorIntHashTableIterator iit;
442 BtorSLSSolver *slv;
443
444 done = false;
445 slv = BTOR_SLS_SOLVER (btor);
446 sls_strat = btor_opt_get (btor, BTOR_OPT_SLS_STRATEGY);
447
448 if (fun == btor_bv_inc)
449 mk = BTOR_SLS_MOVE_INC;
450 else if (fun == btor_bv_dec)
451 mk = BTOR_SLS_MOVE_DEC;
452 else
453 {
454 assert (fun == btor_bv_not);
455 mk = BTOR_SLS_MOVE_NOT;
456 }
457
458 bv_model = btor_model_clone_bv (btor, btor->bv_model, true);
459 score =
460 btor_hashint_map_clone (btor->mm, slv->score, btor_clone_data_as_dbl, 0);
461
462 cans = btor_hashint_map_new (btor->mm);
463
464 for (i = 0; i < BTOR_COUNT_STACK (*candidates); i++)
465 {
466 can = BTOR_PEEK_STACK (*candidates, i);
467 assert (can);
468 assert (btor_node_is_regular (can));
469
470 ass = (BtorBitVector *) btor_model_get_bv (btor, can);
471 assert (ass);
472
473 max_neigh = btor_hashint_map_contains (slv->max_cans, can->id)
474 ? btor_hashint_map_get (slv->max_cans, can->id)->as_ptr
475 : 0;
476
477 btor_hashint_map_add (cans, can->id)->as_ptr =
478 btor_opt_get (btor, BTOR_OPT_SLS_MOVE_INC_MOVE_TEST) && max_neigh
479 ? fun (btor->mm, max_neigh)
480 : fun (btor->mm, ass);
481 }
482
483 sc = try_move (btor, bv_model, score, cans, &done);
484 if (slv->terminate)
485 {
486 BTOR_SLS_DELETE_CANS (cans);
487 goto DONE;
488 }
489 BTOR_SLS_SELECT_MOVE_CHECK_SCORE (sc);
490
491 DONE:
492 btor_model_delete_bv (btor, &bv_model);
493 btor_hashint_map_delete (score);
494 return done;
495 }
496
497 static inline bool
select_flip_move(Btor * btor,BtorNodePtrStack * candidates,int32_t gw)498 select_flip_move (Btor *btor, BtorNodePtrStack *candidates, int32_t gw)
499 {
500 size_t i, n_endpos;
501 uint32_t pos, cpos, sls_strat;
502 bool done = false;
503 double sc;
504 BtorSLSMove *m;
505 BtorSLSMoveKind mk;
506 BtorBitVector *ass, *max_neigh;
507 BtorNode *can;
508 BtorIntHashTable *cans, *bv_model, *score;
509 BtorIntHashTableIterator iit;
510 BtorSLSSolver *slv;
511
512 slv = BTOR_SLS_SOLVER (btor);
513 sls_strat = btor_opt_get (btor, BTOR_OPT_SLS_STRATEGY);
514
515 mk = BTOR_SLS_MOVE_FLIP;
516
517 bv_model = btor_model_clone_bv (btor, btor->bv_model, true);
518 score =
519 btor_hashint_map_clone (btor->mm, slv->score, btor_clone_data_as_dbl, 0);
520
521 for (pos = 0, n_endpos = 0; n_endpos < BTOR_COUNT_STACK (*candidates); pos++)
522 {
523 cans = btor_hashint_map_new (btor->mm);
524
525 for (i = 0; i < BTOR_COUNT_STACK (*candidates); i++)
526 {
527 can = BTOR_PEEK_STACK (*candidates, i);
528 assert (btor_node_is_regular (can));
529 assert (can);
530
531 ass = (BtorBitVector *) btor_model_get_bv (btor, can);
532 assert (ass);
533
534 max_neigh = btor_hashint_map_contains (slv->max_cans, can->id)
535 ? btor_hashint_map_get (slv->max_cans, can->id)->as_ptr
536 : 0;
537
538 if (pos == btor_bv_get_width (ass) - 1) n_endpos += 1;
539 cpos = pos % btor_bv_get_width (ass);
540
541 btor_hashint_map_add (cans, can->id)->as_ptr =
542 btor_opt_get (btor, BTOR_OPT_SLS_MOVE_INC_MOVE_TEST) && max_neigh
543 ? btor_bv_flipped_bit (btor->mm, max_neigh, cpos)
544 : btor_bv_flipped_bit (btor->mm, ass, cpos);
545 }
546
547 sc = try_move (btor, bv_model, score, cans, &done);
548 if (slv->terminate)
549 {
550 BTOR_SLS_DELETE_CANS (cans);
551 goto DONE;
552 }
553 BTOR_SLS_SELECT_MOVE_CHECK_SCORE (sc);
554 }
555
556 DONE:
557 btor_model_delete_bv (btor, &bv_model);
558 btor_hashint_map_delete (score);
559 return done;
560 }
561
562 static inline bool
select_flip_range_move(Btor * btor,BtorNodePtrStack * candidates,int32_t gw)563 select_flip_range_move (Btor *btor, BtorNodePtrStack *candidates, int32_t gw)
564 {
565 size_t i, n_endpos;
566 uint32_t up, cup, clo, sls_strat, bw;
567 bool done = false;
568 double sc;
569 BtorSLSMove *m;
570 BtorSLSMoveKind mk;
571 BtorBitVector *ass, *max_neigh;
572 BtorNode *can;
573 BtorIntHashTable *cans, *bv_model, *score;
574 BtorIntHashTableIterator iit;
575 BtorSLSSolver *slv;
576
577 slv = BTOR_SLS_SOLVER (btor);
578 sls_strat = btor_opt_get (btor, BTOR_OPT_SLS_STRATEGY);
579
580 mk = BTOR_SLS_MOVE_FLIP_RANGE;
581
582 bv_model = btor_model_clone_bv (btor, btor->bv_model, true);
583 score =
584 btor_hashint_map_clone (btor->mm, slv->score, btor_clone_data_as_dbl, 0);
585
586 for (up = 1, n_endpos = 0; n_endpos < BTOR_COUNT_STACK (*candidates);
587 up = 2 * up + 1)
588 {
589 cans = btor_hashint_map_new (btor->mm);
590
591 for (i = 0; i < BTOR_COUNT_STACK (*candidates); i++)
592 {
593 can = BTOR_PEEK_STACK (*candidates, i);
594 assert (can);
595 assert (btor_node_is_regular (can));
596
597 ass = (BtorBitVector *) btor_model_get_bv (btor, can);
598 assert (ass);
599
600 max_neigh = btor_hashint_map_contains (slv->max_cans, can->id)
601 ? btor_hashint_map_get (slv->max_cans, can->id)->as_ptr
602 : 0;
603
604 clo = 0;
605 cup = up;
606 bw = btor_bv_get_width (ass);
607
608 if (up >= bw)
609 {
610 if ((up - 1) / 2 < bw) n_endpos += 1;
611 cup = bw - 1;
612 }
613
614 /* range from MSB rather than LSB with given prob */
615 if (btor_rng_pick_with_prob (&btor->rng, BTOR_SLS_PROB_RANGE_MSB_VS_LSB))
616 {
617 clo = bw - 1 - cup;
618 cup = bw - 1;
619 }
620
621 btor_hashint_map_add (cans, can->id)->as_ptr =
622 btor_opt_get (btor, BTOR_OPT_SLS_MOVE_INC_MOVE_TEST) && max_neigh
623 ? btor_bv_flipped_bit_range (btor->mm, max_neigh, cup, clo)
624 : btor_bv_flipped_bit_range (btor->mm, ass, cup, clo);
625 }
626
627 sc = try_move (btor, bv_model, score, cans, &done);
628 if (slv->terminate)
629 {
630 BTOR_SLS_DELETE_CANS (cans);
631 goto DONE;
632 }
633 BTOR_SLS_SELECT_MOVE_CHECK_SCORE (sc);
634 }
635
636 DONE:
637 btor_model_delete_bv (btor, &bv_model);
638 btor_hashint_map_delete (score);
639 return done;
640 }
641
642 static inline bool
select_flip_segment_move(Btor * btor,BtorNodePtrStack * candidates,int32_t gw)643 select_flip_segment_move (Btor *btor, BtorNodePtrStack *candidates, int32_t gw)
644 {
645 size_t i, n_endpos;
646 int32_t ctmp;
647 uint32_t lo, clo, up, cup, seg, sls_strat, bw;
648 bool done = false;
649 double sc;
650 BtorSLSMove *m;
651 BtorSLSMoveKind mk;
652 BtorBitVector *ass, *max_neigh;
653 BtorNode *can;
654 BtorIntHashTable *cans, *bv_model, *score;
655 BtorIntHashTableIterator iit;
656 BtorSLSSolver *slv;
657
658 slv = BTOR_SLS_SOLVER (btor);
659 sls_strat = btor_opt_get (btor, BTOR_OPT_SLS_STRATEGY);
660
661 mk = BTOR_SLS_MOVE_FLIP_SEGMENT;
662
663 bv_model = btor_model_clone_bv (btor, btor->bv_model, true);
664 score =
665 btor_hashint_map_clone (btor->mm, slv->score, btor_clone_data_as_dbl, 0);
666
667 for (seg = 2; seg <= 8; seg <<= 1)
668 {
669 for (lo = 0, up = seg - 1, n_endpos = 0;
670 n_endpos < BTOR_COUNT_STACK (*candidates);
671 lo += seg, up += seg)
672 {
673 cans = btor_hashint_map_new (btor->mm);
674
675 for (i = 0; i < BTOR_COUNT_STACK (*candidates); i++)
676 {
677 can = BTOR_PEEK_STACK (*candidates, i);
678 assert (can);
679 assert (btor_node_is_regular (can));
680
681 ass = (BtorBitVector *) btor_model_get_bv (btor, can);
682 assert (ass);
683
684 max_neigh = btor_hashint_map_contains (slv->max_cans, can->id)
685 ? btor_hashint_map_get (slv->max_cans, can->id)->as_ptr
686 : 0;
687
688 clo = lo;
689 cup = up;
690 bw = btor_bv_get_width (ass);
691
692 if (up >= bw)
693 {
694 if (up - seg < bw) n_endpos += 1;
695 cup = bw - 1;
696 }
697
698 if (lo >= bw - 1) clo = bw < seg ? 0 : bw - seg;
699
700 /* range from MSB rather than LSB with given prob */
701 if (btor_rng_pick_with_prob (&btor->rng, BTOR_SLS_PROB_SEG_MSB_VS_LSB))
702 {
703 ctmp = clo;
704 clo = bw - 1 - cup;
705 cup = bw - 1 - ctmp;
706 }
707
708 btor_hashint_map_add (cans, can->id)->as_ptr =
709 btor_opt_get (btor, BTOR_OPT_SLS_MOVE_INC_MOVE_TEST) && max_neigh
710 ? btor_bv_flipped_bit_range (btor->mm, max_neigh, cup, clo)
711 : btor_bv_flipped_bit_range (btor->mm, ass, cup, clo);
712 }
713
714 sc = try_move (btor, bv_model, score, cans, &done);
715 if (slv->terminate)
716 {
717 BTOR_SLS_DELETE_CANS (cans);
718 goto DONE;
719 }
720 BTOR_SLS_SELECT_MOVE_CHECK_SCORE (sc);
721 }
722 }
723
724 DONE:
725 btor_model_delete_bv (btor, &bv_model);
726 btor_hashint_map_delete (score);
727 return done;
728 }
729
730 static inline bool
select_rand_range_move(Btor * btor,BtorNodePtrStack * candidates,int32_t gw)731 select_rand_range_move (Btor *btor, BtorNodePtrStack *candidates, int32_t gw)
732 {
733 double sc, rand_max_score = -1.0;
734 size_t i, n_endpos;
735 uint32_t up, cup, clo, sls_strat, bw;
736 bool done;
737 BtorSLSMove *m;
738 BtorSLSMoveKind mk;
739 BtorBitVector *ass;
740 BtorNode *can;
741 BtorIntHashTable *cans, *bv_model, *score;
742 BtorIntHashTableIterator iit;
743 BtorSLSSolver *slv;
744
745 done = false;
746 slv = BTOR_SLS_SOLVER (btor);
747 sls_strat = btor_opt_get (btor, BTOR_OPT_SLS_STRATEGY);
748
749 mk = BTOR_SLS_MOVE_RAND;
750
751 bv_model = btor_model_clone_bv (btor, btor->bv_model, true);
752 score =
753 btor_hashint_map_clone (btor->mm, slv->score, btor_clone_data_as_dbl, 0);
754
755 for (up = 1, n_endpos = 0; n_endpos < BTOR_COUNT_STACK (*candidates);
756 up = 2 * up + 1)
757 {
758 cans = btor_hashint_map_new (btor->mm);
759
760 for (i = 0; i < BTOR_COUNT_STACK (*candidates); i++)
761 {
762 can = BTOR_PEEK_STACK (*candidates, i);
763 assert (can);
764 assert (btor_node_is_regular (can));
765
766 ass = (BtorBitVector *) btor_model_get_bv (btor, can);
767 assert (ass);
768
769 clo = 0;
770 cup = up;
771 bw = btor_bv_get_width (ass);
772 if (up >= bw)
773 {
774 if ((up - 1) / 2 < bw) n_endpos += 1;
775 cup = bw - 1;
776 }
777
778 /* range from MSB rather than LSB with given prob */
779 if (btor_rng_pick_with_prob (&btor->rng, BTOR_SLS_PROB_RANGE_MSB_VS_LSB))
780 {
781 clo = bw - 1 - cup;
782 cup = bw - 1;
783 }
784 btor_hashint_map_add (cans, can->id)->as_ptr =
785 btor_bv_new_random_bit_range (btor->mm, &btor->rng, bw, cup, clo);
786 }
787
788 sc = try_move (btor, bv_model, score, cans, &done);
789 if (slv->terminate)
790 {
791 BTOR_SLS_DELETE_CANS (cans);
792 goto DONE;
793 }
794 if (rand_max_score == -1.0 || sc > rand_max_score)
795 {
796 /* reset, use current */
797 slv->max_score = -1.0;
798 rand_max_score = sc;
799 }
800 BTOR_SLS_SELECT_MOVE_CHECK_SCORE (sc);
801 }
802
803 DONE:
804 btor_model_delete_bv (btor, &bv_model);
805 btor_hashint_map_delete (score);
806 return done;
807 }
808
809 static inline bool
select_move_aux(Btor * btor,BtorNodePtrStack * candidates,int32_t gw)810 select_move_aux (Btor *btor, BtorNodePtrStack *candidates, int32_t gw)
811 {
812 assert (btor);
813 assert (candidates);
814 assert (gw >= 0);
815
816 BtorSLSMoveKind mk;
817 BtorSLSSolver *slv;
818 bool done = false;
819
820 slv = BTOR_SLS_SOLVER (btor);
821
822 for (mk = 0; mk < BTOR_SLS_MOVE_DONE; mk++)
823 {
824 if (slv->nflips && slv->stats.flips >= slv->nflips)
825 {
826 slv->terminate = true;
827 break;
828 }
829
830 switch (mk)
831 {
832 case BTOR_SLS_MOVE_INC:
833 if ((done =
834 select_inc_dec_not_move (btor, btor_bv_inc, candidates, gw)))
835 return done;
836 break;
837
838 case BTOR_SLS_MOVE_DEC:
839 if ((done =
840 select_inc_dec_not_move (btor, btor_bv_dec, candidates, gw)))
841 return done;
842 break;
843
844 case BTOR_SLS_MOVE_NOT:
845 if ((done =
846 select_inc_dec_not_move (btor, btor_bv_not, candidates, gw)))
847 return done;
848 break;
849
850 case BTOR_SLS_MOVE_FLIP_RANGE:
851 if (!btor_opt_get (btor, BTOR_OPT_SLS_MOVE_RANGE)) continue;
852 if ((done = select_flip_range_move (btor, candidates, gw))) return done;
853 break;
854
855 case BTOR_SLS_MOVE_FLIP_SEGMENT:
856 if (!btor_opt_get (btor, BTOR_OPT_SLS_MOVE_SEGMENT)) continue;
857 if ((done = select_flip_segment_move (btor, candidates, gw)))
858 return done;
859 break;
860
861 default:
862 assert (mk == BTOR_SLS_MOVE_FLIP);
863 if ((done = select_flip_move (btor, candidates, gw))) return done;
864 }
865 }
866
867 return done;
868 }
869
870 static inline void
select_move(Btor * btor,BtorNodePtrStack * candidates)871 select_move (Btor *btor, BtorNodePtrStack *candidates)
872 {
873 assert (btor);
874 assert (candidates);
875
876 size_t i, r;
877 bool randomizeall;
878 bool done;
879 double rd, sum;
880 BtorNode *can;
881 BtorBitVector *neigh;
882 BtorNodePtrStack cans;
883 BtorSLSMove *m;
884 BtorIntHashTableIterator iit;
885 BtorSLSSolver *slv;
886
887 slv = BTOR_SLS_SOLVER (btor);
888 assert (slv->max_cans);
889 assert (!slv->max_cans->count);
890
891 BTOR_INIT_STACK (btor->mm, cans);
892 /* one after another */
893 for (i = 0; i < BTOR_COUNT_STACK (*candidates); i++)
894 {
895 can = BTOR_PEEK_STACK (*candidates, i);
896 assert (can);
897 BTOR_PUSH_STACK (cans, can);
898
899 if ((done = select_move_aux (btor, &cans, 0))) goto DONE;
900 if (slv->terminate) goto DONE;
901
902 BTOR_RESET_STACK (cans);
903 }
904
905 /* groupwise */
906 if (btor_opt_get (btor, BTOR_OPT_SLS_MOVE_GW)
907 && BTOR_COUNT_STACK (*candidates) > 1)
908 {
909 if ((done = select_move_aux (btor, candidates, 1))) goto DONE;
910 if (slv->terminate) goto DONE;
911 }
912
913 /* select probabilistic random walk move
914 * (weighted by score; the higher the score, the higher the probability
915 * that a move gets chosen) */
916 if (btor_opt_get (btor, BTOR_OPT_SLS_STRATEGY) == BTOR_SLS_STRAT_RAND_WALK)
917 {
918 assert (slv->max_cans->count == 0);
919 assert (BTOR_COUNT_STACK (slv->moves));
920
921 qsort (slv->moves.start,
922 BTOR_COUNT_STACK (slv->moves),
923 sizeof (BtorSLSMove *),
924 cmp_sls_moves_qsort);
925
926 rd = btor_rng_pick_rand_dbl (&btor->rng, 0, slv->sum_score);
927 m = BTOR_PEEK_STACK (slv->moves, 0);
928 for (i = 0, sum = 0; i < BTOR_COUNT_STACK (slv->moves); i++)
929 {
930 sum += m->sc;
931 if (sum > rd) break;
932 m = BTOR_PEEK_STACK (slv->moves, i);
933 }
934
935 slv->max_gw = m->cans->count > 1;
936 slv->max_move = BTOR_SLS_MOVE_RAND_WALK;
937 btor_iter_hashint_init (&iit, m->cans);
938 while (btor_iter_hashint_has_next (&iit))
939 {
940 neigh = btor_bv_copy (btor->mm, m->cans->data[iit.cur_pos].as_ptr);
941 can = btor_node_get_by_id (btor, btor_iter_hashint_next (&iit));
942 assert (btor_node_is_regular (can));
943 assert (neigh);
944 btor_hashint_map_add (slv->max_cans, can->id)->as_ptr = neigh;
945 }
946 }
947
948 if (slv->max_cans->count == 0)
949 {
950 assert (slv->max_move == BTOR_SLS_MOVE_DONE);
951
952 /* randomize if no best move was found */
953 randomizeall = btor_opt_get (btor, BTOR_OPT_SLS_MOVE_RAND_ALL)
954 ? btor_rng_pick_with_prob (&btor->rng,
955 BTOR_SLS_PROB_RAND_ALL_VS_ONE)
956 : false;
957
958 if (randomizeall)
959 {
960 slv->max_gw = 1;
961 slv->max_move = BTOR_SLS_MOVE_RAND;
962
963 for (r = 0; r <= BTOR_COUNT_STACK (*candidates) - 1; r++)
964 {
965 can = BTOR_PEEK_STACK (*candidates, r);
966 assert (btor_node_is_regular (can));
967 if (btor_node_bv_get_width (btor, can) == 1)
968 neigh = btor_bv_flipped_bit (
969 btor->mm, (BtorBitVector *) btor_model_get_bv (btor, can), 0);
970 else
971 neigh = btor_bv_new_random (
972 btor->mm, &btor->rng, btor_node_bv_get_width (btor, can));
973
974 btor_hashint_map_add (slv->max_cans, can->id)->as_ptr = neigh;
975 }
976 }
977 else
978 {
979 slv->max_gw = 0;
980 slv->max_move = BTOR_SLS_MOVE_RAND;
981
982 can = BTOR_PEEK_STACK (
983 *candidates,
984 btor_rng_pick_rand (
985 &btor->rng, 0, BTOR_COUNT_STACK (*candidates) - 1));
986 assert (btor_node_is_regular (can));
987
988 if (btor_node_bv_get_width (btor, can) == 1)
989 {
990 neigh = btor_bv_flipped_bit (
991 btor->mm, (BtorBitVector *) btor_model_get_bv (btor, can), 0);
992 btor_hashint_map_add (slv->max_cans, can->id)->as_ptr = neigh;
993 }
994 /* pick neighbor with randomized bit range (best guess) */
995 else if (btor_opt_get (btor, BTOR_OPT_SLS_MOVE_RAND_RANGE))
996 {
997 assert (!BTOR_COUNT_STACK (cans));
998 BTOR_PUSH_STACK (cans, can);
999 select_rand_range_move (btor, &cans, 0);
1000 BTOR_RESET_STACK (cans);
1001 assert (slv->max_cans->count == 1);
1002 }
1003 else
1004 {
1005 neigh = btor_bv_new_random (
1006 btor->mm, &btor->rng, btor_node_bv_get_width (btor, can));
1007 btor_hashint_map_add (slv->max_cans, can->id)->as_ptr = neigh;
1008 }
1009
1010 assert (!slv->max_gw);
1011 assert (slv->max_move == BTOR_SLS_MOVE_RAND);
1012 }
1013 assert (slv->max_cans->count);
1014 }
1015
1016 DONE:
1017 BTOR_RELEASE_STACK (cans);
1018 while (!BTOR_EMPTY_STACK (slv->moves))
1019 {
1020 m = BTOR_POP_STACK (slv->moves);
1021 btor_iter_hashint_init (&iit, m->cans);
1022 while (btor_iter_hashint_has_next (&iit))
1023 btor_bv_free (btor->mm, btor_iter_hashint_next_data (&iit)->as_ptr);
1024 btor_hashint_map_delete (m->cans);
1025 BTOR_DELETE (btor->mm, m);
1026 }
1027 }
1028
1029 static inline void
select_random_move(Btor * btor,BtorNodePtrStack * candidates)1030 select_random_move (Btor *btor, BtorNodePtrStack *candidates)
1031 {
1032 assert (btor);
1033 assert (candidates);
1034
1035 uint32_t i, r, up, lo, bw;
1036 BtorSLSMoveKind mk;
1037 BtorNodePtrStack cans, *pcans;
1038 BtorNode *can;
1039 BtorBitVector *ass, *neigh;
1040 BtorSLSSolver *slv;
1041
1042 slv = BTOR_SLS_SOLVER (btor);
1043 assert (slv->max_cans);
1044 assert (!slv->max_cans->count);
1045
1046 BTOR_INIT_STACK (btor->mm, cans);
1047
1048 slv->max_move = BTOR_SLS_MOVE_RAND_WALK;
1049
1050 /* select candidate(s) */
1051 if (btor_opt_get (btor, BTOR_OPT_SLS_MOVE_GW)
1052 && btor_rng_pick_with_prob (&btor->rng, BTOR_SLS_PROB_SINGLE_VS_GW))
1053 {
1054 pcans = candidates;
1055 slv->max_gw = 1;
1056 }
1057 else
1058 {
1059 BTOR_PUSH_STACK (
1060 cans,
1061 BTOR_PEEK_STACK (
1062 *candidates,
1063 btor_rng_pick_rand (
1064 &btor->rng, 0, BTOR_COUNT_STACK (*candidates) - 1)));
1065 pcans = &cans;
1066 slv->max_gw = 0;
1067 }
1068
1069 /* select neighbor(s) */
1070 for (i = 0; i < BTOR_COUNT_STACK (*pcans); i++)
1071 {
1072 can = BTOR_PEEK_STACK ((*pcans), i);
1073 assert (btor_node_is_regular (can));
1074 ass = (BtorBitVector *) btor_model_get_bv (btor, can);
1075 assert (ass);
1076
1077 bw = btor_bv_get_width (ass);
1078 r = btor_rng_pick_rand (&btor->rng, 0, BTOR_SLS_MOVE_DONE - 1 + bw - 1);
1079
1080 if (r < bw)
1081 mk = BTOR_SLS_MOVE_FLIP;
1082 else
1083 mk = (BtorSLSMoveKind) r - bw + 1;
1084 assert (mk >= 0);
1085
1086 if ((!btor_opt_get (btor, BTOR_OPT_SLS_MOVE_SEGMENT)
1087 && mk == BTOR_SLS_MOVE_FLIP_SEGMENT)
1088 || (!btor_opt_get (btor, BTOR_OPT_SLS_MOVE_RANGE)
1089 && mk == BTOR_SLS_MOVE_FLIP_RANGE))
1090 {
1091 mk = BTOR_SLS_MOVE_FLIP;
1092 }
1093
1094 switch (mk)
1095 {
1096 case BTOR_SLS_MOVE_INC: neigh = btor_bv_inc (btor->mm, ass); break;
1097 case BTOR_SLS_MOVE_DEC: neigh = btor_bv_dec (btor->mm, ass); break;
1098 case BTOR_SLS_MOVE_NOT: neigh = btor_bv_not (btor->mm, ass); break;
1099 case BTOR_SLS_MOVE_FLIP_RANGE:
1100 up = btor_rng_pick_rand (&btor->rng, bw > 1 ? 1 : 0, bw - 1);
1101 neigh = btor_bv_flipped_bit_range (btor->mm, ass, up, 0);
1102 break;
1103 case BTOR_SLS_MOVE_FLIP_SEGMENT:
1104 lo = btor_rng_pick_rand (&btor->rng, 0, bw - 1);
1105 up = btor_rng_pick_rand (&btor->rng, lo < bw - 1 ? lo + 1 : lo, bw - 1);
1106 neigh = btor_bv_flipped_bit_range (btor->mm, ass, up, lo);
1107 break;
1108 default:
1109 assert (mk == BTOR_SLS_MOVE_FLIP);
1110 neigh = btor_bv_flipped_bit (
1111 btor->mm, ass, btor_rng_pick_rand (&btor->rng, 0, bw - 1));
1112 break;
1113 }
1114
1115 btor_hashint_map_add (slv->max_cans, can->id)->as_ptr = neigh;
1116 }
1117
1118 BTOR_RELEASE_STACK (cans);
1119 }
1120
1121 /*------------------------------------------------------------------------*/
1122
1123 static bool
move(Btor * btor,uint32_t nmoves)1124 move (Btor *btor, uint32_t nmoves)
1125 {
1126 assert (btor);
1127
1128 uint32_t nprops, nsls;
1129 bool res;
1130 BtorNode *constr, *can;
1131 BtorNodePtrStack candidates;
1132 BtorIntHashTableIterator iit;
1133 BtorSLSSolver *slv;
1134 BtorBitVector *neigh;
1135
1136 BTORLOG (1, "");
1137 BTORLOG (1, "*** move");
1138
1139 BTOR_INIT_STACK (btor->mm, candidates);
1140
1141 slv = BTOR_SLS_SOLVER (btor);
1142 assert (!slv->max_cans);
1143 assert (slv->roots->count);
1144
1145 constr = select_candidate_constraint (btor, nmoves);
1146
1147 slv->max_cans = btor_hashint_map_new (btor->mm);
1148
1149 res = true;
1150
1151 nprops = btor_opt_get (btor, BTOR_OPT_SLS_MOVE_PROP_N_PROP);
1152 nsls = btor_opt_get (btor, BTOR_OPT_SLS_MOVE_PROP_N_SLS);
1153
1154 /* Always perform propagation moves first, i.e. perform moves
1155 * with ratio nprops:nsls of propagation to sls moves */
1156 if (btor_opt_get (btor, BTOR_OPT_SLS_STRATEGY) == BTOR_SLS_STRAT_ALWAYS_PROP
1157 || (btor_opt_get (btor, BTOR_OPT_SLS_MOVE_PROP)
1158 && slv->npropmoves < nprops))
1159 {
1160 slv->npropmoves += 1;
1161 /* Select neighbor by propagating assignments from a given candidate
1162 * constraint (which is forced to be true) downwards. A downward path
1163 * is chosen via justification. If a non-recoverable conflict is
1164 * encountered, no move is performed. */
1165 slv->max_move = BTOR_SLS_MOVE_PROP;
1166 slv->stats.props +=
1167 btor_proputils_select_move_prop (btor, constr, &can, &neigh);
1168 if (can)
1169 {
1170 assert (neigh);
1171 btor_hashint_map_add (slv->max_cans, btor_node_real_addr (can)->id)
1172 ->as_ptr = neigh;
1173 }
1174 else /* recovery move */
1175 {
1176 slv->stats.move_prop_non_rec_conf += 1;
1177 /* force random walk if prop move fails */
1178 if (btor_opt_get (btor, BTOR_OPT_SLS_MOVE_PROP_FORCE_RW))
1179 {
1180 select_candidates (btor, constr, &candidates);
1181 /* root is const false -> unsat */
1182 if (!BTOR_COUNT_STACK (candidates))
1183 {
1184 res = false;
1185 goto DONE;
1186 }
1187
1188 goto SLS_MOVE_RAND_WALK;
1189 }
1190
1191 goto SLS_MOVE;
1192 }
1193 }
1194 else
1195 {
1196 slv->nslsmoves += 1;
1197 SLS_MOVE:
1198 select_candidates (btor, constr, &candidates);
1199 /* root is const false -> unsat */
1200 if (!BTOR_COUNT_STACK (candidates))
1201 {
1202 res = false;
1203 goto DONE;
1204 }
1205
1206 slv->max_score = compute_sls_score_formula (btor, slv->score, 0);
1207 slv->max_move = BTOR_SLS_MOVE_DONE;
1208 slv->max_gw = -1;
1209
1210 if (btor_opt_get (btor, BTOR_OPT_SLS_MOVE_RAND_WALK)
1211 && btor_rng_pick_with_prob (
1212 &btor->rng,
1213 btor_opt_get (btor, BTOR_OPT_SLS_PROB_MOVE_RAND_WALK)))
1214 {
1215 SLS_MOVE_RAND_WALK:
1216 select_random_move (btor, &candidates);
1217 }
1218 else
1219 {
1220 select_move (btor, &candidates);
1221 if (slv->terminate) goto DONE;
1222 }
1223
1224 assert (slv->max_cans->count);
1225 }
1226 assert (slv->max_move != BTOR_SLS_MOVE_DONE);
1227
1228 if (nprops == slv->npropmoves && nsls == slv->nslsmoves)
1229 {
1230 slv->npropmoves = slv->nslsmoves = 0;
1231 }
1232
1233 #ifndef NBTORLOG
1234 BTORLOG (1, "");
1235 BTORLOG (1, " * move");
1236 char *a;
1237 BtorBitVector *ass;
1238 btor_iter_hashint_init (&iit, slv->max_cans);
1239 while (btor_iter_hashint_has_next (&iit))
1240 {
1241 neigh = (BtorBitVector *) slv->max_cans->data[iit.cur_pos].as_ptr;
1242 can = btor_node_get_by_id (btor, btor_iter_hashint_next (&iit));
1243 ass = (BtorBitVector *) btor_model_get_bv (btor, can);
1244 a = btor_bv_to_char (btor->mm, ass);
1245 BTORLOG (1,
1246 " candidate: %s%s",
1247 btor_node_is_regular (can) ? "" : "-",
1248 btor_util_node2string (can));
1249 BTORLOG (1, " prev. assignment: %s", a);
1250 btor_mem_freestr (btor->mm, a);
1251 a = btor_bv_to_char (btor->mm, neigh);
1252 BTORLOG (1, " new assignment: %s", a);
1253 btor_mem_freestr (btor->mm, a);
1254 }
1255 #endif
1256
1257 btor_lsutils_update_cone (btor,
1258 btor->bv_model,
1259 slv->roots,
1260 slv->score,
1261 slv->max_cans,
1262 true,
1263 &slv->stats.updates,
1264 &slv->time.update_cone,
1265 &slv->time.update_cone_reset,
1266 &slv->time.update_cone_model_gen,
1267 &slv->time.update_cone_compute_score);
1268
1269 slv->stats.moves += 1;
1270
1271 assert (slv->max_move != BTOR_SLS_MOVE_DONE);
1272 assert (slv->max_gw >= 0);
1273
1274 switch (slv->max_move)
1275 {
1276 case BTOR_SLS_MOVE_FLIP:
1277 if (!slv->max_gw)
1278 slv->stats.move_flip += 1;
1279 else
1280 slv->stats.move_gw_flip += 1;
1281 break;
1282 case BTOR_SLS_MOVE_INC:
1283 if (!slv->max_gw)
1284 slv->stats.move_inc += 1;
1285 else
1286 slv->stats.move_gw_inc += 1;
1287 break;
1288 case BTOR_SLS_MOVE_DEC:
1289 if (!slv->max_gw)
1290 slv->stats.move_dec += 1;
1291 else
1292 slv->stats.move_gw_dec += 1;
1293 break;
1294 case BTOR_SLS_MOVE_NOT:
1295 if (!slv->max_gw)
1296 slv->stats.move_not += 1;
1297 else
1298 slv->stats.move_gw_not += 1;
1299 break;
1300 case BTOR_SLS_MOVE_FLIP_RANGE:
1301 if (!slv->max_gw)
1302 slv->stats.move_range += 1;
1303 else
1304 slv->stats.move_gw_range += 1;
1305 break;
1306 case BTOR_SLS_MOVE_FLIP_SEGMENT:
1307 if (!slv->max_gw)
1308 slv->stats.move_seg += 1;
1309 else
1310 slv->stats.move_gw_seg += 1;
1311 break;
1312 case BTOR_SLS_MOVE_RAND:
1313 if (!slv->max_gw)
1314 slv->stats.move_rand += 1;
1315 else
1316 slv->stats.move_gw_rand += 1;
1317 break;
1318 case BTOR_SLS_MOVE_RAND_WALK:
1319 if (!slv->max_gw)
1320 slv->stats.move_rand_walk += 1;
1321 else
1322 slv->stats.move_gw_rand_walk += 1;
1323 break;
1324 default:
1325 assert (slv->max_move == BTOR_SLS_MOVE_PROP);
1326 slv->stats.move_prop += 1;
1327 }
1328
1329 if (slv->max_move == BTOR_SLS_MOVE_RAND) update_assertion_weights (btor);
1330
1331 /** cleanup **/
1332 DONE:
1333 btor_iter_hashint_init (&iit, slv->max_cans);
1334 while (btor_iter_hashint_has_next (&iit))
1335 {
1336 assert (slv->max_cans->data[iit.cur_pos].as_ptr);
1337 btor_bv_free (btor->mm, btor_iter_hashint_next_data (&iit)->as_ptr);
1338 }
1339 btor_hashint_map_delete (slv->max_cans);
1340 slv->max_cans = 0;
1341 BTOR_RELEASE_STACK (candidates);
1342 return res;
1343 }
1344
1345 /*------------------------------------------------------------------------*/
1346
1347 static BtorSLSSolver *
clone_sls_solver(Btor * clone,BtorSLSSolver * slv,BtorNodeMap * exp_map)1348 clone_sls_solver (Btor *clone, BtorSLSSolver *slv, BtorNodeMap *exp_map)
1349 {
1350 assert (clone);
1351 assert (slv);
1352 assert (slv->kind == BTOR_SLS_SOLVER_KIND);
1353
1354 uint32_t i;
1355 BtorSLSSolver *res;
1356 BtorSLSMove *m, *cm;
1357
1358 (void) exp_map;
1359
1360 BTOR_NEW (clone->mm, res);
1361 memcpy (res, slv, sizeof (BtorSLSSolver));
1362
1363 res->btor = clone;
1364 res->roots = btor_hashint_map_clone (clone->mm, slv->roots, 0, 0);
1365 res->score =
1366 btor_hashint_map_clone (clone->mm, slv->score, btor_clone_data_as_dbl, 0);
1367
1368 BTOR_INIT_STACK (clone->mm, res->moves);
1369 assert (BTOR_SIZE_STACK (slv->moves) || !BTOR_COUNT_STACK (slv->moves));
1370 if (BTOR_SIZE_STACK (slv->moves))
1371 {
1372 BTOR_NEWN (clone->mm, res->moves.start, BTOR_SIZE_STACK (slv->moves));
1373 res->moves.top = res->moves.start;
1374 res->moves.end = res->moves.start + BTOR_SIZE_STACK (slv->moves);
1375
1376 for (i = 0; i < BTOR_COUNT_STACK (slv->moves); i++)
1377 {
1378 m = BTOR_PEEK_STACK (slv->moves, i);
1379 assert (m);
1380 BTOR_NEW (clone->mm, cm);
1381 cm->cans = btor_hashint_map_clone (
1382 clone->mm, m->cans, btor_clone_data_as_bv_ptr, 0);
1383 cm->sc = m->sc;
1384 BTOR_PUSH_STACK (res->moves, m);
1385 }
1386 }
1387 assert (BTOR_COUNT_STACK (slv->moves) == BTOR_COUNT_STACK (res->moves));
1388 assert (BTOR_SIZE_STACK (slv->moves) == BTOR_SIZE_STACK (res->moves));
1389
1390 res->max_cans = btor_hashint_map_clone (
1391 clone->mm, slv->max_cans, btor_clone_data_as_bv_ptr, 0);
1392
1393 return res;
1394 }
1395
1396 static void
delete_sls_solver(BtorSLSSolver * slv)1397 delete_sls_solver (BtorSLSSolver *slv)
1398 {
1399 assert (slv);
1400 assert (slv->kind == BTOR_SLS_SOLVER_KIND);
1401 assert (slv->btor);
1402 assert (slv->btor->slv == (BtorSolver *) slv);
1403
1404 Btor *btor;
1405 BtorIntHashTableIterator it;
1406 BtorSLSConstrData *d;
1407 BtorSLSMove *m;
1408
1409 btor = slv->btor;
1410
1411 if (slv->score) btor_hashint_map_delete (slv->score);
1412 if (slv->roots) btor_hashint_map_delete (slv->roots);
1413 if (slv->weights)
1414 {
1415 btor_iter_hashint_init (&it, slv->weights);
1416 while (btor_iter_hashint_has_next (&it))
1417 {
1418 d = btor_iter_hashint_next_data (&it)->as_ptr;
1419 BTOR_DELETE (btor->mm, d);
1420 }
1421 btor_hashint_map_delete (slv->weights);
1422 }
1423 while (!BTOR_EMPTY_STACK (slv->moves))
1424 {
1425 m = BTOR_POP_STACK (slv->moves);
1426 btor_iter_hashint_init (&it, m->cans);
1427 while (btor_iter_hashint_has_next (&it))
1428 btor_bv_free (btor->mm, btor_iter_hashint_next_data (&it)->as_ptr);
1429 btor_hashint_map_delete (m->cans);
1430 }
1431 BTOR_RELEASE_STACK (slv->moves);
1432 if (slv->max_cans)
1433 {
1434 btor_iter_hashint_init (&it, slv->max_cans);
1435 while (btor_iter_hashint_has_next (&it))
1436 {
1437 assert (slv->max_cans->data[it.cur_pos].as_ptr);
1438 btor_bv_free (btor->mm, btor_iter_hashint_next_data (&it)->as_ptr);
1439 }
1440 btor_hashint_map_delete (slv->max_cans);
1441 }
1442 BTOR_DELETE (btor->mm, slv);
1443 }
1444
1445 /* Note: failed assumptions -> no handling necessary, sls only works for SAT
1446 * Note: limits are currently unused */
1447 static BtorSolverResult
sat_sls_solver(BtorSLSSolver * slv)1448 sat_sls_solver (BtorSLSSolver *slv)
1449 {
1450 assert (slv);
1451 assert (slv->kind == BTOR_SLS_SOLVER_KIND);
1452 assert (slv->btor);
1453 assert (slv->btor->slv == (BtorSolver *) slv);
1454
1455 int32_t j, max_steps, id, nmoves;
1456 uint32_t nprops;
1457 BtorSolverResult sat_result;
1458 BtorNode *root;
1459 BtorSLSConstrData *d;
1460 BtorPtrHashTableIterator pit;
1461 BtorIntHashTableIterator iit;
1462 Btor *btor;
1463
1464 btor = slv->btor;
1465 assert (!btor->inconsistent);
1466 nmoves = 0;
1467 nprops = btor_opt_get (btor, BTOR_OPT_PROP_NPROPS);
1468 slv->nflips = btor_opt_get (btor, BTOR_OPT_SLS_NFLIPS);
1469
1470 if (btor_terminate (btor))
1471 {
1472 sat_result = BTOR_RESULT_UNKNOWN;
1473 goto DONE;
1474 }
1475
1476 BTOR_ABORT (btor->ufs->count != 0
1477 || (!btor_opt_get (btor, BTOR_OPT_BETA_REDUCE)
1478 && btor->lambdas->count != 0),
1479 "sls engine supports QF_BV only");
1480
1481 /* Generate intial model, all bv vars are initialized with zero. We do
1482 * not have to consider model_for_all_nodes, but let this be handled by
1483 * the model generation (if enabled) after SAT has been determined. */
1484 slv->api.generate_model ((BtorSolver *) slv, false, true);
1485
1486 /* init assertion weights of ALL roots */
1487 assert (!slv->weights);
1488 slv->weights = btor_hashint_map_new (btor->mm);
1489 assert (btor->synthesized_constraints->count == 0);
1490 btor_iter_hashptr_init (&pit, btor->unsynthesized_constraints);
1491 while (btor_iter_hashptr_has_next (&pit))
1492 {
1493 root = btor_iter_hashptr_next (&pit);
1494 assert (!btor_hashptr_table_get (btor->unsynthesized_constraints,
1495 btor_node_invert (root)));
1496 id = btor_node_get_id (root);
1497 if (!btor_hashint_map_contains (slv->weights, id))
1498 {
1499 BTOR_CNEW (btor->mm, d);
1500 d->weight = 1; /* initial assertion weight */
1501 btor_hashint_map_add (slv->weights, id)->as_ptr = d;
1502 }
1503 }
1504 btor_iter_hashptr_init (&pit, btor->assumptions);
1505 while (btor_iter_hashptr_has_next (&pit))
1506 {
1507 root = btor_iter_hashptr_next (&pit);
1508 if (btor_hashptr_table_get (btor->unsynthesized_constraints,
1509 btor_node_invert (root)))
1510 goto UNSAT;
1511 if (btor_hashptr_table_get (btor->assumptions, btor_node_invert (root)))
1512 goto UNSAT;
1513 id = btor_node_get_id (root);
1514 if (!btor_hashint_map_contains (slv->weights, id))
1515 {
1516 BTOR_CNEW (btor->mm, d);
1517 d->weight = 1; /* initial assertion weight */
1518 btor_hashint_map_add (slv->weights, id)->as_ptr = d;
1519 }
1520 }
1521
1522 if (!slv->score) slv->score = btor_hashint_map_new (btor->mm);
1523
1524 for (;;)
1525 {
1526 if (btor_terminate (btor))
1527 {
1528 sat_result = BTOR_RESULT_UNKNOWN;
1529 goto DONE;
1530 }
1531
1532 /* init */
1533 slv->prop_flip_cond_const_prob =
1534 btor_opt_get (btor, BTOR_OPT_PROP_PROB_FLIP_COND_CONST);
1535 slv->prop_flip_cond_const_prob_delta =
1536 slv->prop_flip_cond_const_prob > (BTOR_PROB_MAX / 2)
1537 ? -BTOR_PROPUTILS_PROB_FLIP_COND_CONST_DELTA
1538 : BTOR_PROPUTILS_PROB_FLIP_COND_CONST_DELTA;
1539
1540 /* collect unsatisfied roots (kept up-to-date in update_cone) */
1541 assert (!slv->roots);
1542 slv->roots = btor_hashint_map_new (btor->mm);
1543 assert (btor->synthesized_constraints->count == 0);
1544 btor_iter_hashptr_init (&pit, btor->unsynthesized_constraints);
1545 btor_iter_hashptr_queue (&pit, btor->assumptions);
1546 while (btor_iter_hashptr_has_next (&pit))
1547 {
1548 root = btor_iter_hashptr_next (&pit);
1549 if (!btor_hashint_map_contains (slv->roots, btor_node_get_id (root))
1550 && btor_bv_is_zero (btor_model_get_bv (btor, root)))
1551 {
1552 if (btor_node_is_bv_const (root))
1553 goto UNSAT; /* contains false constraint -> unsat */
1554 btor_hashint_map_add (slv->roots, btor_node_get_id (root));
1555 }
1556 }
1557
1558 /* compute initial sls score */
1559 btor_slsutils_compute_sls_scores (
1560 btor, btor->bv_model, btor->fun_model, slv->score);
1561
1562 if (!slv->roots->count) goto SAT;
1563
1564 for (j = 0, max_steps = BTOR_SLS_MAXSTEPS (slv->stats.restarts + 1);
1565 !btor_opt_get (btor, BTOR_OPT_SLS_USE_RESTARTS) || j < max_steps;
1566 j++)
1567 {
1568 if (btor_terminate (btor)
1569 || (slv->nflips && slv->stats.flips >= slv->nflips)
1570 || (nprops && slv->stats.props >= nprops))
1571 {
1572 sat_result = BTOR_RESULT_UNKNOWN;
1573 goto DONE;
1574 }
1575
1576 if (!move (btor, nmoves)) goto UNSAT;
1577 nmoves += 1;
1578
1579 if (!slv->roots->count) goto SAT;
1580 }
1581
1582 /* restart */
1583 slv->api.generate_model ((BtorSolver *) slv, false, true);
1584 btor_hashint_map_delete (slv->score);
1585 btor_hashint_map_delete (slv->roots);
1586 slv->roots = 0;
1587 slv->score = btor_hashint_map_new (btor->mm);
1588 slv->stats.restarts += 1;
1589 }
1590
1591 SAT:
1592 sat_result = BTOR_RESULT_SAT;
1593 goto DONE;
1594
1595 UNSAT:
1596 sat_result = BTOR_RESULT_UNSAT;
1597
1598 DONE:
1599 if (slv->roots)
1600 {
1601 btor_hashint_map_delete (slv->roots);
1602 slv->roots = 0;
1603 }
1604 if (slv->weights)
1605 {
1606 btor_iter_hashint_init (&iit, slv->weights);
1607 while (btor_iter_hashint_has_next (&iit))
1608 BTOR_DELETE (
1609 btor->mm,
1610 (BtorSLSConstrData *) btor_iter_hashint_next_data (&iit)->as_ptr);
1611 btor_hashint_map_delete (slv->weights);
1612 slv->weights = 0;
1613 }
1614 if (slv->score)
1615 {
1616 btor_hashint_map_delete (slv->score);
1617 slv->score = 0;
1618 }
1619 return sat_result;
1620 }
1621
1622 static void
generate_model_sls_solver(BtorSLSSolver * slv,bool model_for_all_nodes,bool reset)1623 generate_model_sls_solver (BtorSLSSolver *slv,
1624 bool model_for_all_nodes,
1625 bool reset)
1626 {
1627 assert (slv);
1628 assert (slv->kind == BTOR_SLS_SOLVER_KIND);
1629 assert (slv->btor);
1630 assert (slv->btor->slv == (BtorSolver *) slv);
1631
1632 Btor *btor;
1633
1634 btor = slv->btor;
1635
1636 if (!reset && btor->bv_model) return;
1637 btor_model_init_bv (btor, &btor->bv_model);
1638 btor_model_init_fun (btor, &btor->fun_model);
1639 btor_model_generate (
1640 btor, btor->bv_model, btor->fun_model, model_for_all_nodes);
1641 }
1642
1643 static void
print_stats_sls_solver(BtorSLSSolver * slv)1644 print_stats_sls_solver (BtorSLSSolver *slv)
1645 {
1646 assert (slv);
1647 assert (slv->kind == BTOR_SLS_SOLVER_KIND);
1648 assert (slv->btor);
1649 assert (slv->btor->slv == (BtorSolver *) slv);
1650
1651 Btor *btor;
1652
1653 btor = slv->btor;
1654
1655 BTOR_MSG (btor->msg, 1, "");
1656 BTOR_MSG (btor->msg, 1, "sls restarts: %d", slv->stats.restarts);
1657 BTOR_MSG (btor->msg, 1, "sls moves: %d", slv->stats.moves);
1658 BTOR_MSG (btor->msg, 1, "sls flips: %d", slv->stats.flips);
1659 BTOR_MSG (btor->msg, 1, "sls propagation steps: %u", slv->stats.props);
1660 BTOR_MSG (btor->msg, 1, "");
1661 BTOR_MSG (btor->msg,
1662 1,
1663 "sls propagation move conflicts (recoverable): %d",
1664 slv->stats.move_prop_rec_conf);
1665 BTOR_MSG (btor->msg,
1666 1,
1667 "sls propagation move conflicts (non-recoverable): %d",
1668 slv->stats.move_prop_non_rec_conf);
1669
1670 BTOR_MSG (btor->msg, 1, "");
1671 BTOR_MSG (btor->msg, 1, "sls flip moves: %d", slv->stats.move_flip);
1672 BTOR_MSG (btor->msg, 1, "sls inc moves: %d", slv->stats.move_inc);
1673 BTOR_MSG (btor->msg, 1, "sls dec moves: %d", slv->stats.move_dec);
1674 BTOR_MSG (btor->msg, 1, "sls not moves: %d", slv->stats.move_not);
1675 BTOR_MSG (btor->msg, 1, "sls range moves: %d", slv->stats.move_range);
1676 BTOR_MSG (btor->msg, 1, "sls segment moves: %d", slv->stats.move_seg);
1677 BTOR_MSG (btor->msg, 1, "sls random moves: %d", slv->stats.move_rand);
1678 BTOR_MSG (
1679 btor->msg, 1, "sls random walk moves: %d", slv->stats.move_rand_walk);
1680 BTOR_MSG (btor->msg, 1, "sls propagation moves: %d", slv->stats.move_prop);
1681
1682 BTOR_MSG (btor->msg, 1, "");
1683 BTOR_MSG (
1684 btor->msg, 1, "sls gw flip moves: %d", slv->stats.move_gw_flip);
1685 BTOR_MSG (
1686 btor->msg, 1, "sls gw inc moves: %d", slv->stats.move_gw_inc);
1687 BTOR_MSG (
1688 btor->msg, 1, "sls gw dec moves: %d", slv->stats.move_gw_dec);
1689 BTOR_MSG (
1690 btor->msg, 1, "sls gw not moves: %d", slv->stats.move_gw_not);
1691 BTOR_MSG (
1692 btor->msg, 1, "sls gw range moves: %d", slv->stats.move_gw_range);
1693 BTOR_MSG (
1694 btor->msg, 1, "sls gw segment moves: %d", slv->stats.move_gw_seg);
1695 BTOR_MSG (
1696 btor->msg, 1, "sls gw random moves: %d", slv->stats.move_gw_rand);
1697 BTOR_MSG (btor->msg,
1698 1,
1699 "sls gw random walk moves: %d",
1700 slv->stats.move_gw_rand_walk);
1701 }
1702
1703 static void
print_time_stats_sls_solver(BtorSLSSolver * slv)1704 print_time_stats_sls_solver (BtorSLSSolver *slv)
1705 {
1706 assert (slv);
1707 assert (slv->kind == BTOR_SLS_SOLVER_KIND);
1708 assert (slv->btor);
1709 assert (slv->btor->slv == (BtorSolver *) slv);
1710
1711 Btor *btor = slv->btor;
1712
1713 BTOR_MSG (btor->msg, 1, "");
1714 BTOR_MSG (btor->msg,
1715 1,
1716 "%.2f seconds for updating cone (total)",
1717 slv->time.update_cone);
1718 BTOR_MSG (btor->msg,
1719 1,
1720 "%.2f seconds for updating cone (reset)",
1721 slv->time.update_cone_reset);
1722 BTOR_MSG (btor->msg,
1723 1,
1724 "%.2f seconds for updating cone (model gen)",
1725 slv->time.update_cone_model_gen);
1726 BTOR_MSG (btor->msg,
1727 1,
1728 "%.2f seconds for updating cone (compute score)",
1729 slv->time.update_cone_compute_score);
1730 BTOR_MSG (btor->msg, 1, "");
1731 }
1732
1733 static void
print_model_sls_solver(BtorSLSSolver * slv,const char * format,FILE * file)1734 print_model_sls_solver (BtorSLSSolver *slv, const char *format, FILE *file)
1735 {
1736 btor_print_model_aufbv (slv->btor, format, file);
1737 }
1738
1739 BtorSolver *
btor_new_sls_solver(Btor * btor)1740 btor_new_sls_solver (Btor *btor)
1741 {
1742 assert (btor);
1743
1744 BtorSLSSolver *slv;
1745
1746 BTOR_CNEW (btor->mm, slv);
1747
1748 slv->kind = BTOR_SLS_SOLVER_KIND;
1749 slv->btor = btor;
1750
1751 BTOR_INIT_STACK (btor->mm, slv->moves);
1752
1753 slv->api.clone = (BtorSolverClone) clone_sls_solver;
1754 slv->api.delet = (BtorSolverDelete) delete_sls_solver;
1755 slv->api.sat = (BtorSolverSat) sat_sls_solver;
1756 slv->api.generate_model = (BtorSolverGenerateModel) generate_model_sls_solver;
1757 slv->api.print_stats = (BtorSolverPrintStats) print_stats_sls_solver;
1758 slv->api.print_time_stats =
1759 (BtorSolverPrintTimeStats) print_time_stats_sls_solver;
1760 slv->api.print_model = (BtorSolverPrintModel) print_model_sls_solver;
1761
1762 BTOR_MSG (btor->msg, 1, "enabled sls engine");
1763
1764 return (BtorSolver *) slv;
1765 }
1766
1767 /*------------------------------------------------------------------------*/
1768