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 "btorproputils.h"
10
11 #include "btorprintmodel.h"
12 #include "btorslsutils.h"
13 #include "utils/btornodeiter.h"
14 #include "utils/btorutil.h"
15
16 /* ========================================================================== */
17 /* Path selection (for down-propagation) */
18 /* ========================================================================== */
19
20 static int32_t
select_path_non_const(BtorNode * exp)21 select_path_non_const (BtorNode *exp)
22 {
23 assert (exp);
24 assert (btor_node_is_regular (exp));
25 assert (exp->arity <= 2);
26 assert (!btor_node_is_bv_const (exp->e[0])
27 || (exp->arity > 1 && !btor_node_is_bv_const (exp->e[1])));
28
29 uint32_t i;
30 int32_t eidx;
31
32 for (i = 0, eidx = -1; i < exp->arity; i++)
33 if (btor_node_is_bv_const (exp->e[i]))
34 {
35 eidx = i ? 0 : 1;
36 break;
37 }
38 assert (exp->arity == 1 || !btor_node_is_bv_const (exp->e[i ? 0 : 1]));
39 return eidx;
40 }
41
42 static int32_t
select_path_random(Btor * btor,BtorNode * exp)43 select_path_random (Btor *btor, BtorNode *exp)
44 {
45 assert (btor);
46 assert (exp);
47 return (int32_t) btor_rng_pick_rand (&btor->rng, 0, exp->arity - 1);
48 }
49
50 static int32_t
select_path_add(Btor * btor,BtorNode * add,BtorBitVector * bvadd,BtorBitVector ** bve)51 select_path_add (Btor *btor,
52 BtorNode *add,
53 BtorBitVector *bvadd,
54 BtorBitVector **bve)
55 {
56 assert (btor);
57 assert (add);
58 assert (btor_node_is_regular (add));
59 assert (bvadd);
60 assert (bve);
61
62 (void) bvadd;
63 (void) bve;
64
65 int32_t eidx;
66
67 eidx = select_path_non_const (add);
68 if (eidx == -1) eidx = select_path_random (btor, add);
69 assert (eidx >= 0);
70 #ifndef NBTORLOG
71 char *a;
72 BtorMemMgr *mm = btor->mm;
73 BTORLOG (2, "");
74 BTORLOG (2, "select path: %s", btor_util_node2string (add));
75 a = btor_bv_to_char (mm, bve[0]);
76 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (add->e[0]), a);
77 btor_mem_freestr (mm, a);
78 a = btor_bv_to_char (mm, bve[1]);
79 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (add->e[1]), a);
80 btor_mem_freestr (mm, a);
81 BTORLOG (2, " * chose: %d", eidx);
82 #endif
83 return eidx;
84 }
85
86 static int32_t
select_path_and(Btor * btor,BtorNode * and,BtorBitVector * bvand,BtorBitVector ** bve)87 select_path_and (Btor *btor,
88 BtorNode *and,
89 BtorBitVector *bvand,
90 BtorBitVector **bve)
91 {
92 assert (btor);
93 assert (and);
94 assert (btor_node_is_regular (and));
95 assert (bvand);
96 assert (bve);
97
98 uint32_t opt;
99 int32_t i, eidx;
100 BtorBitVector *tmp;
101 BtorMemMgr *mm;
102
103 mm = btor->mm;
104 eidx = select_path_non_const (and);
105
106 if (eidx == -1)
107 {
108 opt = btor_opt_get (btor, BTOR_OPT_PROP_PATH_SEL);
109
110 if (opt == BTOR_PROP_PATH_SEL_RANDOM)
111 {
112 eidx = select_path_random (btor, and);
113 }
114 else if (btor_node_bv_get_width (btor, and) == 1)
115 {
116 /* choose 0-branch if exactly one branch is 0, else choose randomly */
117 for (i = 0; i < and->arity; i++)
118 if (btor_bv_is_zero (bve[i])) eidx = eidx == -1 ? i : -1;
119 if (eidx == -1) eidx = select_path_random (btor, and);
120 }
121 else if (opt == BTOR_PROP_PATH_SEL_ESSENTIAL)
122 {
123 /* 1) all bits set in bvand must be set in both inputs, but
124 * 2) all bits NOT set in bvand can be cancelled out by either or both
125 * -> choose single input that violates 1)
126 * -> else choose randomly */
127 for (i = 0; i < and->arity; i++)
128 {
129 tmp = btor_bv_and (mm, bvand, bve[i]);
130 if (btor_bv_compare (tmp, bvand)) eidx = eidx == -1 ? i : -1;
131 btor_bv_free (mm, tmp);
132 }
133 }
134 if (eidx == -1) eidx = select_path_random (btor, and);
135 }
136
137 assert (eidx >= 0);
138 #ifndef NBTORLOG
139 char *a;
140 BTORLOG (2, "");
141 BTORLOG (2, "select path: %s", btor_util_node2string (and));
142 a = btor_bv_to_char (mm, bve[0]);
143 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (and->e[0]), a);
144 btor_mem_freestr (mm, a);
145 a = btor_bv_to_char (mm, bve[1]);
146 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (and->e[1]), a);
147 btor_mem_freestr (mm, a);
148 BTORLOG (2, " * chose: %d", eidx);
149 #endif
150 return eidx;
151 }
152
153 static int32_t
select_path_eq(Btor * btor,BtorNode * eq,BtorBitVector * bveq,BtorBitVector ** bve)154 select_path_eq (Btor *btor,
155 BtorNode *eq,
156 BtorBitVector *bveq,
157 BtorBitVector **bve)
158 {
159 assert (btor);
160 assert (eq);
161 assert (btor_node_is_regular (eq));
162 assert (bveq);
163 assert (bve);
164
165 (void) bveq;
166 (void) bve;
167
168 int32_t eidx;
169 eidx = select_path_non_const (eq);
170 if (eidx == -1) eidx = select_path_random (btor, eq);
171 assert (eidx >= 0);
172 #ifndef NBTORLOG
173 char *a;
174 BtorMemMgr *mm = btor->mm;
175 BTORLOG (2, "");
176 BTORLOG (2, "select path: %s", btor_util_node2string (eq));
177 a = btor_bv_to_char (mm, bve[0]);
178 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (eq->e[0]), a);
179 btor_mem_freestr (mm, a);
180 a = btor_bv_to_char (mm, bve[1]);
181 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (eq->e[1]), a);
182 btor_mem_freestr (mm, a);
183 BTORLOG (2, " * chose: %d", eidx);
184 #endif
185 return eidx;
186 }
187
188 static int32_t
select_path_ult(Btor * btor,BtorNode * ult,BtorBitVector * bvult,BtorBitVector ** bve)189 select_path_ult (Btor *btor,
190 BtorNode *ult,
191 BtorBitVector *bvult,
192 BtorBitVector **bve)
193 {
194 assert (btor);
195 assert (ult);
196 assert (btor_node_is_regular (ult));
197 assert (bvult);
198 assert (bve);
199
200 int32_t eidx;
201 BtorBitVector *bvmax;
202 BtorMemMgr *mm;
203
204 mm = btor->mm;
205 eidx = select_path_non_const (ult);
206
207 if (eidx == -1)
208 {
209 if (btor_opt_get (btor, BTOR_OPT_PROP_PATH_SEL)
210 == BTOR_PROP_PATH_SEL_ESSENTIAL)
211 {
212 bvmax = btor_bv_ones (mm, btor_bv_get_width (bve[0]));
213 if (btor_bv_is_one (bvult))
214 {
215 /* 1...1 < bve[1] */
216 if (!btor_bv_compare (bve[0], bvmax)) eidx = 0;
217 /* bve[0] < 0 */
218 if (btor_bv_is_zero (bve[1])) eidx = eidx == -1 ? 1 : -1;
219 }
220 btor_bv_free (mm, bvmax);
221 }
222 if (eidx == -1) eidx = select_path_random (btor, ult);
223 }
224
225 assert (eidx >= 0);
226 #ifndef NBTORLOG
227 char *a;
228 BTORLOG (2, "");
229 BTORLOG (2, "select path: %s", btor_util_node2string (ult));
230 a = btor_bv_to_char (mm, bve[0]);
231 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (ult->e[0]), a);
232 btor_mem_freestr (mm, a);
233 a = btor_bv_to_char (mm, bve[1]);
234 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (ult->e[1]), a);
235 btor_mem_freestr (mm, a);
236 BTORLOG (2, " * chose: %d", eidx);
237 #endif
238 return eidx;
239 }
240
241 static int32_t
select_path_sll(Btor * btor,BtorNode * sll,BtorBitVector * bvsll,BtorBitVector ** bve)242 select_path_sll (Btor *btor,
243 BtorNode *sll,
244 BtorBitVector *bvsll,
245 BtorBitVector **bve)
246 {
247 assert (btor);
248 assert (sll);
249 assert (btor_node_is_regular (sll));
250 assert (bvsll);
251 assert (bve);
252
253 int32_t eidx;
254 uint32_t bw;
255 uint64_t i, j, shift;
256 BtorBitVector *bv_bw, *tmp;
257 BtorMemMgr *mm;
258
259 eidx = select_path_non_const (sll);
260
261 mm = btor->mm;
262 bw = btor_bv_get_width (bvsll);
263 assert (btor_bv_get_width (bve[0]) == bw);
264 assert (btor_bv_get_width (bve[1]) == bw);
265
266 if (eidx == -1)
267 {
268 if (btor_opt_get (btor, BTOR_OPT_PROP_PATH_SEL)
269 == BTOR_PROP_PATH_SEL_ESSENTIAL)
270 {
271 if (bw > 64)
272 {
273 bv_bw = btor_bv_uint64_to_bv (mm, bw, bw);
274 tmp = btor_bv_ugte (mm, bve[1], bv_bw);
275 if (btor_bv_is_one (tmp) && !btor_bv_is_zero (bvsll))
276 {
277 btor_bv_free (mm, bv_bw);
278 btor_bv_free (mm, tmp);
279 eidx = 1;
280 goto DONE;
281 }
282 btor_bv_free (mm, bv_bw);
283 btor_bv_free (mm, tmp);
284 /* actual value is small enough to fit into 32 bit (max bit width
285 * handled by Boolector is INT32_MAX) */
286 tmp = btor_bv_slice (mm, bve[1], 32, 0);
287 shift = btor_bv_to_uint64 (tmp);
288 btor_bv_free (mm, tmp);
289 }
290 else
291 {
292 shift = btor_bv_to_uint64 (bve[1]);
293 }
294 /* if shift is greater than bit-width, result must be zero */
295 if (!btor_bv_is_zero (bvsll) && shift >= bw)
296 {
297 eidx = 1;
298 goto DONE;
299 }
300 if (shift < bw)
301 {
302 /* bve[1] and number of LSB 0-bits in bvsll must match */
303 for (i = 0; i < shift; i++)
304 {
305 if (btor_bv_get_bit (bvsll, i))
306 {
307 eidx = 1;
308 goto DONE;
309 }
310 }
311 /* bve[0] and bvsll (except for the bits shifted out) must match */
312 for (i = 0, j = shift; i < bw - j; i++)
313 {
314 if (btor_bv_get_bit (bve[0], i) != btor_bv_get_bit (bvsll, j + i))
315 {
316 eidx = eidx == -1 ? 0 : -1;
317 break;
318 }
319 }
320 }
321 }
322 if (eidx == -1) eidx = select_path_random (btor, sll);
323 }
324 DONE:
325 assert (eidx >= 0);
326 #ifndef NBTORLOG
327 char *a;
328 BTORLOG (2, "");
329 BTORLOG (2, "select path: %s", btor_util_node2string (sll));
330 a = btor_bv_to_char (mm, bve[0]);
331 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (sll->e[0]), a);
332 btor_mem_freestr (mm, a);
333 a = btor_bv_to_char (mm, bve[1]);
334 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (sll->e[1]), a);
335 btor_mem_freestr (mm, a);
336 BTORLOG (2, " * chose: %d", eidx);
337 #endif
338 return eidx;
339 }
340
341 static int32_t
select_path_srl(Btor * btor,BtorNode * srl,BtorBitVector * bvsrl,BtorBitVector ** bve)342 select_path_srl (Btor *btor,
343 BtorNode *srl,
344 BtorBitVector *bvsrl,
345 BtorBitVector **bve)
346 {
347 assert (btor);
348 assert (srl);
349 assert (btor_node_is_regular (srl));
350 assert (bvsrl);
351 assert (bve);
352
353 int32_t eidx;
354 uint32_t bw;
355 uint64_t i, j, shift;
356 BtorBitVector *bv_bw, *tmp;
357 BtorMemMgr *mm;
358
359 eidx = select_path_non_const (srl);
360
361 mm = btor->mm;
362 bw = btor_bv_get_width (bvsrl);
363 assert (btor_bv_get_width (bve[0]) == bw);
364 assert (btor_bv_get_width (bve[1]) == bw);
365
366 if (eidx == -1)
367 {
368 if (btor_opt_get (btor, BTOR_OPT_PROP_PATH_SEL)
369 == BTOR_PROP_PATH_SEL_ESSENTIAL)
370 {
371 if (bw > 64)
372 {
373 bv_bw = btor_bv_uint64_to_bv (mm, bw, bw);
374 tmp = btor_bv_ugte (mm, bve[1], bv_bw);
375 if (btor_bv_is_one (tmp) && !btor_bv_is_zero (bvsrl))
376 {
377 btor_bv_free (mm, bv_bw);
378 btor_bv_free (mm, tmp);
379 eidx = 1;
380 goto DONE;
381 }
382 btor_bv_free (mm, bv_bw);
383 btor_bv_free (mm, tmp);
384 /* actual value is small enough to fit into 32 bit (max bit width
385 * handled by Boolector is INT32_MAX) */
386 tmp = btor_bv_slice (mm, bve[1], 32, 0);
387 shift = btor_bv_to_uint64 (tmp);
388 btor_bv_free (mm, tmp);
389 }
390 else
391 {
392 shift = btor_bv_to_uint64 (bve[1]);
393 }
394 /* if shift is greater than bit-width, result must be zero */
395 if (!btor_bv_is_zero (bvsrl) && shift >= bw)
396 {
397 eidx = 1;
398 goto DONE;
399 }
400 if (shift < bw)
401 {
402 /* bve[1] and number of MSB 0-bits in bvsrl must match */
403 for (i = 0; i < shift; i++)
404 {
405 if (btor_bv_get_bit (bvsrl, bw - 1 - i))
406 {
407 eidx = 1;
408 goto DONE;
409 }
410 }
411 /* bve[0] and bvsrl (except for the bits shifted out) must match */
412 for (i = 0, j = shift; i < bw - j; i++)
413 {
414 if (btor_bv_get_bit (bve[0], bw - 1 - i)
415 != btor_bv_get_bit (bvsrl, bw - 1 - (j + i)))
416 {
417 eidx = eidx == -1 ? 0 : -1;
418 break;
419 }
420 }
421 }
422 }
423 if (eidx == -1) eidx = select_path_random (btor, srl);
424 }
425 DONE:
426 assert (eidx >= 0);
427 #ifndef NBTORLOG
428 char *a;
429 BTORLOG (2, "");
430 BTORLOG (2, "select path: %s", btor_util_node2string (srl));
431 a = btor_bv_to_char (mm, bve[0]);
432 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (srl->e[0]), a);
433 btor_mem_freestr (mm, a);
434 a = btor_bv_to_char (mm, bve[1]);
435 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (srl->e[1]), a);
436 btor_mem_freestr (mm, a);
437 BTORLOG (2, " * chose: %d", eidx);
438 #endif
439 return eidx;
440 }
441
442 static int32_t
select_path_mul(Btor * btor,BtorNode * mul,BtorBitVector * bvmul,BtorBitVector ** bve)443 select_path_mul (Btor *btor,
444 BtorNode *mul,
445 BtorBitVector *bvmul,
446 BtorBitVector **bve)
447 {
448 assert (btor);
449 assert (mul);
450 assert (btor_node_is_regular (mul));
451 assert (bvmul);
452 assert (bve);
453
454 uint32_t ctz_bvmul;
455 int32_t eidx, lsbve0, lsbve1;
456 bool iszerobve0, iszerobve1;
457
458 eidx = select_path_non_const (mul);
459
460 if (eidx == -1)
461 {
462 if (btor_opt_get (btor, BTOR_OPT_PROP_PATH_SEL)
463 == BTOR_PROP_PATH_SEL_ESSENTIAL)
464 {
465 iszerobve0 = btor_bv_is_zero (bve[0]);
466 iszerobve1 = btor_bv_is_zero (bve[1]);
467
468 lsbve0 = btor_bv_get_bit (bve[0], 0);
469 lsbve1 = btor_bv_get_bit (bve[1], 0);
470
471 /* either bve[0] or bve[1] are 0 but bvmul > 0 */
472 if ((iszerobve0 || iszerobve1) && !btor_bv_is_zero (bvmul))
473 {
474 if (iszerobve0) eidx = 0;
475 if (iszerobve1) eidx = eidx == -1 ? 1 : -1;
476 }
477 /* bvmul is odd but either bve[0] or bve[1] are even */
478 else if (btor_bv_get_bit (bvmul, 0) && (!lsbve0 || !lsbve1))
479 {
480 if (!lsbve0) eidx = 0;
481 if (!lsbve1) eidx = eidx == -1 ? 1 : -1;
482 }
483 /* number of 0-LSBs in bvmul < number of 0-LSBs in bve[0|1] */
484 else
485 {
486 ctz_bvmul = btor_bv_get_num_trailing_zeros (bvmul);
487 if (ctz_bvmul < btor_bv_get_num_trailing_zeros (bve[0])) eidx = 0;
488 if (ctz_bvmul < btor_bv_get_num_trailing_zeros (bve[1]))
489 eidx = eidx == -1 ? 1 : -1;
490 }
491 }
492 if (eidx == -1) eidx = select_path_random (btor, mul);
493 }
494 assert (eidx >= 0);
495 #ifndef NBTORLOG
496 char *a;
497 BtorMemMgr *mm = btor->mm;
498 BTORLOG (2, "");
499 BTORLOG (2, "select path: %s", btor_util_node2string (mul));
500 a = btor_bv_to_char (mm, bve[0]);
501 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (mul->e[0]), a);
502 btor_mem_freestr (mm, a);
503 a = btor_bv_to_char (mm, bve[1]);
504 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (mul->e[1]), a);
505 btor_mem_freestr (mm, a);
506 BTORLOG (2, " * chose: %d", eidx);
507 #endif
508 return eidx;
509 }
510
511 static int32_t
select_path_udiv(Btor * btor,BtorNode * udiv,BtorBitVector * bvudiv,BtorBitVector ** bve)512 select_path_udiv (Btor *btor,
513 BtorNode *udiv,
514 BtorBitVector *bvudiv,
515 BtorBitVector **bve)
516 {
517 assert (btor);
518 assert (udiv);
519 assert (btor_node_is_regular (udiv));
520 assert (bvudiv);
521 assert (bve);
522
523 int32_t eidx, cmp_udiv_max;
524 BtorBitVector *bvmax, *up, *lo, *tmp;
525 BtorMemMgr *mm;
526
527 mm = btor->mm;
528 eidx = select_path_non_const (udiv);
529
530 if (eidx == -1)
531 {
532 if (btor_opt_get (btor, BTOR_OPT_PROP_PATH_SEL)
533 == BTOR_PROP_PATH_SEL_ESSENTIAL)
534 {
535 bvmax = btor_bv_ones (mm, btor_bv_get_width (bve[0]));
536 cmp_udiv_max = btor_bv_compare (bvudiv, bvmax);
537
538 /* bve[0] / bve[1] = 1...1 -> choose e[1]
539 * + 1...1 / 0 = 1...1
540 * + 1...1 / 1 = 1...1
541 * + x...x / 0 = 1...1 */
542 if (!cmp_udiv_max)
543 eidx = 1;
544 else
545 {
546 /* 1...1 / e[0] = 0 -> choose e[0] */
547 if (btor_bv_is_zero (bvudiv) && !btor_bv_compare (bve[0], bvmax))
548 eidx = 0;
549 /* bve[0] < bvudiv -> choose e[0] */
550 else if (btor_bv_compare (bve[0], bvudiv) < 0)
551 eidx = 0;
552 else
553 {
554 up = btor_bv_udiv (mm, bve[0], bvudiv);
555 lo = btor_bv_inc (mm, bvudiv);
556 tmp = btor_bv_udiv (mm, bve[0], lo);
557 btor_bv_free (mm, lo);
558 lo = btor_bv_inc (mm, tmp);
559
560 if (btor_bv_compare (lo, up) > 0) eidx = 0;
561 btor_bv_free (mm, up);
562 btor_bv_free (mm, lo);
563 btor_bv_free (mm, tmp);
564 }
565
566 /* e[0] / 0 != 1...1 -> choose e[1] */
567 if (btor_bv_is_zero (bve[1]) || btor_bv_is_umulo (mm, bve[1], bvudiv))
568 eidx = eidx == -1 ? 1 : -1;
569 }
570 btor_bv_free (mm, bvmax);
571 }
572 if (eidx == -1) eidx = select_path_random (btor, udiv);
573 }
574
575 assert (eidx >= 0);
576 #ifndef NBTORLOG
577 char *a;
578 BTORLOG (2, "");
579 BTORLOG (2, "select path: %s", btor_util_node2string (udiv));
580 a = btor_bv_to_char (mm, bve[0]);
581 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (udiv->e[0]), a);
582 btor_mem_freestr (mm, a);
583 a = btor_bv_to_char (mm, bve[1]);
584 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (udiv->e[1]), a);
585 btor_mem_freestr (mm, a);
586 BTORLOG (2, " * chose: %d", eidx);
587 #endif
588 return eidx;
589 }
590
591 static int32_t
select_path_urem(Btor * btor,BtorNode * urem,BtorBitVector * bvurem,BtorBitVector ** bve)592 select_path_urem (Btor *btor,
593 BtorNode *urem,
594 BtorBitVector *bvurem,
595 BtorBitVector **bve)
596 {
597 assert (btor);
598 assert (urem);
599 assert (btor_node_is_regular (urem));
600 assert (bvurem);
601 assert (bve);
602
603 int32_t eidx;
604 BtorBitVector *bvmax, *sub, *tmp;
605 BtorMemMgr *mm;
606
607 mm = btor->mm;
608 eidx = select_path_non_const (urem);
609
610 if (eidx == -1)
611 {
612 if (btor_opt_get (btor, BTOR_OPT_PROP_PATH_SEL)
613 == BTOR_PROP_PATH_SEL_ESSENTIAL)
614 {
615 bvmax = btor_bv_ones (mm, btor_bv_get_width (bve[0]));
616 sub = btor_bv_sub (mm, bve[0], bvurem);
617 tmp = btor_bv_dec (mm, bve[0]);
618
619 /* bvurem = 1...1 -> bve[0] = 1...1 and bve[1] = 0...0 */
620 if (!btor_bv_compare (bvurem, bvmax))
621 {
622 if (!btor_bv_is_zero (bve[1])) eidx = 1;
623 if (btor_bv_compare (bve[0], bvmax)) eidx = eidx == -1 ? 0 : -1;
624 }
625 /* bvurem > 0 and bve[1] = 1 */
626 else if (!btor_bv_is_zero (bvurem) && btor_bv_is_one (bve[1]))
627 {
628 eidx = 1;
629 }
630 /* 0 < bve[1] <= bvurem */
631 else if (!btor_bv_is_zero (bve[1])
632 && btor_bv_compare (bve[1], bvurem) <= 0)
633 {
634 eidx = eidx == -1 ? 1 : -1;
635 }
636 /* bve[0] < bvurem or
637 * bve[0] > bvurem and bve[0] - bvurem <= bvurem or
638 * and bve[0] - 1 = bvurem */
639 else if (btor_bv_compare (bve[0], bvurem) < 0
640 || (btor_bv_compare (bve[0], bvurem) > 0
641 && (btor_bv_compare (sub, bvurem) <= 0
642 || !btor_bv_compare (tmp, bvurem))))
643 {
644 eidx = 0;
645 }
646
647 btor_bv_free (mm, tmp);
648 btor_bv_free (mm, bvmax);
649 btor_bv_free (mm, sub);
650 }
651
652 if (eidx == -1) eidx = select_path_random (btor, urem);
653 }
654
655 assert (eidx >= 0);
656 #ifndef NBTORLOG
657 char *a;
658 BTORLOG (2, "");
659 BTORLOG (2, "select path: %s", btor_util_node2string (urem));
660 a = btor_bv_to_char (mm, bve[0]);
661 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (urem->e[0]), a);
662 btor_mem_freestr (mm, a);
663 a = btor_bv_to_char (mm, bve[1]);
664 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (urem->e[1]), a);
665 btor_mem_freestr (mm, a);
666 BTORLOG (2, " * chose: %d", eidx);
667 #endif
668 return eidx;
669 }
670
671 static int32_t
select_path_concat(Btor * btor,BtorNode * concat,BtorBitVector * bvconcat,BtorBitVector ** bve)672 select_path_concat (Btor *btor,
673 BtorNode *concat,
674 BtorBitVector *bvconcat,
675 BtorBitVector **bve)
676 {
677 assert (btor);
678 assert (concat);
679 assert (btor_node_is_regular (concat));
680 assert (bvconcat);
681 assert (bve);
682
683 int32_t eidx;
684 uint32_t bw_concat;
685 BtorBitVector *tmp;
686 BtorMemMgr *mm;
687
688 mm = btor->mm;
689 eidx = select_path_non_const (concat);
690
691 if (eidx == -1)
692 {
693 if (btor_opt_get (btor, BTOR_OPT_PROP_PATH_SEL)
694 == BTOR_PROP_PATH_SEL_ESSENTIAL)
695 {
696 /* bve[0] o bve[1] = bvconcat
697 * -> bve[0] resp. bve[1] must match with bvconcat */
698 bw_concat = btor_bv_get_width (bvconcat);
699 tmp = btor_bv_slice (
700 mm, bvconcat, bw_concat - 1, bw_concat - btor_bv_get_width (bve[0]));
701 if (btor_bv_compare (tmp, bve[0])) eidx = 0;
702 btor_bv_free (mm, tmp);
703 tmp = btor_bv_slice (mm, bvconcat, btor_bv_get_width (bve[1]) - 1, 0);
704 if (btor_bv_compare (tmp, bve[1])) eidx = eidx == -1 ? 1 : -1;
705 btor_bv_free (mm, tmp);
706 }
707
708 if (eidx == -1) eidx = select_path_random (btor, concat);
709 }
710
711 assert (eidx >= 0);
712 #ifndef NBTORLOG
713 char *a;
714 BTORLOG (2, "");
715 BTORLOG (2, "select path: %s", btor_util_node2string (concat));
716 a = btor_bv_to_char (mm, bve[0]);
717 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (concat->e[0]), a);
718 btor_mem_freestr (mm, a);
719 a = btor_bv_to_char (mm, bve[1]);
720 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (concat->e[1]), a);
721 btor_mem_freestr (mm, a);
722 BTORLOG (2, " * chose: %d", eidx);
723 #endif
724 return eidx;
725 }
726
727 static int32_t
select_path_slice(Btor * btor,BtorNode * slice,BtorBitVector * bvslice,BtorBitVector ** bve)728 select_path_slice (Btor *btor,
729 BtorNode *slice,
730 BtorBitVector *bvslice,
731 BtorBitVector **bve)
732 {
733 assert (btor);
734 assert (slice);
735 assert (btor_node_is_regular (slice));
736 assert (bvslice);
737 assert (bve);
738
739 assert (!btor_node_is_bv_const (slice->e[0]));
740
741 (void) btor;
742 (void) slice;
743 (void) bvslice;
744 (void) bve;
745 #ifndef NBTORLOG
746 char *a;
747 BtorMemMgr *mm = btor->mm;
748 BTORLOG (2, "");
749 BTORLOG (2, "select path: %s", btor_util_node2string (slice));
750 a = btor_bv_to_char (mm, bve[0]);
751 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (slice->e[0]), a);
752 btor_mem_freestr (mm, a);
753 BTORLOG (2, " * chose: 0");
754 #endif
755
756 return 0;
757 }
758
759 static int32_t
select_path_cond(Btor * btor,BtorNode * cond,BtorBitVector * bvcond,BtorBitVector ** bve)760 select_path_cond (Btor *btor,
761 BtorNode *cond,
762 BtorBitVector *bvcond,
763 BtorBitVector **bve)
764 {
765 assert (btor);
766 assert (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP
767 || btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_SLS);
768 assert (cond);
769 assert (btor_node_is_regular (cond));
770 assert (bvcond);
771 assert (bve);
772
773 bool e1const, e2const;
774 int32_t eidx;
775 uint32_t prob;
776 BtorBitVector *bve0;
777
778 (void) bvcond;
779
780 bve0 = *bve;
781 assert (bve0);
782
783 if (btor_node_is_bv_const (cond->e[0]))
784 eidx = cond->e[0] == btor->true_exp ? 1 : 2;
785 else
786 {
787 e1const = btor_node_is_bv_const (cond->e[1]);
788 e2const = btor_node_is_bv_const (cond->e[2]);
789
790 /* flip condition
791 *
792 * if either the 'then' or 'else' branch is const
793 * with probability BTOR_OPT_PROP_FLIP_COND_CONST_PROB,
794 * which is dynamically updated (depending on the number
795 * times this case has already bin encountered)
796 *
797 * else with probability BTOR_OPT_PROP_FLIP_COND_PROB,
798 * which is constant and will not be updated */
799 if (((e1const && btor_bv_is_true (bve0))
800 || (e2const && btor_bv_is_false (bve0)))
801 && btor_rng_pick_with_prob (
802 &btor->rng,
803 (prob = btor_opt_get (btor, BTOR_OPT_PROP_PROB_FLIP_COND_CONST))))
804 {
805 eidx = 0;
806
807 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
808 {
809 BtorPropSolver *slv;
810 slv = BTOR_PROP_SOLVER (btor);
811 if (++slv->nflip_cond_const
812 == btor_opt_get (btor, BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL))
813 {
814 slv->nflip_cond_const = 0;
815 slv->flip_cond_const_prob_delta =
816 prob == 0
817 ? 100
818 : (prob == 1000 ? -100 : slv->flip_cond_const_prob_delta);
819 btor_opt_set (btor,
820 BTOR_OPT_PROP_PROB_FLIP_COND_CONST,
821 prob + slv->flip_cond_const_prob_delta);
822 }
823 }
824 else
825 {
826 BtorSLSSolver *slv;
827 slv = BTOR_SLS_SOLVER (btor);
828 if (++slv->prop_nflip_cond_const
829 == btor_opt_get (btor, BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL))
830 {
831 slv->prop_nflip_cond_const = 0;
832 slv->prop_flip_cond_const_prob_delta =
833 prob == 0 ? 100
834 : (prob == 1000 ? -100
835 : slv->prop_flip_cond_const_prob_delta);
836 btor_opt_set (btor,
837 BTOR_OPT_PROP_PROB_FLIP_COND_CONST,
838 prob + slv->prop_flip_cond_const_prob_delta);
839 }
840 }
841 }
842 else if (btor_rng_pick_with_prob (
843 &btor->rng, btor_opt_get (btor, BTOR_OPT_PROP_PROB_FLIP_COND)))
844 {
845 eidx = 0;
846 }
847 /* assume cond to be fixed and select enabled branch */
848 else
849 {
850 eidx = btor_bv_is_true (bve0) ? 1 : 2;
851 }
852 }
853
854 #ifndef NBTORLOG
855 char *a;
856 BtorMemMgr *mm = btor->mm;
857
858 BTORLOG (2, "");
859 BTORLOG (2, "select path: %s", btor_util_node2string (cond));
860 a = btor_bv_to_char (mm, bve0);
861 BTORLOG (2, " e[0]: %s (%s)", btor_util_node2string (cond->e[0]), a);
862 btor_mem_freestr (mm, a);
863 a = btor_bv_to_char (mm, btor_model_get_bv (btor, cond->e[1]));
864 BTORLOG (2, " e[1]: %s (%s)", btor_util_node2string (cond->e[1]), a);
865 btor_mem_freestr (mm, a);
866 a = btor_bv_to_char (mm, btor_model_get_bv (btor, cond->e[2]));
867 BTORLOG (2, " e[2]: %s (%s)", btor_util_node2string (cond->e[2]), a);
868 btor_mem_freestr (mm, a);
869 BTORLOG (2, " * chose: %d", eidx);
870 #endif
871 return eidx;
872 }
873
874 /* ========================================================================== */
875 /* Consistent value computation */
876 /* ========================================================================== */
877
878 #ifdef NDEBUG
879 static BtorBitVector *inv_slice_bv (
880 Btor *, BtorNode *, BtorBitVector *, BtorBitVector *, int32_t);
881 static BtorBitVector *inv_cond_bv (
882 Btor *, BtorNode *, BtorBitVector *, BtorBitVector *, int32_t);
883 #endif
884
885 static BtorBitVector *
cons_add_bv(Btor * btor,BtorNode * add,BtorBitVector * bvadd,BtorBitVector * bve,int32_t eidx)886 cons_add_bv (Btor *btor,
887 BtorNode *add,
888 BtorBitVector *bvadd,
889 BtorBitVector *bve,
890 int32_t eidx)
891 {
892 assert (btor);
893 assert (add);
894 assert (btor_node_is_regular (add));
895 assert (bvadd);
896 assert (bve);
897 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvadd));
898 assert (eidx >= 0 && eidx <= 1);
899 assert (!btor_node_is_bv_const (add->e[eidx]));
900
901 (void) add;
902 (void) bve;
903 (void) eidx;
904
905 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
906 {
907 #ifndef NDEBUG
908 BTOR_PROP_SOLVER (btor)->stats.cons_add++;
909 #endif
910 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
911 }
912 return btor_bv_new_random (btor->mm, &btor->rng, btor_bv_get_width (bvadd));
913 }
914
915 static BtorBitVector *
cons_and_bv(Btor * btor,BtorNode * and,BtorBitVector * bvand,BtorBitVector * bve,int32_t eidx)916 cons_and_bv (Btor *btor,
917 BtorNode *and,
918 BtorBitVector *bvand,
919 BtorBitVector *bve,
920 int32_t eidx)
921 {
922 assert (btor);
923 assert (and);
924 assert (btor_node_is_regular (and));
925 assert (bvand);
926 assert (bve);
927 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvand));
928 assert (eidx >= 0 && eidx <= 1);
929 assert (!btor_node_is_bv_const (and->e[eidx]));
930
931 uint32_t i, bw;
932 BtorBitVector *res;
933 BtorUIntStack dcbits;
934 bool b;
935
936 (void) bve;
937
938 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
939 {
940 #ifndef NDEBUG
941 BTOR_PROP_SOLVER (btor)->stats.cons_and++;
942 #endif
943 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
944 }
945
946 b = btor_rng_pick_with_prob (
947 &btor->rng, btor_opt_get (btor, BTOR_OPT_PROP_PROB_AND_FLIP));
948 BTOR_INIT_STACK (btor->mm, dcbits);
949
950 res = btor_bv_copy (btor->mm, btor_model_get_bv (btor, and->e[eidx]));
951
952 /* bve & res = bvand
953 * -> all bits set in bvand must be set in res
954 * -> all bits not set in bvand are chosen to be set randomly */
955 for (i = 0, bw = btor_bv_get_width (bvand); i < bw; i++)
956 {
957 if (btor_bv_get_bit (bvand, i))
958 btor_bv_set_bit (res, i, 1);
959 else if (b)
960 BTOR_PUSH_STACK (dcbits, i);
961 else
962 btor_bv_set_bit (res, i, btor_rng_pick_rand (&btor->rng, 0, 1));
963 }
964
965 if (b && BTOR_COUNT_STACK (dcbits))
966 btor_bv_flip_bit (
967 res,
968 BTOR_PEEK_STACK (
969 dcbits,
970 btor_rng_pick_rand (&btor->rng, 0, BTOR_COUNT_STACK (dcbits) - 1)));
971
972 BTOR_RELEASE_STACK (dcbits);
973 return res;
974 }
975
976 static BtorBitVector *
cons_eq_bv(Btor * btor,BtorNode * eq,BtorBitVector * bveq,BtorBitVector * bve,int32_t eidx)977 cons_eq_bv (Btor *btor,
978 BtorNode *eq,
979 BtorBitVector *bveq,
980 BtorBitVector *bve,
981 int32_t eidx)
982 {
983 assert (btor);
984 assert (eq);
985 assert (btor_node_is_regular (eq));
986 assert (bveq);
987 assert (btor_bv_get_width (bveq) == 1);
988 assert (bve);
989 assert (eidx >= 0 && eidx <= 1);
990 assert (!btor_node_is_bv_const (eq->e[eidx]));
991
992 (void) bveq;
993
994 BtorBitVector *res;
995
996 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
997 {
998 #ifndef NDEBUG
999 BTOR_PROP_SOLVER (btor)->stats.cons_eq++;
1000 #endif
1001 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1002 }
1003
1004 if (btor_rng_pick_with_prob (&btor->rng,
1005 btor_opt_get (btor, BTOR_OPT_PROP_PROB_EQ_FLIP)))
1006 {
1007 res = btor_bv_copy (btor->mm, btor_model_get_bv (btor, eq->e[eidx]));
1008 btor_bv_flip_bit (
1009 res, btor_rng_pick_rand (&btor->rng, 0, btor_bv_get_width (res) - 1));
1010 }
1011 else
1012 {
1013 res = btor_bv_new_random (btor->mm, &btor->rng, btor_bv_get_width (bve));
1014 }
1015 return res;
1016 }
1017
1018 static BtorBitVector *
cons_ult_bv(Btor * btor,BtorNode * ult,BtorBitVector * bvult,BtorBitVector * bve,int32_t eidx)1019 cons_ult_bv (Btor *btor,
1020 BtorNode *ult,
1021 BtorBitVector *bvult,
1022 BtorBitVector *bve,
1023 int32_t eidx)
1024 {
1025 assert (btor);
1026 assert (ult);
1027 assert (btor_node_is_regular (ult));
1028 assert (bvult);
1029 assert (btor_bv_get_width (bvult) == 1);
1030 assert (bve);
1031 assert (eidx >= 0 && eidx <= 1);
1032 assert (!btor_node_is_bv_const (ult->e[eidx]));
1033
1034 bool isult;
1035 uint32_t bw;
1036 BtorBitVector *bvmax, *zero, *tmp, *res;
1037 BtorMemMgr *mm;
1038
1039 (void) ult;
1040
1041 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1042 {
1043 #ifndef NDEBUG
1044 BTOR_PROP_SOLVER (btor)->stats.cons_ult++;
1045 #endif
1046 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1047 }
1048
1049 mm = btor->mm;
1050 bw = btor_bv_get_width (bve);
1051 isult = !btor_bv_is_zero (bvult);
1052 zero = btor_bv_new (mm, bw);
1053 bvmax = btor_bv_ones (mm, bw);
1054
1055 if (eidx && isult)
1056 {
1057 /* bve < res = 1 -> res > 0 */
1058 tmp = btor_bv_one (mm, bw);
1059 res = btor_bv_new_random_range (mm, &btor->rng, bw, tmp, bvmax);
1060 btor_bv_free (mm, tmp);
1061 }
1062 else if (!eidx && isult)
1063 {
1064 /* res < bve = 1 -> 0 <= res < 1...1 */
1065 tmp = btor_bv_dec (mm, bvmax);
1066 res = btor_bv_new_random_range (mm, &btor->rng, bw, zero, tmp);
1067 btor_bv_free (mm, tmp);
1068 }
1069 else
1070 {
1071 res = btor_bv_new_random (mm, &btor->rng, bw);
1072 }
1073
1074 btor_bv_free (mm, bvmax);
1075 btor_bv_free (mm, zero);
1076
1077 return res;
1078 }
1079
1080 static BtorBitVector *
cons_sll_bv(Btor * btor,BtorNode * sll,BtorBitVector * bvsll,BtorBitVector * bve,int32_t eidx)1081 cons_sll_bv (Btor *btor,
1082 BtorNode *sll,
1083 BtorBitVector *bvsll,
1084 BtorBitVector *bve,
1085 int32_t eidx)
1086 {
1087 assert (btor);
1088 assert (sll);
1089 assert (btor_node_is_regular (sll));
1090 assert (bvsll);
1091 assert (bve);
1092 assert (eidx >= 0 && eidx <= 1);
1093 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvsll));
1094 assert (!btor_node_is_bv_const (sll->e[eidx]));
1095
1096 uint32_t i, bw, ctz_bvsll, shift;
1097 BtorBitVector *res, *bv_shift;
1098 BtorMemMgr *mm;
1099
1100 (void) sll;
1101 (void) bve;
1102
1103 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1104 {
1105 #ifndef NDEBUG
1106 BTOR_PROP_SOLVER (btor)->stats.cons_sll++;
1107 #endif
1108 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1109 }
1110
1111 mm = btor->mm;
1112 bw = btor_bv_get_width (bvsll);
1113
1114 ctz_bvsll = btor_bv_get_num_trailing_zeros (bvsll);
1115 shift = btor_rng_pick_rand (
1116 &btor->rng, 0, ctz_bvsll == bw ? ctz_bvsll - 1 : ctz_bvsll);
1117 bv_shift = btor_bv_uint64_to_bv (mm, shift, bw);
1118
1119 if (eidx)
1120 {
1121 res = bv_shift;
1122 }
1123 else
1124 {
1125 res = btor_bv_srl (mm, bvsll, bv_shift);
1126 for (i = 0; i < shift; i++)
1127 {
1128 btor_bv_set_bit (res, bw - 1 - i, btor_rng_pick_rand (&btor->rng, 0, 1));
1129 }
1130 btor_bv_free (mm, bv_shift);
1131 }
1132 return res;
1133 }
1134
1135 static BtorBitVector *
cons_srl_bv(Btor * btor,BtorNode * srl,BtorBitVector * bvsrl,BtorBitVector * bve,int32_t eidx)1136 cons_srl_bv (Btor *btor,
1137 BtorNode *srl,
1138 BtorBitVector *bvsrl,
1139 BtorBitVector *bve,
1140 int32_t eidx)
1141 {
1142 assert (btor);
1143 assert (srl);
1144 assert (btor_node_is_regular (srl));
1145 assert (bvsrl);
1146 assert (bve);
1147 assert (eidx >= 0 && eidx <= 1);
1148 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvsrl));
1149 assert (!btor_node_is_bv_const (srl->e[eidx]));
1150
1151 uint32_t i, shift, bw;
1152 BtorBitVector *res, *bv_shift;
1153 BtorMemMgr *mm;
1154
1155 (void) srl;
1156 (void) bve;
1157
1158 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1159 {
1160 #ifndef NDEBUG
1161 BTOR_PROP_SOLVER (btor)->stats.cons_srl++;
1162 #endif
1163 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1164 }
1165
1166 mm = btor->mm;
1167 bw = btor_bv_get_width (bvsrl);
1168
1169 for (i = 0; i < bw; i++)
1170 {
1171 if (btor_bv_get_bit (bvsrl, bw - 1 - i)) break;
1172 }
1173
1174 shift = btor_rng_pick_rand (&btor->rng, 0, i == bw ? i - 1 : i);
1175 bv_shift = btor_bv_uint64_to_bv (mm, shift, bw);
1176
1177 if (eidx)
1178 {
1179 res = bv_shift;
1180 }
1181 else
1182 {
1183 res = btor_bv_sll (mm, bvsrl, bv_shift);
1184 for (i = 0; i < shift; i++)
1185 {
1186 btor_bv_set_bit (res, i, btor_rng_pick_rand (&btor->rng, 0, 1));
1187 }
1188 btor_bv_free (mm, bv_shift);
1189 }
1190 return res;
1191 }
1192
1193 static BtorBitVector *
cons_mul_bv(Btor * btor,BtorNode * mul,BtorBitVector * bvmul,BtorBitVector * bve,int32_t eidx)1194 cons_mul_bv (Btor *btor,
1195 BtorNode *mul,
1196 BtorBitVector *bvmul,
1197 BtorBitVector *bve,
1198 int32_t eidx)
1199 {
1200 assert (btor);
1201 assert (mul);
1202 assert (btor_node_is_regular (mul));
1203 assert (bvmul);
1204 assert (bve);
1205 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvmul));
1206 assert (eidx >= 0 && eidx <= 1);
1207 assert (!btor_node_is_bv_const (mul->e[eidx]));
1208
1209 uint32_t r, bw, ctz_res, ctz_bvmul;
1210 BtorBitVector *res, *tmp;
1211 BtorMemMgr *mm;
1212
1213 (void) mul;
1214 (void) bve;
1215 (void) eidx;
1216
1217 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1218 {
1219 #ifndef NDEBUG
1220 BTOR_PROP_SOLVER (btor)->stats.cons_mul++;
1221 #endif
1222 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1223 }
1224
1225 mm = btor->mm;
1226 bw = btor_bv_get_width (bvmul);
1227 res = btor_bv_new_random (mm, &btor->rng, bw);
1228 if (!btor_bv_is_zero (bvmul))
1229 {
1230 if (btor_bv_is_zero (res))
1231 {
1232 btor_bv_free (mm, res);
1233 res = btor_bv_new_random (mm, &btor->rng, bw);
1234 }
1235 /* bvmul odd -> choose odd value > 0 */
1236 if (btor_bv_get_bit (bvmul, 0))
1237 {
1238 if (!btor_bv_get_bit (res, 0)) btor_bv_set_bit (res, 0, 1);
1239 }
1240 /* bvmul even -> choose random value > 0
1241 * with number of 0-LSBs in res less or equal
1242 * than in bvmul */
1243 else
1244 {
1245 ctz_bvmul = btor_bv_get_num_trailing_zeros (bvmul);
1246 /* choose res as 2^n with ctz(bvmul) >= ctz(res) with prob 0.1 */
1247 if (btor_rng_pick_with_prob (&btor->rng, 100))
1248 {
1249 btor_bv_free (mm, res);
1250 res = btor_bv_new (mm, bw);
1251 btor_bv_set_bit (
1252 res, btor_rng_pick_rand (&btor->rng, 0, ctz_bvmul - 1), 1);
1253 }
1254 /* choose res as bvmul / 2^n with prob 0.1
1255 * (note: bw not necessarily power of 2 -> do not use srl) */
1256 else if (btor_rng_pick_with_prob (&btor->rng, 100))
1257 {
1258 btor_bv_free (mm, res);
1259 if ((r = btor_rng_pick_rand (&btor->rng, 0, ctz_bvmul)))
1260 {
1261 tmp = btor_bv_slice (mm, bvmul, bw - 1, r);
1262 res = btor_bv_uext (mm, tmp, r);
1263 btor_bv_free (mm, tmp);
1264 }
1265 else
1266 {
1267 res = btor_bv_copy (mm, bvmul);
1268 }
1269 }
1270 /* choose random value with ctz(bvmul) >= ctz(res) with prob 0.8 */
1271 else
1272 {
1273 ctz_res = btor_bv_get_num_trailing_zeros (res);
1274 if (ctz_res > ctz_bvmul)
1275 btor_bv_set_bit (
1276 res, btor_rng_pick_rand (&btor->rng, 0, ctz_bvmul - 1), 1);
1277 }
1278 }
1279 }
1280
1281 return res;
1282 }
1283
1284 static BtorBitVector *
cons_udiv_bv(Btor * btor,BtorNode * udiv,BtorBitVector * bvudiv,BtorBitVector * bve,int32_t eidx)1285 cons_udiv_bv (Btor *btor,
1286 BtorNode *udiv,
1287 BtorBitVector *bvudiv,
1288 BtorBitVector *bve,
1289 int32_t eidx)
1290 {
1291 assert (btor);
1292 assert (udiv);
1293 assert (btor_node_is_regular (udiv));
1294 assert (bvudiv);
1295 assert (bve);
1296 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvudiv));
1297 assert (eidx >= 0 && eidx <= 1);
1298 assert (!btor_node_is_bv_const (udiv->e[eidx]));
1299
1300 uint32_t bw;
1301 BtorBitVector *res, *tmp, *tmpbve, *zero, *one, *bvmax;
1302 BtorMemMgr *mm;
1303
1304 mm = btor->mm;
1305 bw = btor_bv_get_width (bvudiv);
1306 zero = btor_bv_new (mm, bw);
1307 one = btor_bv_one (mm, bw);
1308 bvmax = btor_bv_ones (mm, bw);
1309
1310 (void) udiv;
1311 (void) bve;
1312
1313 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1314 {
1315 #ifndef NDEBUG
1316 BTOR_PROP_SOLVER (btor)->stats.cons_udiv++;
1317 #endif
1318 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1319 }
1320
1321 if (eidx)
1322 {
1323 /* -> bvudiv = 1...1 then res = 0 or res = 1
1324 * -> else choose res s.t. res * bvudiv does not overflow */
1325 if (!btor_bv_compare (bvudiv, bvmax))
1326 res =
1327 btor_bv_uint64_to_bv (mm, btor_rng_pick_rand (&btor->rng, 0, 1), bw);
1328 else
1329 {
1330 res = btor_bv_new_random_range (mm, &btor->rng, bw, one, bvmax);
1331 while (btor_bv_is_umulo (mm, res, bvudiv))
1332 {
1333 tmp = btor_bv_sub (mm, res, one);
1334 btor_bv_free (mm, res);
1335 res = btor_bv_new_random_range (mm, &btor->rng, bw, one, tmp);
1336 btor_bv_free (mm, tmp);
1337 }
1338 }
1339 }
1340 else
1341 {
1342 /* -> bvudiv = 0 then res < 1...1
1343 * -> bvudiv = 1...1 then choose random res
1344 * -> else choose tmpbve s.t. res = tmpbve * bvudiv does not overflow */
1345 if (btor_bv_is_zero (bvudiv))
1346 {
1347 tmp = btor_bv_dec (mm, bvmax);
1348 res = btor_bv_new_random_range (mm, &btor->rng, bw, zero, tmp);
1349 btor_bv_free (mm, tmp);
1350 }
1351 else if (!btor_bv_compare (bvudiv, bvmax))
1352 {
1353 res = btor_bv_new_random (mm, &btor->rng, bw);
1354 }
1355 else
1356 {
1357 tmpbve = btor_bv_new_random_range (mm, &btor->rng, bw, one, bvmax);
1358 while (btor_bv_is_umulo (mm, tmpbve, bvudiv))
1359 {
1360 tmp = btor_bv_sub (mm, tmpbve, one);
1361 btor_bv_free (mm, tmpbve);
1362 tmpbve = btor_bv_new_random_range (mm, &btor->rng, bw, one, tmp);
1363 btor_bv_free (mm, tmp);
1364 }
1365 res = btor_bv_mul (mm, tmpbve, bvudiv);
1366 btor_bv_free (mm, tmpbve);
1367 }
1368 }
1369
1370 btor_bv_free (mm, one);
1371 btor_bv_free (mm, zero);
1372 btor_bv_free (mm, bvmax);
1373 return res;
1374 }
1375
1376 static BtorBitVector *
cons_urem_bv(Btor * btor,BtorNode * urem,BtorBitVector * bvurem,BtorBitVector * bve,int32_t eidx)1377 cons_urem_bv (Btor *btor,
1378 BtorNode *urem,
1379 BtorBitVector *bvurem,
1380 BtorBitVector *bve,
1381 int32_t eidx)
1382 {
1383 assert (btor);
1384 assert (urem);
1385 assert (btor_node_is_regular (urem));
1386 assert (bvurem);
1387 assert (bve);
1388 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvurem));
1389 assert (eidx >= 0 && eidx <= 1);
1390 assert (!btor_node_is_bv_const (urem->e[eidx]));
1391
1392 uint32_t bw;
1393 BtorBitVector *res, *bvmax, *tmp;
1394 BtorMemMgr *mm;
1395
1396 (void) urem;
1397 (void) bve;
1398
1399 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1400 {
1401 #ifndef NDEBUG
1402 BTOR_PROP_SOLVER (btor)->stats.cons_urem++;
1403 #endif
1404 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1405 }
1406 mm = btor->mm;
1407 bw = btor_bv_get_width (bvurem);
1408 bvmax = btor_bv_ones (mm, bw);
1409
1410 if (eidx)
1411 {
1412 /* bvurem = 1...1 -> res = 0 */
1413 if (!btor_bv_compare (bvurem, bvmax))
1414 {
1415 res = btor_bv_new (mm, bw);
1416 }
1417 /* else res > bvurem */
1418 else
1419 {
1420 tmp = btor_bv_inc (mm, bvurem);
1421 res = btor_bv_new_random_range (mm, &btor->rng, bw, tmp, bvmax);
1422 btor_bv_free (mm, tmp);
1423 }
1424 }
1425 else
1426 {
1427 /* bvurem = 1...1 -> res = 1...1 */
1428 if (!btor_bv_compare (bvurem, bvmax))
1429 {
1430 res = btor_bv_copy (mm, bvmax);
1431 }
1432 /* else res >= bvurem */
1433 else
1434 {
1435 res = btor_bv_new_random_range (mm, &btor->rng, bw, bvurem, bvmax);
1436 }
1437 }
1438
1439 btor_bv_free (mm, bvmax);
1440 return res;
1441 }
1442
1443 static BtorBitVector *
cons_concat_bv(Btor * btor,BtorNode * concat,BtorBitVector * bvconcat,BtorBitVector * bve,int32_t eidx)1444 cons_concat_bv (Btor *btor,
1445 BtorNode *concat,
1446 BtorBitVector *bvconcat,
1447 BtorBitVector *bve,
1448 int32_t eidx)
1449 {
1450 assert (btor);
1451 assert (concat);
1452 assert (btor_node_is_regular (concat));
1453 assert (bvconcat);
1454 assert (bve);
1455 assert (eidx >= 0 && eidx <= 1);
1456 assert (!btor_node_is_bv_const (concat->e[eidx]));
1457
1458 int32_t idx, bw_t, bw_s;
1459 uint32_t r;
1460 BtorBitVector *res;
1461 const BtorBitVector *bvcur;
1462
1463 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1464 {
1465 #ifndef NDEBUG
1466 BTOR_PROP_SOLVER (btor)->stats.cons_concat++;
1467 #endif
1468 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1469 }
1470
1471 idx = eidx ? 0 : 1;
1472 bw_t = btor_bv_get_width (bvconcat);
1473 bw_s = btor_bv_get_width (bve);
1474
1475 /* If one operand is const, with BTOR_OPT_CONC_FLIP_PROB
1476 * either slice bits out of current assignment and flip max. one bit
1477 * randomly, or slice bits out of given assignment 'bve'. */
1478
1479 if (btor_node_is_bv_const (concat->e[idx])
1480 && btor_rng_pick_with_prob (
1481 &btor->rng, btor_opt_get (btor, BTOR_OPT_PROP_PROB_CONC_FLIP)))
1482 {
1483 bvcur = btor_model_get_bv (btor, concat);
1484 res = eidx ? btor_bv_slice (btor->mm, bvcur, bw_t - bw_s - 1, 0)
1485 : btor_bv_slice (btor->mm, bvcur, bw_t - 1, bw_s);
1486 r = btor_rng_pick_rand (&btor->rng, 0, btor_bv_get_width (res));
1487 if (r) btor_bv_flip_bit (res, r - 1);
1488 }
1489 else
1490 {
1491 res = eidx ? btor_bv_slice (btor->mm, bvconcat, bw_t - bw_s - 1, 0)
1492 : btor_bv_slice (btor->mm, bvconcat, bw_t - 1, bw_s);
1493 }
1494 return res;
1495 }
1496
1497 static BtorBitVector *
cons_slice_bv(Btor * btor,BtorNode * slice,BtorBitVector * bvslice,BtorBitVector * bve,int32_t eidx)1498 cons_slice_bv (Btor *btor,
1499 BtorNode *slice,
1500 BtorBitVector *bvslice,
1501 BtorBitVector *bve,
1502 int32_t eidx)
1503 {
1504 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1505 {
1506 #ifndef NDEBUG
1507 BTOR_PROP_SOLVER (btor)->stats.cons_slice++;
1508 #endif
1509 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1510 }
1511 return inv_slice_bv (btor, slice, bvslice, bve, eidx);
1512 }
1513
1514 static BtorBitVector *
cons_cond_bv(Btor * btor,BtorNode * cond,BtorBitVector * bvcond,BtorBitVector * bve,int32_t eidx)1515 cons_cond_bv (Btor *btor,
1516 BtorNode *cond,
1517 BtorBitVector *bvcond,
1518 BtorBitVector *bve,
1519 int32_t eidx)
1520 {
1521 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1522 {
1523 #ifndef NDEBUG
1524 BTOR_PROP_SOLVER (btor)->stats.cons_cond++;
1525 #endif
1526 BTOR_PROP_SOLVER (btor)->stats.props_cons += 1;
1527 }
1528 return inv_cond_bv (btor, cond, bvcond, bve, eidx);
1529 }
1530
1531 /* ========================================================================== */
1532 /* Inverse value computation */
1533 /* ========================================================================== */
1534
1535 static BtorBitVector *
res_rec_conf(Btor * btor,BtorNode * exp,BtorNode * e,BtorBitVector * bvexp,BtorBitVector * bve,int32_t eidx,BtorBitVector * (* fun)(Btor *,BtorNode *,BtorBitVector *,BtorBitVector *,int32_t),char * op)1536 res_rec_conf (Btor *btor,
1537 BtorNode *exp,
1538 BtorNode *e,
1539 BtorBitVector *bvexp,
1540 BtorBitVector *bve,
1541 int32_t eidx,
1542 BtorBitVector *(*fun) (Btor *,
1543 BtorNode *,
1544 BtorBitVector *,
1545 BtorBitVector *,
1546 int32_t),
1547 char *op)
1548 {
1549 assert (btor);
1550 assert (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP
1551 || btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_SLS);
1552 assert (exp);
1553 assert (btor_node_is_regular (exp));
1554 assert (e);
1555 assert (bvexp);
1556 assert (bve);
1557 assert (op);
1558 (void) op;
1559 (void) e;
1560
1561 bool is_recoverable = btor_node_is_bv_const (e) ? false : true;
1562 BtorBitVector *res =
1563 btor_opt_get (btor, BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT) && !is_recoverable
1564 ? 0
1565 : fun (btor, exp, bvexp, bve, eidx);
1566 assert (btor_opt_get (btor, BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT) || res);
1567
1568 #ifndef NDEBUG
1569 char *sbve = btor_bv_to_char (btor->mm, bve);
1570 char *sbvexp = btor_bv_to_char (btor->mm, bvexp);
1571 BTORLOG (2, "");
1572 if (eidx)
1573 BTORLOG (2,
1574 "%s CONFLICT (@%d): %s := %s %s x",
1575 is_recoverable ? "recoverable" : "non-recoverable",
1576 btor_node_get_id (exp),
1577 sbvexp,
1578 sbve,
1579 op);
1580 else
1581 BTORLOG (2,
1582 "%s CONFLICT (@%d): %s := x %s %s",
1583 is_recoverable ? "recoverable" : "non-recoverable",
1584 btor_node_get_id (exp),
1585 sbvexp,
1586 op,
1587 sbve);
1588 btor_mem_freestr (btor->mm, sbve);
1589 btor_mem_freestr (btor->mm, sbvexp);
1590 #endif
1591 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1592 {
1593 #ifndef NDEBUG
1594 /* fix counters since we always increase the counter, even in the conflict
1595 * case */
1596 switch (exp->kind)
1597 {
1598 case BTOR_BV_ADD_NODE: BTOR_PROP_SOLVER (btor)->stats.inv_add -= 1; break;
1599 case BTOR_BV_AND_NODE: BTOR_PROP_SOLVER (btor)->stats.inv_and -= 1; break;
1600 case BTOR_BV_EQ_NODE: BTOR_PROP_SOLVER (btor)->stats.inv_eq -= 1; break;
1601 case BTOR_BV_ULT_NODE: BTOR_PROP_SOLVER (btor)->stats.inv_ult -= 1; break;
1602 case BTOR_BV_SLL_NODE: BTOR_PROP_SOLVER (btor)->stats.inv_sll -= 1; break;
1603 case BTOR_BV_SRL_NODE: BTOR_PROP_SOLVER (btor)->stats.inv_srl -= 1; break;
1604 case BTOR_BV_MUL_NODE: BTOR_PROP_SOLVER (btor)->stats.inv_mul -= 1; break;
1605 case BTOR_BV_UDIV_NODE:
1606 BTOR_PROP_SOLVER (btor)->stats.inv_udiv -= 1;
1607 break;
1608 case BTOR_BV_UREM_NODE:
1609 BTOR_PROP_SOLVER (btor)->stats.inv_urem -= 1;
1610 break;
1611 case BTOR_BV_CONCAT_NODE:
1612 BTOR_PROP_SOLVER (btor)->stats.inv_concat -= 1;
1613 break;
1614 case BTOR_BV_SLICE_NODE:
1615 BTOR_PROP_SOLVER (btor)->stats.inv_slice -= 1;
1616 break;
1617 default:
1618 assert (btor_node_is_bv_cond (exp));
1619 /* do not decrease, we do not call cons function in conflict case */
1620 }
1621 #endif
1622 if (is_recoverable)
1623 BTOR_PROP_SOLVER (btor)->stats.rec_conf += 1;
1624 else
1625 BTOR_PROP_SOLVER (btor)->stats.non_rec_conf += 1;
1626 /* fix counter since we always increase the counter, even in the conflict
1627 * case */
1628 BTOR_PROP_SOLVER (btor)->stats.props_inv -= 1;
1629 }
1630 else
1631 {
1632 if (is_recoverable)
1633 BTOR_SLS_SOLVER (btor)->stats.move_prop_rec_conf += 1;
1634 else
1635 BTOR_SLS_SOLVER (btor)->stats.move_prop_non_rec_conf += 1;
1636 }
1637
1638 return res;
1639 }
1640
1641 /*------------------------------------------------------------------------*/
1642
1643 #ifndef NDEBUG
1644 static void
check_result_binary_dbg(Btor * btor,BtorBitVector * (* fun)(BtorMemMgr *,const BtorBitVector *,const BtorBitVector *),BtorNode * exp,BtorBitVector * bve,BtorBitVector * bvexp,BtorBitVector * res,int32_t eidx,char * op)1645 check_result_binary_dbg (Btor *btor,
1646 BtorBitVector *(*fun) (BtorMemMgr *,
1647 const BtorBitVector *,
1648 const BtorBitVector *),
1649 BtorNode *exp,
1650 BtorBitVector *bve,
1651 BtorBitVector *bvexp,
1652 BtorBitVector *res,
1653 int32_t eidx,
1654 char *op)
1655 {
1656 assert (btor);
1657 assert (fun);
1658 assert (exp);
1659 assert (bve);
1660 assert (bvexp);
1661 assert (res);
1662 assert (op);
1663
1664 (void) exp;
1665 (void) op;
1666
1667 BtorBitVector *tmp;
1668 char *sbve, *sbvexp, *sres;
1669
1670 tmp = eidx ? fun (btor->mm, bve, res) : fun (btor->mm, res, bve);
1671 assert (!btor_bv_compare (tmp, bvexp));
1672 sbvexp = btor_bv_to_char (btor->mm, bvexp);
1673 sbve = btor_bv_to_char (btor->mm, bve);
1674 sres = btor_bv_to_char (btor->mm, res);
1675 BTORLOG (3,
1676 "prop (e[%d]): %s: %s := %s %s %s",
1677 eidx,
1678 btor_util_node2string (exp),
1679 sbvexp,
1680 eidx ? sbve : sres,
1681 op,
1682 eidx ? sres : sbve);
1683 btor_bv_free (btor->mm, tmp);
1684 btor_mem_freestr (btor->mm, sbvexp);
1685 btor_mem_freestr (btor->mm, sbve);
1686 btor_mem_freestr (btor->mm, sres);
1687 }
1688 #endif
1689
1690 /* -------------------------------------------------------------------------- */
1691 /* INV: and */
1692 /* -------------------------------------------------------------------------- */
1693 #ifdef NDEBUG
1694 static BtorBitVector *
1695 #else
1696 BtorBitVector *
1697 #endif
inv_add_bv(Btor * btor,BtorNode * add,BtorBitVector * bvadd,BtorBitVector * bve,int32_t eidx)1698 inv_add_bv (Btor *btor,
1699 BtorNode *add,
1700 BtorBitVector *bvadd,
1701 BtorBitVector *bve,
1702 int32_t eidx)
1703 {
1704 assert (btor);
1705 assert (add);
1706 assert (btor_node_is_regular (add));
1707 assert (bvadd);
1708 assert (bve);
1709 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvadd));
1710 assert (eidx >= 0 && eidx <= 1);
1711 assert (!btor_node_is_bv_const (add->e[eidx]));
1712
1713 BtorBitVector *res;
1714
1715 (void) add;
1716 (void) eidx;
1717
1718 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1719 {
1720 #ifndef NDEBUG
1721 BTOR_PROP_SOLVER (btor)->stats.inv_add++;
1722 #endif
1723 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
1724 }
1725
1726 /* res + bve = bve + res = bvadd -> res = bvadd - bve */
1727 res = btor_bv_sub (btor->mm, bvadd, bve);
1728 #ifndef NDEBUG
1729 check_result_binary_dbg (btor, btor_bv_add, add, bve, bvadd, res, eidx, "+");
1730 #endif
1731 return res;
1732 }
1733
1734 #ifdef NDEBUG
1735 static BtorBitVector *
1736 #else
1737 BtorBitVector *
1738 #endif
inv_and_bv(Btor * btor,BtorNode * and,BtorBitVector * bvand,BtorBitVector * bve,int32_t eidx)1739 inv_and_bv (Btor *btor,
1740 BtorNode *and,
1741 BtorBitVector *bvand,
1742 BtorBitVector *bve,
1743 int32_t eidx)
1744 {
1745 assert (btor);
1746 assert (and);
1747 assert (btor_node_is_regular (and));
1748 assert (bvand);
1749 assert (bve);
1750 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvand));
1751 assert (eidx >= 0 && eidx <= 1);
1752 assert (!btor_node_is_bv_const (and->e[eidx]));
1753
1754 uint32_t i, bw;
1755 int32_t bitand, bite;
1756 BtorNode *e;
1757 BtorBitVector *res;
1758 BtorMemMgr *mm;
1759 BtorUIntStack dcbits;
1760 bool b;
1761
1762 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1763 {
1764 #ifndef NDEBUG
1765 BTOR_PROP_SOLVER (btor)->stats.inv_and++;
1766 #endif
1767 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
1768 }
1769
1770 mm = btor->mm;
1771 e = and->e[eidx ? 0 : 1];
1772 assert (e);
1773
1774 b = btor_rng_pick_with_prob (
1775 &btor->rng, btor_opt_get (btor, BTOR_OPT_PROP_PROB_AND_FLIP));
1776 BTOR_INIT_STACK (mm, dcbits);
1777
1778 res = btor_bv_copy (mm, btor_model_get_bv (btor, and->e[eidx]));
1779 assert (res);
1780
1781 for (i = 0, bw = btor_bv_get_width (bvand); i < bw; i++)
1782 {
1783 bitand = btor_bv_get_bit (bvand, i);
1784 bite = btor_bv_get_bit (bve, i);
1785
1786 if (bitand&&!bite)
1787 {
1788 /* CONFLICT: all bits set in bvand, must be set in bve ---------------- */
1789 btor_bv_free (mm, res);
1790 res = res_rec_conf (btor, and, e, bvand, bve, eidx, cons_and_bv, "AND");
1791 goto DONE;
1792 }
1793
1794 /* ----------------------------------------------------------------------
1795 * res & bve = bve & res = bvand
1796 *
1797 * -> all bits set in bvand and bve must be set in res
1798 * -> all bits not set in bvand but set in bve must not be set in res
1799 * -> all bits not set in bve can be chosen to be set randomly
1800 * ---------------------------------------------------------------------- */
1801 if (bitand)
1802 btor_bv_set_bit (res, i, 1);
1803 else if (bite)
1804 btor_bv_set_bit (res, i, 0);
1805 else if (b)
1806 BTOR_PUSH_STACK (dcbits, i);
1807 else
1808 btor_bv_set_bit (res, i, btor_rng_pick_rand (&btor->rng, 0, 1));
1809 }
1810
1811 if (b && BTOR_COUNT_STACK (dcbits))
1812 btor_bv_flip_bit (
1813 res,
1814 BTOR_PEEK_STACK (
1815 dcbits,
1816 btor_rng_pick_rand (&btor->rng, 0, BTOR_COUNT_STACK (dcbits) - 1)));
1817
1818 #ifndef NDEBUG
1819 check_result_binary_dbg (
1820 btor, btor_bv_and, and, bve, bvand, res, eidx, "AND");
1821 #endif
1822
1823 DONE:
1824 BTOR_RELEASE_STACK (dcbits);
1825 return res;
1826 }
1827
1828 /* -------------------------------------------------------------------------- */
1829 /* INV: eq */
1830 /* -------------------------------------------------------------------------- */
1831 #ifdef NDEBUG
1832 static BtorBitVector *
1833 #else
1834 BtorBitVector *
1835 #endif
inv_eq_bv(Btor * btor,BtorNode * eq,BtorBitVector * bveq,BtorBitVector * bve,int32_t eidx)1836 inv_eq_bv (Btor *btor,
1837 BtorNode *eq,
1838 BtorBitVector *bveq,
1839 BtorBitVector *bve,
1840 int32_t eidx)
1841 {
1842 assert (btor);
1843 assert (eq);
1844 assert (btor_node_is_regular (eq));
1845 assert (bveq);
1846 assert (btor_bv_get_width (bveq) == 1);
1847 assert (bve);
1848 assert (eidx >= 0 && eidx <= 1);
1849 assert (!btor_node_is_bv_const (eq->e[eidx]));
1850
1851 BtorBitVector *res;
1852 BtorMemMgr *mm;
1853
1854 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1855 {
1856 #ifndef NDEBUG
1857 BTOR_PROP_SOLVER (btor)->stats.inv_eq++;
1858 #endif
1859 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
1860 }
1861
1862 mm = btor->mm;
1863
1864 if (btor_bv_is_zero (bveq))
1865 {
1866 /* res != bveq -> choose random res != bveq ----------------------------- */
1867 if (btor_rng_pick_with_prob (
1868 &btor->rng, btor_opt_get (btor, BTOR_OPT_PROP_PROB_EQ_FLIP)))
1869 {
1870 res = 0;
1871 do
1872 {
1873 if (res) btor_bv_free (btor->mm, res);
1874 res = btor_bv_copy (btor->mm, btor_model_get_bv (btor, eq->e[eidx]));
1875 btor_bv_flip_bit (
1876 res,
1877 btor_rng_pick_rand (&btor->rng, 0, btor_bv_get_width (res) - 1));
1878 } while (!btor_bv_compare (res, bve));
1879 }
1880 else
1881 {
1882 res = 0;
1883 do
1884 {
1885 if (res) btor_bv_free (mm, res);
1886 res = btor_bv_new_random (mm, &btor->rng, btor_bv_get_width (bve));
1887 } while (!btor_bv_compare (res, bve));
1888 }
1889 }
1890 else
1891 {
1892 /* res = bveq ----------------------------------------------------------- */
1893 res = btor_bv_copy (mm, bve);
1894 }
1895
1896 #ifndef NDEBUG
1897 check_result_binary_dbg (btor, btor_bv_eq, eq, bve, bveq, res, eidx, "=");
1898 #endif
1899 return res;
1900 }
1901
1902 /* -------------------------------------------------------------------------- */
1903 /* INV: ult */
1904 /* -------------------------------------------------------------------------- */
1905 #ifdef NDEBUG
1906 static BtorBitVector *
1907 #else
1908 BtorBitVector *
1909 #endif
inv_ult_bv(Btor * btor,BtorNode * ult,BtorBitVector * bvult,BtorBitVector * bve,int32_t eidx)1910 inv_ult_bv (Btor *btor,
1911 BtorNode *ult,
1912 BtorBitVector *bvult,
1913 BtorBitVector *bve,
1914 int32_t eidx)
1915 {
1916 assert (btor);
1917 assert (ult);
1918 assert (btor_node_is_regular (ult));
1919 assert (bvult);
1920 assert (btor_bv_get_width (bvult) == 1);
1921 assert (bve);
1922 assert (eidx >= 0 && eidx <= 1);
1923 assert (!btor_node_is_bv_const (ult->e[eidx]));
1924
1925 bool isult;
1926 uint32_t bw;
1927 BtorNode *e;
1928 BtorBitVector *res, *zero, *one, *bvmax, *tmp;
1929 BtorMemMgr *mm;
1930 #ifndef NDEBUG
1931 bool is_inv = true;
1932 #endif
1933
1934 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
1935 {
1936 #ifndef NDEBUG
1937 BTOR_PROP_SOLVER (btor)->stats.inv_ult++;
1938 #endif
1939 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
1940 }
1941
1942 mm = btor->mm;
1943 e = ult->e[eidx ? 0 : 1];
1944 assert (e);
1945
1946 bw = btor_bv_get_width (bve);
1947 zero = btor_bv_new (mm, bw);
1948 one = btor_bv_one (mm, bw);
1949 bvmax = btor_bv_ones (mm, bw);
1950 isult = !btor_bv_is_zero (bvult);
1951
1952 res = 0;
1953
1954 if (eidx)
1955 {
1956 if (!btor_bv_compare (bve, bvmax) && isult)
1957 {
1958 BVULT_CONF:
1959 /* CONFLICT: 1...1 < e[1] --------------------------------------------- */
1960 res = res_rec_conf (btor, ult, e, bvult, bve, eidx, cons_ult_bv, "<");
1961 #ifndef NDEBUG
1962 is_inv = false;
1963 #endif
1964 }
1965 else
1966 {
1967 if (!isult)
1968 {
1969 /* bve >= e[1] ------------------------------------------------------ */
1970 res = btor_bv_new_random_range (mm, &btor->rng, bw, zero, bve);
1971 }
1972 else
1973 {
1974 /* bve < e[1] ------------------------------------------------------- */
1975 tmp = btor_bv_add (mm, bve, one);
1976 res = btor_bv_new_random_range (mm, &btor->rng, bw, tmp, bvmax);
1977 btor_bv_free (mm, tmp);
1978 }
1979 }
1980 }
1981 else
1982 {
1983 if (btor_bv_is_zero (bve) && isult)
1984 {
1985 /* CONFLICT: e[0] < 0 ------------------------------------------------- */
1986 goto BVULT_CONF;
1987 }
1988 else
1989 {
1990 if (!isult)
1991 {
1992 /* e[0] >= bve ------------------------------------------------------ */
1993 res = btor_bv_new_random_range (mm, &btor->rng, bw, bve, bvmax);
1994 }
1995 else
1996 {
1997 /* e[0] < bve ------------------------------------------------------- */
1998 tmp = btor_bv_sub (mm, bve, one);
1999 res = btor_bv_new_random_range (mm, &btor->rng, bw, zero, tmp);
2000 btor_bv_free (mm, tmp);
2001 }
2002 }
2003 }
2004
2005 #ifndef NDEBUG
2006 if (is_inv)
2007 check_result_binary_dbg (
2008 btor, btor_bv_ult, ult, bve, bvult, res, eidx, "<");
2009 #endif
2010 btor_bv_free (mm, zero);
2011 btor_bv_free (mm, one);
2012 btor_bv_free (mm, bvmax);
2013 return res;
2014 }
2015
2016 /* -------------------------------------------------------------------------- */
2017 /* INV: sll */
2018 /* -------------------------------------------------------------------------- */
2019 #ifdef NDEBUG
2020 static BtorBitVector *
2021 #else
2022 BtorBitVector *
2023 #endif
inv_sll_bv(Btor * btor,BtorNode * sll,BtorBitVector * bvsll,BtorBitVector * bve,int32_t eidx)2024 inv_sll_bv (Btor *btor,
2025 BtorNode *sll,
2026 BtorBitVector *bvsll,
2027 BtorBitVector *bve,
2028 int32_t eidx)
2029 {
2030 assert (btor);
2031 assert (sll);
2032 assert (btor_node_is_regular (sll));
2033 assert (bvsll);
2034 assert (bve);
2035 assert (eidx >= 0 && eidx <= 1);
2036 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvsll));
2037 assert (!btor_node_is_bv_const (sll->e[eidx]));
2038
2039 uint32_t i, j, ctz_bve, ctz_bvsll, shift, bw;
2040 BtorNode *e;
2041 BtorBitVector *res, *tmp, *bvmax;
2042 BtorMemMgr *mm;
2043 #ifndef NDEBUG
2044 bool is_inv = true;
2045 #endif
2046
2047 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
2048 {
2049 #ifndef NDEBUG
2050 BTOR_PROP_SOLVER (btor)->stats.inv_sll++;
2051 #endif
2052 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
2053 }
2054
2055 mm = btor->mm;
2056 e = sll->e[eidx ? 0 : 1];
2057 assert (e);
2058 bw = btor_bv_get_width (bvsll);
2059
2060 res = 0;
2061 bw = btor_bv_get_width (bvsll);
2062 ctz_bvsll = btor_bv_get_num_trailing_zeros (bvsll);
2063
2064 /* ------------------------------------------------------------------------
2065 * bve << e[1] = bvsll
2066 *
2067 * -> identify possible shift value via zero LSB in bvsll
2068 * (considering zero LSB in bve)
2069 * ------------------------------------------------------------------------ */
2070 if (eidx)
2071 {
2072 if (btor_bv_is_zero (bve) && btor_bv_is_zero (bvsll))
2073 {
2074 /* 0...0 << e[1] = 0...0 -> choose res randomly ----------------------- */
2075 res = btor_bv_new_random (mm, &btor->rng, bw);
2076 }
2077 else
2078 {
2079 /* -> ctz(bve) > ctz (bvsll) -> conflict
2080 * -> shift = ctz(bvsll) - ctz(bve)
2081 * -> if bvsll = 0 choose shift <= res < bw
2082 * -> else res = shift
2083 * + if all remaining shifted bits match
2084 * -> else conflict
2085 * -------------------------------------------------------------------- */
2086 ctz_bve = btor_bv_get_num_trailing_zeros (bve);
2087 if (ctz_bve <= ctz_bvsll)
2088 {
2089 shift = ctz_bvsll - ctz_bve;
2090
2091 if (btor_bv_is_zero (bvsll))
2092 {
2093 /* x...x0 << e[1] = 0...0
2094 * -> choose random shift <= res < 2^bw
2095 * ---------------------------------------------------------------- */
2096 bvmax = btor_bv_ones (mm, bw);
2097 tmp = btor_bv_uint64_to_bv (mm, (uint64_t) shift, bw);
2098 res = btor_bv_new_random_range (mm, &btor->rng, bw, tmp, bvmax);
2099 btor_bv_free (mm, bvmax);
2100 btor_bv_free (mm, tmp);
2101 }
2102 else
2103 {
2104 for (i = 0, j = shift, res = 0; i < bw - j; i++)
2105 {
2106 /* CONFLICT: shifted bits must match ---------------------------- */
2107 if (btor_bv_get_bit (bve, i) != btor_bv_get_bit (bvsll, j + i))
2108 goto BVSLL_CONF;
2109 }
2110
2111 res = btor_bv_uint64_to_bv (mm, (uint64_t) shift, bw);
2112 }
2113 }
2114 else
2115 {
2116 BVSLL_CONF:
2117 res = res_rec_conf (btor, sll, e, bvsll, bve, eidx, cons_sll_bv, "<<");
2118 #ifndef NDEBUG
2119 is_inv = false;
2120 #endif
2121 }
2122 }
2123 }
2124 /* ------------------------------------------------------------------------
2125 * e[0] << bve = bvsll
2126 *
2127 * -> e[0] = bvsll >> bve
2128 * set irrelevant MSBs (the ones that get shifted out) randomly
2129 * ------------------------------------------------------------------------ */
2130 else
2131 {
2132 /* actual value is small enough to fit into 32 bit (max bit width handled
2133 * by Boolector is INT32_MAX) */
2134 if (bw > 64)
2135 {
2136 tmp = btor_bv_slice (mm, bve, 32, 0);
2137 shift = btor_bv_to_uint64 (tmp);
2138 btor_bv_free (mm, tmp);
2139 }
2140 else
2141 {
2142 shift = btor_bv_to_uint64 (bve);
2143 }
2144
2145 if ((shift < bw && ctz_bvsll < shift) || (shift >= bw && ctz_bvsll != bw))
2146 {
2147 /* CONFLICT: the LSBs shifted must be zero ---------------------------- */
2148 goto BVSLL_CONF;
2149 }
2150
2151 res = btor_bv_srl (mm, bvsll, bve);
2152 for (i = 0; i < shift && i < bw; i++)
2153 {
2154 btor_bv_set_bit (res,
2155 btor_bv_get_width (res) - 1 - i,
2156 btor_rng_pick_rand (&btor->rng, 0, 1));
2157 }
2158 }
2159 #ifndef NDEBUG
2160 if (is_inv)
2161 check_result_binary_dbg (
2162 btor, btor_bv_sll, sll, bve, bvsll, res, eidx, "<<");
2163 #endif
2164 return res;
2165 }
2166
2167 /* -------------------------------------------------------------------------- */
2168 /* INV: srl */
2169 /* -------------------------------------------------------------------------- */
2170 #ifdef NDEBUG
2171 static BtorBitVector *
2172 #else
2173 BtorBitVector *
2174 #endif
inv_srl_bv(Btor * btor,BtorNode * srl,BtorBitVector * bvsrl,BtorBitVector * bve,int32_t eidx)2175 inv_srl_bv (Btor *btor,
2176 BtorNode *srl,
2177 BtorBitVector *bvsrl,
2178 BtorBitVector *bve,
2179 int32_t eidx)
2180 {
2181 assert (btor);
2182 assert (srl);
2183 assert (btor_node_is_regular (srl));
2184 assert (bvsrl);
2185 assert (bve);
2186 assert (eidx >= 0 && eidx <= 1);
2187 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvsrl));
2188 assert (!btor_node_is_bv_const (srl->e[eidx]));
2189
2190 uint32_t i, j, clz_bve, clz_bvsrl, shift, bw;
2191 BtorNode *e;
2192 BtorBitVector *res, *bvmax, *tmp;
2193 BtorMemMgr *mm;
2194 #ifndef NDEBUG
2195 bool is_inv = true;
2196 #endif
2197
2198 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
2199 {
2200 #ifndef NDEBUG
2201 BTOR_PROP_SOLVER (btor)->stats.inv_srl++;
2202 #endif
2203 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
2204 }
2205
2206 mm = btor->mm;
2207 e = srl->e[eidx ? 0 : 1];
2208 assert (e);
2209 bw = btor_bv_get_width (bvsrl);
2210
2211 res = 0;
2212 bw = btor_bv_get_width (bvsrl);
2213 clz_bvsrl = btor_bv_get_num_leading_zeros (bvsrl);
2214
2215 /* ------------------------------------------------------------------------
2216 * bve >> e[1] = bvsll
2217 *
2218 * -> identify possible shift value via zero MSBs in bvsll
2219 * (considering zero MSBs in bve)
2220 * ------------------------------------------------------------------------ */
2221 if (eidx)
2222 {
2223 if (btor_bv_is_zero (bve) && btor_bv_is_zero (bvsrl))
2224 {
2225 /* 0...0 >> e[1] = 0...0 -> choose random res ------------------------- */
2226 res = btor_bv_new_random (mm, &btor->rng, bw);
2227 }
2228 else
2229 {
2230 /* clz(bve) > clz(bvsrl) -> conflict
2231 *
2232 * -> shift = clz(bvsrl) - clz(bve)
2233 * -> if bvsrl = 0 choose shift <= res < bw
2234 * -> else res = shift
2235 * + if all remaining shifted bits match
2236 * -> else conflict
2237 * -------------------------------------------------------------------- */
2238 clz_bve = btor_bv_get_num_leading_zeros (bve);
2239 if (clz_bve <= clz_bvsrl)
2240 {
2241 shift = clz_bvsrl - clz_bve;
2242
2243 if (btor_bv_is_zero (bvsrl))
2244 {
2245 /* x...x0 >> e[1] = 0...0
2246 * -> choose random shift <= res < 2^bw
2247 * ---------------------------------------------------------------- */
2248 bvmax = btor_bv_ones (mm, bw);
2249 tmp = btor_bv_uint64_to_bv (mm, (uint64_t) shift, bw);
2250 res = btor_bv_new_random_range (mm, &btor->rng, bw, tmp, bvmax);
2251 btor_bv_free (mm, bvmax);
2252 btor_bv_free (mm, tmp);
2253 }
2254 else
2255 {
2256 for (i = 0, j = shift, res = 0; i < bw - j; i++)
2257 {
2258 if (btor_bv_get_bit (bve, bw - 1 - i)
2259 != btor_bv_get_bit (bvsrl, bw - 1 - (j + i)))
2260 {
2261 /* CONFLICT: shifted bits must match -------------------------- */
2262 goto BVSRL_CONF;
2263 }
2264 }
2265
2266 res = btor_bv_uint64_to_bv (mm, (uint64_t) shift, bw);
2267 }
2268 }
2269 else
2270 {
2271 BVSRL_CONF:
2272 res = res_rec_conf (btor, srl, e, bvsrl, bve, eidx, cons_srl_bv, ">>");
2273 #ifndef NDEBUG
2274 is_inv = false;
2275 #endif
2276 }
2277 }
2278 }
2279 /* ------------------------------------------------------------------------
2280 * e[0] >> bve = bvsll
2281 *
2282 * -> e[0] = bvsll << bve
2283 * set irrelevant LSBs (the ones that get shifted out) randomly
2284 * ------------------------------------------------------------------------ */
2285 else
2286 {
2287 /* actual value is small enough to fit into 32 bit (max bit width handled
2288 * by Boolector is INT32_MAX) */
2289 if (bw > 64)
2290 {
2291 tmp = btor_bv_slice (mm, bve, 32, 0);
2292 shift = btor_bv_to_uint64 (tmp);
2293 btor_bv_free (mm, tmp);
2294 }
2295 else
2296 {
2297 shift = btor_bv_to_uint64 (bve);
2298 }
2299
2300 if ((shift < bw && clz_bvsrl < shift) || (shift >= bw && clz_bvsrl != bw))
2301 {
2302 /* CONFLICT: the MSBs shifted must be zero ---------------------------- */
2303 goto BVSRL_CONF;
2304 }
2305
2306 res = btor_bv_sll (mm, bvsrl, bve);
2307 for (i = 0; i < shift && i < bw; i++)
2308 {
2309 btor_bv_set_bit (res, i, btor_rng_pick_rand (&btor->rng, 0, 1));
2310 }
2311 }
2312
2313 #ifndef NDEBUG
2314 if (is_inv)
2315 check_result_binary_dbg (
2316 btor, btor_bv_srl, srl, bve, bvsrl, res, eidx, ">>");
2317 #endif
2318 return res;
2319 }
2320
2321 /* -------------------------------------------------------------------------- */
2322 /* INV: mul */
2323 /* -------------------------------------------------------------------------- */
2324 #ifdef NDEBUG
2325 static BtorBitVector *
2326 #else
2327 BtorBitVector *
2328 #endif
inv_mul_bv(Btor * btor,BtorNode * mul,BtorBitVector * bvmul,BtorBitVector * bve,int32_t eidx)2329 inv_mul_bv (Btor *btor,
2330 BtorNode *mul,
2331 BtorBitVector *bvmul,
2332 BtorBitVector *bve,
2333 int32_t eidx)
2334 {
2335 assert (btor);
2336 assert (mul);
2337 assert (btor_node_is_regular (mul));
2338 assert (bvmul);
2339 assert (bve);
2340 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvmul));
2341 assert (eidx >= 0 && eidx <= 1);
2342 assert (!btor_node_is_bv_const (mul->e[eidx]));
2343
2344 int32_t lsbve, lsbvmul, ispow2_bve;
2345 uint32_t i, j, bw;
2346 BtorBitVector *res, *inv, *tmp, *tmp2;
2347 BtorMemMgr *mm;
2348 BtorNode *e;
2349 #ifndef NDEBUG
2350 bool is_inv = true;
2351 #endif
2352
2353 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
2354 {
2355 #ifndef NDEBUG
2356 BTOR_PROP_SOLVER (btor)->stats.inv_mul++;
2357 #endif
2358 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
2359 }
2360
2361 mm = btor->mm;
2362 e = mul->e[eidx ? 0 : 1];
2363 assert (e);
2364 bw = btor_bv_get_width (bvmul);
2365
2366 res = 0;
2367
2368 /* ------------------------------------------------------------------------
2369 * bve * res = bvmul
2370 *
2371 * -> if bve = 0: * bvmul = 0 -> choose random value for res
2372 * * bvmul > 0 -> conflict
2373 *
2374 * -> if bvmul odd and bve even -> conflict
2375 *
2376 * -> if bve odd -> determine res via modular inverse (extended euklid)
2377 * (unique solution)
2378 *
2379 * -> else if bve is even (non-unique, multiple solutions possible!)
2380 * * bve = 2^n: + if number of 0-LSBs in bvmul < n -> conflict
2381 * + else res = bvmul >> n
2382 * (with all bits shifted in randomly set to 0 or 1)
2383 * * else: bve = 2^n * m, m is odd
2384 * + if number of 0-LSBs in bvmul < n -> conflict
2385 * + else c' = bvmul >> n
2386 * (with all bits shifted in randomly set to 0 or 1)
2387 * -> res = c' * m^-1 (with m^-1 the mod inverse of m, m odd)
2388 * ------------------------------------------------------------------------ */
2389
2390 lsbve = btor_bv_get_bit (bve, 0);
2391 lsbvmul = btor_bv_get_bit (bvmul, 0);
2392
2393 if (btor_bv_is_zero (bve))
2394 {
2395 /* bve = 0 -> if bvmul = 0 choose random value, else conflict ----------- */
2396 if (btor_bv_is_zero (bvmul))
2397 {
2398 res = btor_bv_new_random (mm, &btor->rng, bw);
2399 }
2400 else
2401 {
2402 BVMUL_CONF:
2403 /* CONFLICT: bve = 0 but bvmul != 0 ----------------------------------- */
2404 res = res_rec_conf (btor, mul, e, bvmul, bve, eidx, cons_mul_bv, "*");
2405 #ifndef NDEBUG
2406 is_inv = false;
2407 #endif
2408 }
2409 }
2410 else if (lsbvmul && !lsbve)
2411 {
2412 /* CONFLICT: bvmul odd and bve is even ---------------------------------- */
2413 goto BVMUL_CONF;
2414 }
2415 else
2416 {
2417 /* ----------------------------------------------------------------------
2418 * bve odd
2419 *
2420 * -> determine res via modular inverse (extended euklid)
2421 * (unique solution)
2422 * ---------------------------------------------------------------------- */
2423 if (lsbve)
2424 {
2425 inv = btor_bv_mod_inverse (mm, bve);
2426 res = btor_bv_mul (mm, inv, bvmul);
2427 btor_bv_free (mm, inv);
2428 }
2429 /* ----------------------------------------------------------------------
2430 * bve even
2431 * (non-unique, multiple solutions possible!)
2432 *
2433 * if bve = 2^n: + if number of 0-LSBs in bvmul < n -> conflict
2434 * + else res = bvmul >> n
2435 * (with all bits shifted in set randomly)
2436 * else: bve = 2^n * m, m is odd
2437 * + if number of 0-LSBs in bvmul < n -> conflict
2438 * + else c' = bvmul >> n (with all bits shifted in set randomly)
2439 * res = c' * m^-1 (with m^-1 the mod inverse of m)
2440 * ---------------------------------------------------------------------- */
2441 else
2442 {
2443 if ((ispow2_bve = btor_bv_power_of_two (bve)) >= 0)
2444 {
2445 for (i = 0; i < bw; i++)
2446 if (btor_bv_get_bit (bvmul, i)) break;
2447 if (i < (uint32_t) ispow2_bve)
2448 {
2449 /* CONFLICT: number of 0-LSBs in bvmul < n (for bve = 2^n) -------- */
2450 goto BVMUL_CONF;
2451 }
2452 else
2453 {
2454 /* res = bvmul >> n with all bits shifted in set randomly
2455 * (note: bw is not necessarily power of 2 -> do not use srl)
2456 * ---------------------------------------------------------------- */
2457 tmp = btor_bv_slice (mm, bvmul, bw - 1, ispow2_bve);
2458 res = btor_bv_uext (mm, tmp, ispow2_bve);
2459 assert (btor_bv_get_width (res) == bw);
2460 for (i = 0; i < (uint32_t) ispow2_bve; i++)
2461 btor_bv_set_bit (
2462 res, bw - 1 - i, btor_rng_pick_rand (&btor->rng, 0, 1));
2463 btor_bv_free (mm, tmp);
2464 }
2465 }
2466 else
2467 {
2468 for (i = 0; i < bw; i++)
2469 if (btor_bv_get_bit (bvmul, i)) break;
2470 for (j = 0; j < bw; j++)
2471 if (btor_bv_get_bit (bve, j)) break;
2472 if (i < j)
2473 {
2474 /* CONFLICT: number of 0-LSB in bvmul < number of 0-LSB in bve ---- */
2475 goto BVMUL_CONF;
2476 }
2477 else
2478 {
2479 /* c' = bvmul >> n (with all bits shifted in set randomly)
2480 * (note: bw is not necessarily power of 2 -> do not use srl)
2481 * -> res = c' * m^-1 (with m^-1 the mod inverse of m, m odd)
2482 * ---------------------------------------------------------------- */
2483 tmp = btor_bv_slice (mm, bvmul, bw - 1, j);
2484 res = btor_bv_uext (mm, tmp, j);
2485 assert (btor_bv_get_width (res) == bw);
2486 btor_bv_free (mm, tmp);
2487
2488 tmp = btor_bv_slice (mm, bve, bw - 1, j);
2489 tmp2 = btor_bv_uext (mm, tmp, j);
2490 assert (btor_bv_get_width (tmp2) == bw);
2491 assert (btor_bv_get_bit (tmp2, 0));
2492 inv = btor_bv_mod_inverse (mm, tmp2);
2493 btor_bv_free (mm, tmp);
2494 btor_bv_free (mm, tmp2);
2495 tmp = res;
2496 res = btor_bv_mul (mm, tmp, inv);
2497 /* choose one of all possible values */
2498 for (i = 0; i < j; i++)
2499 btor_bv_set_bit (
2500 res, bw - 1 - i, btor_rng_pick_rand (&btor->rng, 0, 1));
2501 btor_bv_free (mm, tmp);
2502 btor_bv_free (mm, inv);
2503 }
2504 }
2505 }
2506 }
2507
2508 #ifndef NDEBUG
2509 if (is_inv)
2510 check_result_binary_dbg (
2511 btor, btor_bv_mul, mul, bve, bvmul, res, eidx, "*");
2512 #endif
2513 return res;
2514 }
2515
2516 /* -------------------------------------------------------------------------- */
2517 /* INV: udiv */
2518 /* -------------------------------------------------------------------------- */
2519 #ifdef NDEBUG
2520 static BtorBitVector *
2521 #else
2522 BtorBitVector *
2523 #endif
inv_udiv_bv(Btor * btor,BtorNode * udiv,BtorBitVector * bvudiv,BtorBitVector * bve,int32_t eidx)2524 inv_udiv_bv (Btor *btor,
2525 BtorNode *udiv,
2526 BtorBitVector *bvudiv,
2527 BtorBitVector *bve,
2528 int32_t eidx)
2529 {
2530 assert (btor);
2531 assert (udiv);
2532 assert (btor_node_is_regular (udiv));
2533 assert (bvudiv);
2534 assert (bve);
2535 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvudiv));
2536 assert (eidx >= 0 && eidx <= 1);
2537 assert (!btor_node_is_bv_const (udiv->e[eidx]));
2538
2539 uint32_t bw;
2540 BtorNode *e;
2541 BtorBitVector *res, *lo, *up, *one, *bvmax, *tmp;
2542 BtorMemMgr *mm;
2543 BtorRNG *rng;
2544 #ifndef NDEBUG
2545 bool is_inv = true;
2546 #endif
2547
2548 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
2549 {
2550 #ifndef NDEBUG
2551 BTOR_PROP_SOLVER (btor)->stats.inv_udiv++;
2552 #endif
2553 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
2554 }
2555
2556 mm = btor->mm;
2557 rng = &btor->rng;
2558 e = udiv->e[eidx ? 0 : 1];
2559 assert (e);
2560 bw = btor_bv_get_width (bve);
2561
2562 one = btor_bv_one (mm, bw);
2563 bvmax = btor_bv_ones (mm, bw); /* 2^bw - 1 */
2564
2565 res = 0;
2566
2567 /* ------------------------------------------------------------------------
2568 * bve / e[1] = bvudiv
2569 *
2570 * -> if bvudiv = 2^bw - 1: + bve = bvudiv = 2^bw - 1 -> e[1] = 1 or e[1] = 0
2571 * + bve != bvudiv -> e[1] = 0
2572 * -> if bvudiv = 0 and 0 < bve < 2^bw - 1 choose random e[1] > bve
2573 * and bve = 0 choose random e[1] > 0
2574 * else conflict
2575 * -> if bve < bvudiv -> conflict
2576 * -> if bvudiv is a divisor of bve choose with 0.5 prob out of
2577 * + e[1] = bvudiv / bve
2578 * + choose bve s.t. bve / e[1] = bvudiv
2579 * -> else choose bve s.t. bve / e[1] = bvudiv
2580 * ------------------------------------------------------------------------ */
2581 if (eidx)
2582 {
2583 if (!btor_bv_compare (bvudiv, bvmax))
2584 {
2585 if (!btor_bv_compare (bve, bvudiv)
2586 && btor_rng_pick_with_prob (&btor->rng, 500))
2587 {
2588 /* bve = bvudiv = 2^bw - 1 -> choose either e[1] = 0 or e[1] = 1
2589 * with prob 0.5
2590 * ------------------------------------------------------------------ */
2591 res = btor_bv_one (mm, bw);
2592 }
2593 else
2594 {
2595 /* bvudiv = 2^bw - 1 and bve != bvudiv -> e[1] = 0 ------------------ */
2596 res = btor_bv_new (mm, bw);
2597 }
2598 }
2599 else if (btor_bv_is_zero (bvudiv))
2600 {
2601 if (btor_bv_is_zero (bve))
2602 {
2603 /* bvudiv = 0 and bve = 0 -> choose random e[1] > 0 ----------------- */
2604 res = btor_bv_new_random_range (mm, rng, bw, one, bvmax);
2605 }
2606 else if (btor_bv_compare (bve, bvmax))
2607 {
2608 /* bvudiv = 0 and 0 < bve < 2^bw - 1 -> choose random e[1] > bve ---- */
2609 tmp = btor_bv_inc (mm, bve);
2610 res = btor_bv_new_random_range (mm, rng, bw, tmp, bvmax);
2611 btor_bv_free (mm, tmp);
2612 }
2613 else
2614 {
2615 BVUDIV_CONF:
2616 /* CONFLICT --------------------------------------------------------- */
2617 res =
2618 res_rec_conf (btor, udiv, e, bvudiv, bve, eidx, cons_udiv_bv, "/");
2619 #ifndef NDEBUG
2620 is_inv = false;
2621 #endif
2622 }
2623 }
2624 else if (btor_bv_compare (bve, bvudiv) < 0)
2625 {
2626 /* CONFLICT: bve < bvudiv --------------------------------------------- */
2627 goto BVUDIV_CONF;
2628 }
2629 else
2630 {
2631 /* if bvudiv is a divisor of bve, choose e[1] = bve / bvudiv
2632 * with prob = 0.5 and a bve s.t. bve / e[1] = bvudiv otherwise
2633 * -------------------------------------------------------------------- */
2634 tmp = btor_bv_urem (mm, bve, bvudiv);
2635 if (btor_bv_is_zero (tmp) && btor_rng_pick_with_prob (rng, 500))
2636 {
2637 btor_bv_free (mm, tmp);
2638 res = btor_bv_udiv (mm, bve, bvudiv);
2639 }
2640 else
2641 {
2642 /* choose e[1] out of all options that yield bve / e[1] = bvudiv
2643 * Note: udiv always truncates the results towards 0.
2644 * ------------------------------------------------------------------ */
2645
2646 /* determine upper and lower bounds for e[1]:
2647 * up = bve / bvudiv
2648 * lo = bve / (bvudiv + 1) + 1
2649 * if lo > up -> conflict */
2650 btor_bv_free (mm, tmp);
2651 up = btor_bv_udiv (mm, bve, bvudiv); /* upper bound */
2652 tmp = btor_bv_inc (mm, bvudiv);
2653 lo = btor_bv_udiv (mm, bve, tmp); /* lower bound (excl.) */
2654 btor_bv_free (mm, tmp);
2655 tmp = lo;
2656 lo = btor_bv_inc (mm, tmp); /* lower bound (incl.) */
2657 btor_bv_free (mm, tmp);
2658
2659 if (btor_bv_compare (lo, up) > 0)
2660 {
2661 /* CONFLICT: lo > up ---------------------------------------------- */
2662 btor_bv_free (mm, lo);
2663 btor_bv_free (mm, up);
2664 goto BVUDIV_CONF;
2665 }
2666 else
2667 {
2668 /* choose lo <= e[1] <= up ---------------------------------------- */
2669 res = btor_bv_new_random_range (mm, rng, bw, lo, up);
2670 btor_bv_free (mm, lo);
2671 btor_bv_free (mm, up);
2672 }
2673 }
2674 }
2675 }
2676
2677 /* ------------------------------------------------------------------------
2678 * e[0] / bve = bvudiv
2679 *
2680 * -> if bvudiv = 2^bw - 1 and bve = 1 e[0] = 2^bw-1
2681 * and bve = 0, choose random e[0] > 0
2682 * and bve > 0 -> conflict
2683 * -> if bve = 0 and bvudiv < 2^bw - 1 -> conflict
2684 * -> if bve * bvudiv does not overflow, choose with 0.5 prob out of
2685 * + e[0] = bve * bvudiv
2686 * + choose bve s.t. e[0] / bve = bvudiv
2687 * -> else choose bve s.t. e[0] / bve = bvudiv
2688 * ------------------------------------------------------------------------ */
2689 else
2690 {
2691 if (!btor_bv_compare (bvudiv, bvmax))
2692 {
2693 if (!btor_bv_compare (bve, one))
2694 {
2695 /* bvudiv = 2^bw-1 and bve = 1 -> e[0] = 2^bw-1 --------------------- */
2696 res = btor_bv_copy (mm, bvmax);
2697 }
2698 else if (btor_bv_is_zero (bve))
2699 {
2700 /* bvudiv = 2^bw - 1 and bve = 0 -> choose random e[0] -------------- */
2701 res = btor_bv_new_random (mm, rng, bw);
2702 }
2703 else
2704 {
2705 /* CONFLICT --------------------------------------------------------- */
2706 goto BVUDIV_CONF;
2707 }
2708 }
2709 else if (btor_bv_is_zero (bve))
2710 {
2711 /* CONFLICT: bve = 0 and bvudiv < 2^bw - 1 ---------------------------- */
2712 goto BVUDIV_CONF;
2713 }
2714 else
2715 {
2716 /* if bve * bvudiv does not overflow, choose e[0] = bve * bvudiv
2717 * with prob = 0.5 and a bve s.t. e[0] / bve = bvudiv otherwise */
2718
2719 if (btor_bv_is_umulo (mm, bve, bvudiv))
2720 {
2721 /* CONFLICT: overflow: bve * bvudiv --------------------------------- */
2722 goto BVUDIV_CONF;
2723 }
2724 else
2725 {
2726 if (btor_rng_pick_with_prob (rng, 500))
2727 res = btor_bv_mul (mm, bve, bvudiv);
2728 else
2729 {
2730 /* choose e[0] out of all options that yield
2731 * e[0] / bve = bvudiv
2732 * Note: udiv always truncates the results towards 0.
2733 * ---------------------------------------------------------------- */
2734
2735 /* determine upper and lower bounds for e[0]:
2736 * up = bve * (budiv + 1) - 1
2737 * if bve * (bvudiv + 1) does not overflow
2738 * else 2^bw - 1
2739 * lo = bve * bvudiv */
2740 lo = btor_bv_mul (mm, bve, bvudiv);
2741 tmp = btor_bv_inc (mm, bvudiv);
2742 if (btor_bv_is_umulo (mm, bve, tmp))
2743 {
2744 btor_bv_free (mm, tmp);
2745 up = btor_bv_copy (mm, bvmax);
2746 }
2747 else
2748 {
2749 up = btor_bv_mul (mm, bve, tmp);
2750 btor_bv_free (mm, tmp);
2751 tmp = btor_bv_dec (mm, up);
2752 btor_bv_free (mm, up);
2753 up = tmp;
2754 }
2755
2756 res = btor_bv_new_random_range (mm, &btor->rng, bw, lo, up);
2757
2758 btor_bv_free (mm, up);
2759 btor_bv_free (mm, lo);
2760 }
2761 }
2762 }
2763 }
2764
2765 btor_bv_free (mm, bvmax);
2766 btor_bv_free (mm, one);
2767 #ifndef NDEBUG
2768 if (is_inv)
2769 check_result_binary_dbg (
2770 btor, btor_bv_udiv, udiv, bve, bvudiv, res, eidx, "/");
2771 #endif
2772 return res;
2773 }
2774
2775 /* -------------------------------------------------------------------------- */
2776 /* INV: urem */
2777 /* -------------------------------------------------------------------------- */
2778 #ifdef NDEBUG
2779 static BtorBitVector *
2780 #else
2781 BtorBitVector *
2782 #endif
inv_urem_bv(Btor * btor,BtorNode * urem,BtorBitVector * bvurem,BtorBitVector * bve,int32_t eidx)2783 inv_urem_bv (Btor *btor,
2784 BtorNode *urem,
2785 BtorBitVector *bvurem,
2786 BtorBitVector *bve,
2787 int32_t eidx)
2788 {
2789 assert (btor);
2790 assert (urem);
2791 assert (btor_node_is_regular (urem));
2792 assert (bvurem);
2793 assert (bve);
2794 assert (btor_bv_get_width (bve) == btor_bv_get_width (bvurem));
2795 assert (eidx >= 0 && eidx <= 1);
2796 assert (!btor_node_is_bv_const (urem->e[eidx]));
2797
2798 uint32_t bw, cnt;
2799 int32_t cmp;
2800 BtorNode *e;
2801 BtorBitVector *res, *bvmax, *tmp, *tmp2, *one, *n, *mul, *up, *sub;
2802 BtorMemMgr *mm;
2803 #ifndef NDEBUG
2804 bool is_inv = true;
2805 #endif
2806
2807 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
2808 {
2809 #ifndef NDEBUG
2810 BTOR_PROP_SOLVER (btor)->stats.inv_urem++;
2811 #endif
2812 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
2813 }
2814
2815 mm = btor->mm;
2816 e = urem->e[eidx ? 0 : 1];
2817 assert (e);
2818
2819 bw = btor_bv_get_width (bvurem);
2820
2821 bvmax = btor_bv_ones (mm, bw); /* 2^bw - 1 */
2822 one = btor_bv_one (mm, bw);
2823
2824 res = 0;
2825
2826 /* -----------------------------------------------------------------------
2827 * bve % e[1] = bvurem
2828 *
2829 * -> if bvurem = 1...1 -> bve = 1...1 and e[1] = 0...0, else conflict
2830 * -> if bve = bvurem, choose either e[1] = 0 or some e[1] > bvurem randomly
2831 * -> if bvurem > 0 and bvurem = bve - 1, conflict
2832 * -> if bve > bvurem, e[1] = ((bve - bvurem) / n) > bvurem, else conflict
2833 * -> if bve < bvurem, conflict
2834 * ------------------------------------------------------------------------ */
2835 if (eidx)
2836 {
2837 if (!btor_bv_compare (bvurem, bvmax))
2838 {
2839 /* CONFLICT: bvurem = 1...1 but bve != 1...1 -------------------------- */
2840 if (btor_bv_compare (bve, bvmax))
2841 {
2842 BVUREM_CONF:
2843 res =
2844 res_rec_conf (btor, urem, e, bvurem, bve, eidx, cons_urem_bv, "%");
2845 #ifndef NDEBUG
2846 is_inv = false;
2847 #endif
2848 }
2849 else
2850 {
2851 /* bve % e[1] = 1...1 -> bve = 1...1, e[1] = 0 ---------------------- */
2852 res = btor_bv_new (mm, bw);
2853 }
2854 }
2855 else
2856 {
2857 cmp = btor_bv_compare (bve, bvurem);
2858
2859 if (cmp == 0)
2860 {
2861 /* bve = bvurem, choose either e[1] = 0 or random e[1] > bvurem ----- */
2862
2863 /* choose e[1] = 0 with prob = 0.25*/
2864 if (btor_rng_pick_with_prob (&btor->rng, 250))
2865 res = btor_bv_new (mm, bw);
2866 /* bvurem < res <= 2^bw - 1 */
2867 else
2868 {
2869 tmp = btor_bv_add (mm, bvurem, one);
2870 res = btor_bv_new_random_range (mm, &btor->rng, bw, tmp, bvmax);
2871 btor_bv_free (mm, tmp);
2872 }
2873 }
2874 else if (cmp > 0)
2875 {
2876 /* bve > bvurem, e[1] = (bve - bvurem) / n -------------------------- */
2877 if (!btor_bv_is_zero (bvurem))
2878 {
2879 tmp = btor_bv_dec (mm, bve);
2880 if (!btor_bv_compare (bvurem, tmp))
2881 {
2882 /* CONFLICT:
2883 * bvurem = bve - 1 -> bve % e[1] = bve - 1
2884 * -> not possible if bvurem > 0
2885 * -------------------------------------------------------------- */
2886 btor_bv_free (mm, tmp);
2887 goto BVUREM_CONF;
2888 }
2889 btor_bv_free (mm, tmp);
2890 }
2891
2892 sub = btor_bv_sub (mm, bve, bvurem);
2893
2894 if (btor_bv_compare (sub, bvurem) <= 0)
2895 {
2896 /* CONFLICT: bve - bvurem <= bvurem ------------------------------- */
2897 btor_bv_free (mm, sub);
2898 goto BVUREM_CONF;
2899 }
2900 else
2901 {
2902 /* choose either n = 1 or 1 <= n < (bve - bvurem) / bvurem
2903 * with prob = 0.5
2904 * ---------------------------------------------------------------- */
2905
2906 if (btor_rng_pick_with_prob (&btor->rng, 500))
2907 {
2908 res = btor_bv_copy (mm, sub);
2909 }
2910 else
2911 {
2912 /* 1 <= n < (bve - bvurem) / bvurem (non-truncating)
2913 * (note: div truncates towards 0!)
2914 * -------------------------------------------------------------- */
2915
2916 if (btor_bv_is_zero (bvurem))
2917 {
2918 /* bvurem = 0 -> 1 <= n <= bve -------------------------------- */
2919 up = btor_bv_copy (mm, bve);
2920 }
2921 else
2922 {
2923 /* e[1] > bvurem
2924 * -> (bve - bvurem) / n > bvurem
2925 * -> (bve - bvurem) / bvurem > n
2926 * ------------------------------------------------------------ */
2927 tmp = btor_bv_urem (mm, sub, bvurem);
2928 tmp2 = btor_bv_udiv (mm, sub, bvurem);
2929 if (btor_bv_is_zero (tmp))
2930 {
2931 /* (bve - bvurem) / bvurem is not truncated
2932 * (remainder is 0), therefore the EXclusive
2933 * upper bound
2934 * -> up = (bve - bvurem) / bvurem - 1
2935 * ---------------------------------------------------------- */
2936 up = btor_bv_sub (mm, tmp2, one);
2937 btor_bv_free (mm, tmp2);
2938 }
2939 else
2940 {
2941 /* (bve - bvurem) / bvurem is truncated
2942 * (remainder is not 0), therefore the INclusive
2943 * upper bound
2944 * -> up = (bve - bvurem) / bvurem
2945 * ---------------------------------------------------------- */
2946 up = tmp2;
2947 }
2948 btor_bv_free (mm, tmp);
2949 }
2950
2951 if (btor_bv_is_zero (up))
2952 res = btor_bv_udiv (mm, sub, one);
2953 else
2954 {
2955 /* choose 1 <= n <= up randomly
2956 * s.t (bve - bvurem) % n = 0
2957 * ------------------------------------------------------------ */
2958 n = btor_bv_new_random_range (mm, &btor->rng, bw, one, up);
2959 tmp = btor_bv_urem (mm, sub, n);
2960 for (cnt = 0; cnt < bw && !btor_bv_is_zero (tmp); cnt++)
2961 {
2962 btor_bv_free (mm, n);
2963 btor_bv_free (mm, tmp);
2964 n = btor_bv_new_random_range (mm, &btor->rng, bw, one, up);
2965 tmp = btor_bv_urem (mm, sub, n);
2966 }
2967
2968 if (btor_bv_is_zero (tmp))
2969 {
2970 /* res = (bve - bvurem) / n */
2971 res = btor_bv_udiv (mm, sub, n);
2972 }
2973 else
2974 {
2975 /* fallback: n = 1 */
2976 res = btor_bv_copy (mm, sub);
2977 }
2978
2979 btor_bv_free (mm, n);
2980 btor_bv_free (mm, tmp);
2981 }
2982 btor_bv_free (mm, up);
2983 }
2984 }
2985 btor_bv_free (mm, sub);
2986 }
2987 else
2988 {
2989 /* CONFLICT: bve < bvurem ------------------------------------------- */
2990 goto BVUREM_CONF;
2991 }
2992 }
2993 }
2994 /* ------------------------------------------------------------------------
2995 * e[0] % bve = bvurem
2996 *
2997 * -> if bve = 0, e[0] = bvurem
2998 * -> if bvurem = 1...1 and bve != 0, conflict
2999 * -> if bve <= bvurem, conflict
3000 * -> if bvurem > 0 and bve = 1, conflict
3001 * -> else choose either
3002 * - e[0] = bvurem, or
3003 * - e[0] = bve * n + b, with n s.t. (bve * n + b) does not overflow
3004 * ------------------------------------------------------------------------ */
3005 else
3006 {
3007 if (btor_bv_is_zero (bve))
3008 {
3009 BVUREM_ZERO_0:
3010 /* bve = 0 -> e[0] = bvurem ------------------------------------------- */
3011 res = btor_bv_copy (mm, bvurem);
3012 }
3013 else if (!btor_bv_is_zero (bvurem) && btor_bv_is_one (bve))
3014 {
3015 /* CONFLICT: bvurem > 0 and bve = 1 ----------------------------------- */
3016 goto BVUREM_CONF;
3017 }
3018 else if (!btor_bv_compare (bvurem, bvmax))
3019 {
3020 if (!btor_bv_is_zero (bve))
3021 {
3022 /* CONFLICT: bve != 0 ----------------------------------------------- */
3023 goto BVUREM_CONF;
3024 }
3025 else
3026 {
3027 /* bvurem = 1...1 -> bve = 0, e[0] = 1...1 -------------------------- */
3028 goto BVUREM_ZERO_0;
3029 }
3030 }
3031 else if (btor_bv_compare (bve, bvurem) > 0)
3032 {
3033 if (btor_rng_pick_with_prob (&btor->rng, 500))
3034 {
3035 BVUREM_EQ_0:
3036 /* choose simplest solution (0 <= res < bve -> res = bvurem)
3037 * with prob 0.5
3038 * ------------------------------------------------------------------ */
3039 res = btor_bv_copy (mm, bvurem);
3040 }
3041 else
3042 {
3043 /* e[0] = bve * n + bvurem,
3044 * with n s.t. (bve * n + bvurem) does not overflow
3045 * ------------------------------------------------------------------ */
3046 tmp2 = btor_bv_sub (mm, bvmax, bve);
3047
3048 /* overflow for n = 1 -> only simplest solution possible */
3049 if (btor_bv_compare (tmp2, bvurem) < 0)
3050 {
3051 btor_bv_free (mm, tmp2);
3052 goto BVUREM_EQ_0;
3053 }
3054 else
3055 {
3056 btor_bv_free (mm, tmp2);
3057
3058 tmp = btor_bv_copy (mm, bvmax);
3059 n = btor_bv_new_random_range (mm, &btor->rng, bw, one, tmp);
3060
3061 while (btor_bv_is_umulo (mm, bve, n))
3062 {
3063 btor_bv_free (mm, tmp);
3064 tmp = btor_bv_sub (mm, n, one);
3065 btor_bv_free (mm, n);
3066 n = btor_bv_new_random_range (mm, &btor->rng, bw, one, tmp);
3067 }
3068
3069 mul = btor_bv_mul (mm, bve, n);
3070 tmp2 = btor_bv_sub (mm, bvmax, mul);
3071
3072 if (btor_bv_compare (tmp2, bvurem) < 0)
3073 {
3074 btor_bv_free (mm, tmp);
3075 tmp = btor_bv_sub (mm, n, one);
3076 btor_bv_free (mm, n);
3077 n = btor_bv_new_random_range (mm, &btor->rng, bw, one, tmp);
3078 btor_bv_free (mm, mul);
3079 mul = btor_bv_mul (mm, bve, n);
3080 }
3081
3082 res = btor_bv_add (mm, mul, bvurem);
3083 assert (btor_bv_compare (res, mul) >= 0);
3084 assert (btor_bv_compare (res, bvurem) >= 0);
3085
3086 btor_bv_free (mm, tmp);
3087 btor_bv_free (mm, tmp2);
3088 btor_bv_free (mm, mul);
3089 btor_bv_free (mm, n);
3090 }
3091 }
3092 }
3093 else
3094 {
3095 /* CONFLICT: bve <= bvurem -------------------------------------------- */
3096 goto BVUREM_CONF;
3097 }
3098 }
3099
3100 btor_bv_free (mm, one);
3101 btor_bv_free (mm, bvmax);
3102
3103 #ifndef NDEBUG
3104 if (is_inv)
3105 check_result_binary_dbg (
3106 btor, btor_bv_urem, urem, bve, bvurem, res, eidx, "%");
3107 #endif
3108 return res;
3109 }
3110
3111 /* -------------------------------------------------------------------------- */
3112 /* INV: concat */
3113 /* -------------------------------------------------------------------------- */
3114 #ifdef NDEBUG
3115 static BtorBitVector *
3116 #else
3117 BtorBitVector *
3118 #endif
inv_concat_bv(Btor * btor,BtorNode * concat,BtorBitVector * bvconcat,BtorBitVector * bve,int32_t eidx)3119 inv_concat_bv (Btor *btor,
3120 BtorNode *concat,
3121 BtorBitVector *bvconcat,
3122 BtorBitVector *bve,
3123 int32_t eidx)
3124 {
3125 assert (btor);
3126 assert (concat);
3127 assert (btor_node_is_regular (concat));
3128 assert (bvconcat);
3129 assert (bve);
3130 assert (eidx >= 0 && eidx <= 1);
3131 assert (!btor_node_is_bv_const (concat->e[eidx]));
3132
3133 uint32_t bw_t, bw_s;
3134 BtorNode *e;
3135 BtorBitVector *res, *tmp;
3136 BtorMemMgr *mm;
3137 #ifndef NDEBUG
3138 bool is_inv = true;
3139 #endif
3140
3141 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
3142 {
3143 #ifndef NDEBUG
3144 BTOR_PROP_SOLVER (btor)->stats.inv_concat++;
3145 #endif
3146 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
3147 }
3148
3149 mm = btor->mm;
3150 e = concat->e[eidx ? 0 : 1];
3151 assert (e);
3152 bw_t = btor_bv_get_width (bvconcat);
3153 bw_s = btor_bv_get_width (bve);
3154
3155 res = 0;
3156
3157 /* ------------------------------------------------------------------------
3158 * bve o e[1] = bvconcat
3159 *
3160 * -> slice e[1] out of the lower bits of bvconcat
3161 * ------------------------------------------------------------------------ */
3162 if (eidx)
3163 {
3164 tmp = btor_bv_slice (mm, bvconcat, bw_t - 1, bw_t - bw_s);
3165 if (btor_bv_compare (tmp, bve))
3166 {
3167 BVCONCAT_CONF:
3168 /* CONFLICT: bve bits do not match bvconcat --------------------------- */
3169 res = res_rec_conf (
3170 btor, concat, e, bvconcat, bve, eidx, cons_concat_bv, "o");
3171 #ifndef NDEBUG
3172 is_inv = false;
3173 #endif
3174 }
3175 else
3176 {
3177 res = btor_bv_slice (mm, bvconcat, bw_t - bw_s - 1, 0);
3178 }
3179 }
3180 /* ------------------------------------------------------------------------
3181 * e[0] o bve = bvconcat
3182 *
3183 * -> slice e[0] out of the upper bits of bvconcat
3184 * ------------------------------------------------------------------------ */
3185 else
3186 {
3187 tmp = btor_bv_slice (mm, bvconcat, bw_s - 1, 0);
3188 if (btor_bv_compare (tmp, bve))
3189 {
3190 /* CONFLICT: bve bits do not match bvconcat --------------------------- */
3191 goto BVCONCAT_CONF;
3192 }
3193 else
3194 {
3195 res = btor_bv_slice (mm, bvconcat, bw_t - 1, bw_s);
3196 }
3197 }
3198 btor_bv_free (mm, tmp);
3199 #ifndef NDEBUG
3200 if (is_inv)
3201 check_result_binary_dbg (
3202 btor, btor_bv_concat, concat, bve, bvconcat, res, eidx, "o");
3203 #endif
3204 return res;
3205 }
3206
3207 /* -------------------------------------------------------------------------- */
3208 /* INV: slice */
3209 /* -------------------------------------------------------------------------- */
3210 #ifdef NDEBUG
3211 static BtorBitVector *
3212 #else
3213 BtorBitVector *
3214 #endif
inv_slice_bv(Btor * btor,BtorNode * slice,BtorBitVector * bvslice,BtorBitVector * bve,int32_t eidx)3215 inv_slice_bv (Btor *btor,
3216 BtorNode *slice,
3217 BtorBitVector *bvslice,
3218 BtorBitVector *bve,
3219 int32_t eidx)
3220 {
3221 assert (btor);
3222 assert (slice);
3223 assert (btor_node_is_regular (slice));
3224 assert (bvslice);
3225 assert (!btor_node_is_bv_const (slice->e[0]));
3226 (void) eidx;
3227
3228 uint32_t i, upper, lower, rlower, rupper, rboth, bw_x;
3229 BtorNode *e;
3230 BtorBitVector *res;
3231 BtorMemMgr *mm;
3232 bool bkeep, bflip;
3233
3234 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
3235 {
3236 #ifndef NDEBUG
3237 BTOR_PROP_SOLVER (btor)->stats.inv_slice++;
3238 #endif
3239 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
3240 }
3241
3242 mm = btor->mm;
3243 e = slice->e[0];
3244 assert (e);
3245
3246 bflip = btor_rng_pick_with_prob (
3247 &btor->rng, btor_opt_get (btor, BTOR_OPT_PROP_PROB_SLICE_FLIP));
3248
3249 bkeep = bflip ? true
3250 : btor_rng_pick_with_prob (
3251 &btor->rng,
3252 btor_opt_get (btor, BTOR_OPT_PROP_PROB_SLICE_KEEP_DC));
3253
3254 upper = btor_node_bv_slice_get_upper (slice);
3255 lower = btor_node_bv_slice_get_lower (slice);
3256
3257 res = btor_bv_new (mm, btor_node_bv_get_width (btor, e));
3258
3259 /* keep previous value for don't care bits or set randomly with prob
3260 * BTOR_OPT_PROP_PROB_SLICE_KEEP_DC */
3261 for (i = 0; i < lower; i++)
3262 btor_bv_set_bit (res,
3263 i,
3264 bkeep ? btor_bv_get_bit (bve, i)
3265 : btor_rng_pick_rand (&btor->rng, 0, 1));
3266
3267 /* set sliced bits to propagated value */
3268 for (i = lower; i <= upper; i++)
3269 btor_bv_set_bit (res, i, btor_bv_get_bit (bvslice, i - lower));
3270
3271 /* keep previous value for don't care bits or set randomly with prob
3272 * BTOR_OPT_PROP_PROB_SLICE_KEEP_DC */
3273 bw_x = btor_bv_get_width (res);
3274 for (i = upper + 1; i < bw_x; i++)
3275 btor_bv_set_bit (res,
3276 i,
3277 bkeep ? btor_bv_get_bit (bve, i)
3278 : btor_rng_pick_rand (&btor->rng, 0, 1));
3279
3280 if (bflip)
3281 {
3282 rboth = 0;
3283 rupper = bw_x - 1;
3284 rlower = 0;
3285
3286 if (lower)
3287 {
3288 rboth += 1;
3289 rlower = btor_rng_pick_rand (&btor->rng, 0, lower - 1);
3290 }
3291
3292 if (upper + 1 < bw_x)
3293 {
3294 rboth += 2;
3295 rupper = btor_rng_pick_rand (&btor->rng, upper + 1, bw_x - 1);
3296 }
3297
3298 switch (rboth)
3299 {
3300 case 3:
3301 assert (rupper >= upper + 1 && rupper < bw_x);
3302 assert (rlower < lower);
3303 btor_bv_flip_bit (
3304 res, btor_rng_pick_with_prob (&btor->rng, 500) ? rupper : rlower);
3305 break;
3306 case 2:
3307 assert (rupper >= upper + 1 && rupper < bw_x);
3308 btor_bv_flip_bit (res, rupper);
3309 break;
3310 case 1:
3311 assert (rlower < lower);
3312 btor_bv_flip_bit (res, rlower);
3313 break;
3314 }
3315 }
3316
3317 #ifndef NDEBUG
3318 BtorBitVector *tmpdbg = btor_bv_slice (mm, res, upper, lower);
3319 assert (!btor_bv_compare (tmpdbg, bvslice));
3320 btor_bv_free (mm, tmpdbg);
3321
3322 char *sbvslice = btor_bv_to_char (mm, bvslice);
3323 char *sres = btor_bv_to_char (mm, res);
3324 BTORLOG (3,
3325 "prop (xxxxx): %s: %s := %s[%d:%d]",
3326 btor_util_node2string (slice),
3327 sbvslice,
3328 sres,
3329 lower,
3330 upper);
3331 btor_mem_freestr (mm, sbvslice);
3332 btor_mem_freestr (mm, sres);
3333 #endif
3334 return res;
3335 }
3336
3337 /* -------------------------------------------------------------------------- */
3338 /* INV: cond */
3339 /* -------------------------------------------------------------------------- */
3340 #ifdef NDEBUG
3341 static BtorBitVector *
3342 #else
3343 BtorBitVector *
3344 #endif
inv_cond_bv(Btor * btor,BtorNode * cond,BtorBitVector * bvcond,BtorBitVector * bve,int32_t eidx)3345 inv_cond_bv (Btor *btor,
3346 BtorNode *cond,
3347 BtorBitVector *bvcond,
3348 BtorBitVector *bve,
3349 int32_t eidx)
3350 {
3351 assert (btor);
3352 assert (cond);
3353 assert (btor_node_is_regular (cond));
3354 assert (bvcond);
3355 assert (!btor_bv_compare (bve, btor_model_get_bv (btor, cond->e[0])));
3356 assert (eidx || !btor_node_is_bv_const (cond->e[eidx]));
3357
3358 BtorBitVector *res, *bve1, *bve2;
3359 BtorMemMgr *mm = btor->mm;
3360
3361 bve1 = (BtorBitVector *) btor_model_get_bv (btor, cond->e[1]);
3362 bve2 = (BtorBitVector *) btor_model_get_bv (btor, cond->e[2]);
3363 #ifndef NDEBUG
3364 char *sbvcond = btor_bv_to_char (btor->mm, bvcond);
3365 char *sbve0 = btor_bv_to_char (mm, bve);
3366 char *sbve1 = btor_bv_to_char (mm, bve1);
3367 char *sbve2 = btor_bv_to_char (mm, bve2);
3368 #endif
3369
3370 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
3371 {
3372 #ifndef NDEBUG
3373 BTOR_PROP_SOLVER (btor)->stats.inv_cond++;
3374 #endif
3375 BTOR_PROP_SOLVER (btor)->stats.props_inv += 1;
3376 }
3377
3378 /* either assume that cond is fixed and propagate bvenew
3379 * to enabled path, or flip condition */
3380
3381 if (eidx == 0)
3382 {
3383 /* flip condition */
3384 res = btor_bv_not (mm, bve);
3385 }
3386 else
3387 {
3388 /* else continue propagating current target value down */
3389 res = btor_bv_copy (mm, bvcond);
3390 if (btor_node_is_bv_const (cond->e[eidx]))
3391 {
3392 bool is_recoverable = !btor_bv_compare (bvcond, eidx == 1 ? bve2 : bve1);
3393 #ifndef NDEBUG
3394 if (eidx == 2)
3395 {
3396 BTORLOG (2,
3397 "%s CONFLICT (@%d): %s := %s ? %s : x",
3398 is_recoverable ? "recoverable" : "non-recoverable",
3399 btor_node_get_id (cond),
3400 sbvcond,
3401 sbve0,
3402 sbve1);
3403 }
3404 else
3405 {
3406 BTORLOG (2,
3407 "%s CONFLICT (@%d): %s := %s ? x : %s",
3408 is_recoverable ? "recoverable" : "non-recoverable",
3409 btor_node_get_id (cond),
3410 sbvcond,
3411 sbve0,
3412 sbve2);
3413 }
3414 BTORLOG (2, "");
3415 #endif
3416 if (btor_opt_get (btor, BTOR_OPT_ENGINE) == BTOR_ENGINE_PROP)
3417 {
3418 if (is_recoverable)
3419 BTOR_PROP_SOLVER (btor)->stats.rec_conf += 1;
3420 else
3421 BTOR_PROP_SOLVER (btor)->stats.non_rec_conf += 1;
3422 }
3423 else
3424 {
3425 if (is_recoverable)
3426 BTOR_SLS_SOLVER (btor)->stats.move_prop_rec_conf += 1;
3427 else
3428 BTOR_SLS_SOLVER (btor)->stats.move_prop_non_rec_conf += 1;
3429 }
3430 }
3431 }
3432
3433 #ifndef NDEBUG
3434 char *sres = btor_bv_to_char (mm, res);
3435 BTORLOG (3,
3436 "prop (e[%d]): %s: %s := %s ? %s : %s",
3437 eidx,
3438 btor_util_node2string (cond),
3439 sbvcond,
3440 eidx == 0 ? sres : sbve0,
3441 eidx == 1 ? sres : sbve1,
3442 eidx == 2 ? sres : sbve2);
3443 btor_mem_freestr (mm, sbvcond);
3444 btor_mem_freestr (mm, sres);
3445 btor_mem_freestr (mm, sbve0);
3446 btor_mem_freestr (mm, sbve1);
3447 btor_mem_freestr (mm, sbve2);
3448 #endif
3449 return res;
3450 }
3451
3452 /* ========================================================================== */
3453 /* Propagation move */
3454 /* ========================================================================== */
3455
3456 static BtorNode *
select_move(Btor * btor,BtorNode * exp,BtorBitVector * bvexp,BtorBitVector * bve[3],int32_t (* select_path)(Btor *,BtorNode *,BtorBitVector *,BtorBitVector **),BtorBitVector * (* compute_value)(Btor *,BtorNode *,BtorBitVector *,BtorBitVector *,int32_t),BtorBitVector ** value)3457 select_move (Btor *btor,
3458 BtorNode *exp,
3459 BtorBitVector *bvexp,
3460 BtorBitVector *bve[3],
3461 int32_t (*select_path) (
3462 Btor *, BtorNode *, BtorBitVector *, BtorBitVector **),
3463 BtorBitVector *(*compute_value) (
3464 Btor *, BtorNode *, BtorBitVector *, BtorBitVector *, int32_t),
3465 BtorBitVector **value)
3466 {
3467 assert (btor);
3468 assert (exp);
3469 assert (btor_node_is_regular (exp));
3470 assert (bvexp);
3471 assert (bve);
3472 assert (select_path);
3473 assert (compute_value);
3474 assert (value);
3475
3476 int32_t eidx, idx;
3477
3478 eidx = select_path (btor, exp, bvexp, bve);
3479 assert (eidx >= 0);
3480 /* special case slice: only one child
3481 * special case cond: we only need assignment of condition to compute value */
3482 idx = eidx ? 0
3483 : (btor_node_is_bv_slice (exp) || btor_node_is_cond (exp) ? 0 : 1);
3484 *value = compute_value (btor, exp, bvexp, bve[idx], eidx);
3485 return exp->e[eidx];
3486 }
3487
3488 uint64_t
btor_proputils_select_move_prop(Btor * btor,BtorNode * root,BtorNode ** input,BtorBitVector ** assignment)3489 btor_proputils_select_move_prop (Btor *btor,
3490 BtorNode *root,
3491 BtorNode **input,
3492 BtorBitVector **assignment)
3493 {
3494 assert (btor);
3495 assert (root);
3496 assert (btor_bv_to_uint64 ((BtorBitVector *) btor_model_get_bv (btor, root))
3497 == 0);
3498
3499 bool b;
3500 int32_t i, nconst;
3501 uint64_t nprops;
3502 BtorNode *cur, *real_cur;
3503 BtorBitVector *bve[3], *bvcur, *bvenew, *tmp;
3504 int32_t (*select_path) (
3505 Btor *, BtorNode *, BtorBitVector *, BtorBitVector **);
3506 BtorBitVector *(*compute_value) (
3507 Btor *, BtorNode *, BtorBitVector *, BtorBitVector *, int32_t);
3508 #ifndef NBTORLOG
3509 char *a;
3510 #endif
3511
3512 *input = 0;
3513 *assignment = 0;
3514 nprops = 0;
3515
3516 cur = root;
3517 bvcur = btor_bv_one (btor->mm, 1);
3518
3519 for (;;)
3520 {
3521 real_cur = btor_node_real_addr (cur);
3522
3523 if (btor_node_is_bv_var (cur))
3524 {
3525 *input = real_cur;
3526 *assignment = btor_node_is_inverted (cur)
3527 ? btor_bv_not (btor->mm, bvcur)
3528 : btor_bv_copy (btor->mm, bvcur);
3529 break;
3530 }
3531 else if (btor_node_is_bv_const (cur))
3532 {
3533 break;
3534 }
3535 else
3536 {
3537 nprops += 1;
3538 assert (!btor_node_is_bv_const (cur));
3539
3540 if (btor_node_is_inverted (cur))
3541 {
3542 tmp = bvcur;
3543 bvcur = btor_bv_not (btor->mm, tmp);
3544 btor_bv_free (btor->mm, tmp);
3545 }
3546
3547 /* check if all paths are const, if yes -> conflict */
3548 for (i = 0, nconst = 0; i < real_cur->arity; i++)
3549 {
3550 bve[i] = (BtorBitVector *) btor_model_get_bv (btor, real_cur->e[i]);
3551 if (btor_node_is_bv_const (real_cur->e[i])) nconst += 1;
3552 }
3553 if (nconst > real_cur->arity - 1) break;
3554
3555 #ifndef NBTORLOG
3556 a = btor_bv_to_char (btor->mm, bvcur);
3557 BTORLOG (2, "");
3558 BTORLOG (2, "propagate: %s", a);
3559 btor_mem_freestr (btor->mm, a);
3560 #endif
3561
3562 /* we either select a consistent or inverse value
3563 * as path assignment, depending on the given probability p
3564 * -> if b then inverse else consistent */
3565 b = btor_rng_pick_with_prob (
3566 &btor->rng, btor_opt_get (btor, BTOR_OPT_PROP_PROB_USE_INV_VALUE));
3567
3568 /* select path and determine path assignment */
3569 switch (real_cur->kind)
3570 {
3571 case BTOR_BV_ADD_NODE:
3572 select_path = select_path_add;
3573 compute_value = b ? inv_add_bv : cons_add_bv;
3574 break;
3575 case BTOR_BV_AND_NODE:
3576 select_path = select_path_and;
3577 compute_value = b ? inv_and_bv : cons_and_bv;
3578 break;
3579 case BTOR_BV_EQ_NODE:
3580 select_path = select_path_eq;
3581 compute_value = b ? inv_eq_bv : cons_eq_bv;
3582 break;
3583 case BTOR_BV_ULT_NODE:
3584 select_path = select_path_ult;
3585 compute_value = b ? inv_ult_bv : cons_ult_bv;
3586 break;
3587 case BTOR_BV_SLL_NODE:
3588 select_path = select_path_sll;
3589 compute_value = b ? inv_sll_bv : cons_sll_bv;
3590 break;
3591 case BTOR_BV_SRL_NODE:
3592 select_path = select_path_srl;
3593 compute_value = b ? inv_srl_bv : cons_srl_bv;
3594 break;
3595 case BTOR_BV_MUL_NODE:
3596 select_path = select_path_mul;
3597 compute_value = b ? inv_mul_bv : cons_mul_bv;
3598 break;
3599 case BTOR_BV_UDIV_NODE:
3600 select_path = select_path_udiv;
3601 compute_value = b ? inv_udiv_bv : cons_udiv_bv;
3602 break;
3603 case BTOR_BV_UREM_NODE:
3604 select_path = select_path_urem;
3605 compute_value = b ? inv_urem_bv : cons_urem_bv;
3606 break;
3607 case BTOR_BV_CONCAT_NODE:
3608 select_path = select_path_concat;
3609 compute_value = b ? inv_concat_bv : cons_concat_bv;
3610 break;
3611 case BTOR_BV_SLICE_NODE:
3612 select_path = select_path_slice;
3613 compute_value = b ? inv_slice_bv : cons_slice_bv;
3614 break;
3615 default:
3616 assert (btor_node_is_bv_cond (real_cur));
3617 select_path = select_path_cond;
3618 compute_value = b ? inv_cond_bv : cons_cond_bv;
3619 }
3620
3621 cur = select_move (
3622 btor, real_cur, bvcur, bve, select_path, compute_value, &bvenew);
3623 if (!bvenew) break; /* non-recoverable conflict */
3624
3625 btor_bv_free (btor->mm, bvcur);
3626 bvcur = bvenew;
3627 }
3628 }
3629
3630 btor_bv_free (btor->mm, bvcur);
3631
3632 return nprops;
3633 }
3634