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 "btorexp.h"
10
11 #include "btorcore.h"
12 #include "btordbg.h"
13 #include "btorrewrite.h"
14
15 #include <limits.h>
16
17 /*------------------------------------------------------------------------*/
18
19 BtorNode *
btor_exp_create(Btor * btor,BtorNodeKind kind,BtorNode * e[],uint32_t arity)20 btor_exp_create (Btor *btor, BtorNodeKind kind, BtorNode *e[], uint32_t arity)
21 {
22 assert (arity > 0);
23 assert (arity <= 3);
24
25 switch (kind)
26 {
27 case BTOR_BV_AND_NODE:
28 assert (arity == 2);
29 return btor_exp_bv_and (btor, e[0], e[1]);
30 case BTOR_BV_EQ_NODE:
31 case BTOR_FUN_EQ_NODE:
32 assert (arity == 2);
33 return btor_exp_eq (btor, e[0], e[1]);
34 case BTOR_BV_ADD_NODE:
35 assert (arity == 2);
36 return btor_exp_bv_add (btor, e[0], e[1]);
37 case BTOR_BV_MUL_NODE:
38 assert (arity == 2);
39 return btor_exp_bv_mul (btor, e[0], e[1]);
40 case BTOR_BV_ULT_NODE:
41 assert (arity == 2);
42 return btor_exp_bv_ult (btor, e[0], e[1]);
43 case BTOR_BV_SLL_NODE:
44 assert (arity == 2);
45 return btor_exp_bv_sll (btor, e[0], e[1]);
46 case BTOR_BV_SRL_NODE:
47 assert (arity == 2);
48 return btor_exp_bv_srl (btor, e[0], e[1]);
49 case BTOR_BV_UDIV_NODE:
50 assert (arity == 2);
51 return btor_exp_bv_udiv (btor, e[0], e[1]);
52 case BTOR_BV_UREM_NODE:
53 assert (arity == 2);
54 return btor_exp_bv_urem (btor, e[0], e[1]);
55 case BTOR_BV_CONCAT_NODE:
56 assert (arity == 2);
57 return btor_exp_bv_concat (btor, e[0], e[1]);
58 case BTOR_APPLY_NODE:
59 assert (arity == 2);
60 return btor_exp_apply (btor, e[0], e[1]);
61 case BTOR_LAMBDA_NODE:
62 assert (arity == 2);
63 return btor_exp_lambda (btor, e[0], e[1]);
64 case BTOR_EXISTS_NODE:
65 assert (arity == 2);
66 return btor_exp_exists (btor, e[0], e[1]);
67 case BTOR_FORALL_NODE:
68 assert (arity == 2);
69 return btor_exp_forall (btor, e[0], e[1]);
70 case BTOR_COND_NODE:
71 assert (arity == 3);
72 return btor_exp_cond (btor, e[0], e[1], e[2]);
73 case BTOR_UPDATE_NODE:
74 assert (arity == 3);
75 return btor_exp_update (btor, e[0], e[1], e[2]);
76 default:
77 assert (kind == BTOR_ARGS_NODE);
78 return btor_exp_args (btor, e, arity);
79 }
80 return 0;
81 }
82
83 /*------------------------------------------------------------------------*/
84
85 BtorNode *
btor_exp_var(Btor * btor,BtorSortId sort,const char * symbol)86 btor_exp_var (Btor *btor, BtorSortId sort, const char *symbol)
87 {
88 return btor_node_create_var (btor, sort, symbol);
89 }
90
91 BtorNode *
btor_exp_param(Btor * btor,BtorSortId sort,const char * symbol)92 btor_exp_param (Btor *btor, BtorSortId sort, const char *symbol)
93 {
94 return btor_node_create_param (btor, sort, symbol);
95 }
96
97 BtorNode *
btor_exp_array(Btor * btor,BtorSortId sort,const char * symbol)98 btor_exp_array (Btor *btor, BtorSortId sort, const char *symbol)
99 {
100 assert (btor);
101 assert (sort);
102 assert (btor_sort_is_fun (btor, sort));
103 assert (
104 btor_sort_tuple_get_arity (btor, btor_sort_fun_get_domain (btor, sort))
105 == 1);
106
107 BtorNode *exp;
108
109 exp = btor_exp_uf (btor, sort, symbol);
110 exp->is_array = 1;
111
112 return exp;
113 }
114
115 BtorNode *
btor_exp_const_array(Btor * btor,BtorSortId sort,BtorNode * value)116 btor_exp_const_array (Btor *btor, BtorSortId sort, BtorNode *value)
117 {
118 assert (btor);
119 assert (sort);
120 assert (btor_sort_is_fun (btor, sort));
121 assert (
122 btor_sort_tuple_get_arity (btor, btor_sort_fun_get_domain (btor, sort))
123 == 1);
124 assert (btor_sort_array_get_element (btor, sort)
125 == btor_node_get_sort_id (value));
126 assert (value);
127 assert (btor_sort_is_bv (btor, btor_node_get_sort_id (value)));
128
129 BtorNode *exp, *param;
130 BtorSortId idxsort;
131
132 idxsort = btor_sort_array_get_index (btor, sort);
133 param = btor_exp_param (btor, idxsort, 0);
134 exp = btor_exp_lambda (btor, param, value);
135 exp->is_array = 1;
136
137 btor_node_release (btor, param);
138
139 return exp;
140 }
141
142 BtorNode *
btor_exp_uf(Btor * btor,BtorSortId sort,const char * symbol)143 btor_exp_uf (Btor *btor, BtorSortId sort, const char *symbol)
144 {
145 return btor_node_create_uf (btor, sort, symbol);
146 }
147
148 /*------------------------------------------------------------------------*/
149
150 BtorNode *
btor_exp_true(Btor * btor)151 btor_exp_true (Btor *btor)
152 {
153 assert (btor);
154
155 BtorSortId sort;
156 BtorNode *result;
157
158 sort = btor_sort_bv (btor, 1);
159 result = btor_exp_bv_one (btor, sort);
160 btor_sort_release (btor, sort);
161 return result;
162 }
163
164 BtorNode *
btor_exp_false(Btor * btor)165 btor_exp_false (Btor *btor)
166 {
167 assert (btor);
168
169 BtorSortId sort;
170 BtorNode *result;
171
172 sort = btor_sort_bv (btor, 1);
173 result = btor_exp_bv_zero (btor, sort);
174 btor_sort_release (btor, sort);
175 return result;
176 }
177
178 BtorNode *
btor_exp_implies(Btor * btor,BtorNode * e0,BtorNode * e1)179 btor_exp_implies (Btor *btor, BtorNode *e0, BtorNode *e1)
180 {
181 assert (btor == btor_node_real_addr (e0)->btor);
182 assert (btor == btor_node_real_addr (e1)->btor);
183
184 e0 = btor_simplify_exp (btor, e0);
185 e1 = btor_simplify_exp (btor, e1);
186 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
187 assert (btor_node_bv_get_width (btor, e0) == 1);
188 return btor_node_invert (btor_exp_bv_and (btor, e0, btor_node_invert (e1)));
189 }
190
191 BtorNode *
btor_exp_iff(Btor * btor,BtorNode * e0,BtorNode * e1)192 btor_exp_iff (Btor *btor, BtorNode *e0, BtorNode *e1)
193 {
194 assert (btor == btor_node_real_addr (e0)->btor);
195 assert (btor == btor_node_real_addr (e1)->btor);
196
197 e0 = btor_simplify_exp (btor, e0);
198 e1 = btor_simplify_exp (btor, e1);
199 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
200 assert (btor_node_bv_get_width (btor, e0) == 1);
201 return btor_exp_eq (btor, e0, e1);
202 }
203
204 /*------------------------------------------------------------------------*/
205
206 BtorNode *
btor_exp_eq(Btor * btor,BtorNode * e0,BtorNode * e1)207 btor_exp_eq (Btor *btor, BtorNode *e0, BtorNode *e1)
208 {
209 assert (btor == btor_node_real_addr (e0)->btor);
210 assert (btor == btor_node_real_addr (e1)->btor);
211
212 BtorNode *result;
213
214 e0 = btor_simplify_exp (btor, e0);
215 e1 = btor_simplify_exp (btor, e1);
216 assert (btor_dbg_precond_eq_exp (btor, e0, e1));
217
218 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
219 {
220 if (btor_node_is_fun (e0))
221 result = btor_rewrite_binary_exp (btor, BTOR_FUN_EQ_NODE, e0, e1);
222 else
223 result = btor_rewrite_binary_exp (btor, BTOR_BV_EQ_NODE, e0, e1);
224 }
225 else
226 result = btor_node_create_eq (btor, e0, e1);
227
228 assert (result);
229 return result;
230 }
231
232 BtorNode *
btor_exp_ne(Btor * btor,BtorNode * e0,BtorNode * e1)233 btor_exp_ne (Btor *btor, BtorNode *e0, BtorNode *e1)
234 {
235 assert (btor == btor_node_real_addr (e0)->btor);
236 assert (btor == btor_node_real_addr (e1)->btor);
237
238 e0 = btor_simplify_exp (btor, e0);
239 e1 = btor_simplify_exp (btor, e1);
240 assert (btor_dbg_precond_eq_exp (btor, e0, e1));
241 return btor_node_invert (btor_exp_eq (btor, e0, e1));
242 }
243
244 /*------------------------------------------------------------------------*/
245
246 BtorNode *
btor_exp_cond(Btor * btor,BtorNode * e_cond,BtorNode * e_if,BtorNode * e_else)247 btor_exp_cond (Btor *btor, BtorNode *e_cond, BtorNode *e_if, BtorNode *e_else)
248 {
249 assert (btor == btor_node_real_addr (e_cond)->btor);
250 assert (btor == btor_node_real_addr (e_if)->btor);
251 assert (btor == btor_node_real_addr (e_else)->btor);
252
253 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
254 return btor_rewrite_ternary_exp (
255 btor, BTOR_COND_NODE, e_cond, e_if, e_else);
256
257 return btor_node_create_cond (btor, e_cond, e_if, e_else);
258 }
259
260 BtorNode *
btor_exp_bv_const(Btor * btor,const BtorBitVector * bits)261 btor_exp_bv_const (Btor *btor, const BtorBitVector *bits)
262 {
263 return btor_node_create_bv_const (btor, bits);
264 }
265
266 /*------------------------------------------------------------------------*/
267
268 static BtorNode *
int_min_exp(Btor * btor,uint32_t width)269 int_min_exp (Btor *btor, uint32_t width)
270 {
271 assert (btor);
272 assert (width > 0);
273
274 BtorBitVector *bv;
275 BtorNode *result;
276
277 bv = btor_bv_new (btor->mm, width);
278 btor_bv_set_bit (bv, width - 1, 1);
279 result = btor_exp_bv_const (btor, bv);
280 btor_bv_free (btor->mm, bv);
281 return result;
282 }
283
284 BtorNode *
btor_exp_bv_zero(Btor * btor,BtorSortId sort)285 btor_exp_bv_zero (Btor *btor, BtorSortId sort)
286 {
287 assert (btor);
288 assert (sort);
289 assert (btor_sort_is_bv (btor, sort));
290
291 uint32_t width;
292 BtorNode *result;
293 BtorBitVector *bv;
294
295 width = btor_sort_bv_get_width (btor, sort);
296 bv = btor_bv_new (btor->mm, width);
297 result = btor_exp_bv_const (btor, bv);
298 btor_bv_free (btor->mm, bv);
299 return result;
300 }
301
302 BtorNode *
btor_exp_bv_ones(Btor * btor,BtorSortId sort)303 btor_exp_bv_ones (Btor *btor, BtorSortId sort)
304 {
305 assert (btor);
306 assert (sort);
307 assert (btor_sort_is_bv (btor, sort));
308
309 uint32_t width;
310 BtorNode *result;
311 BtorBitVector *bv;
312
313 width = btor_sort_bv_get_width (btor, sort);
314 bv = btor_bv_ones (btor->mm, width);
315 result = btor_exp_bv_const (btor, bv);
316 btor_bv_free (btor->mm, bv);
317 return result;
318 }
319
320 BtorNode *
btor_exp_bv_one(Btor * btor,BtorSortId sort)321 btor_exp_bv_one (Btor *btor, BtorSortId sort)
322 {
323 assert (btor);
324 assert (sort);
325 assert (btor_sort_is_bv (btor, sort));
326
327 uint32_t width;
328 BtorNode *result;
329 BtorBitVector *bv;
330
331 width = btor_sort_bv_get_width (btor, sort);
332 bv = btor_bv_one (btor->mm, width);
333 result = btor_exp_bv_const (btor, bv);
334 btor_bv_free (btor->mm, bv);
335 return result;
336 }
337
338 BtorNode *
btor_exp_bv_min_signed(Btor * btor,BtorSortId sort)339 btor_exp_bv_min_signed (Btor *btor, BtorSortId sort)
340 {
341 assert (btor);
342 assert (sort);
343 assert (btor_sort_is_bv (btor, sort));
344
345 uint32_t width;
346 BtorNode *result;
347 BtorBitVector *bv;
348
349 width = btor_sort_bv_get_width (btor, sort);
350 bv = btor_bv_min_signed (btor->mm, width);
351 result = btor_exp_bv_const (btor, bv);
352 btor_bv_free (btor->mm, bv);
353 return result;
354 }
355
356 BtorNode *
btor_exp_bv_max_signed(Btor * btor,BtorSortId sort)357 btor_exp_bv_max_signed (Btor *btor, BtorSortId sort)
358 {
359 assert (btor);
360 assert (sort);
361 assert (btor_sort_is_bv (btor, sort));
362
363 uint32_t width;
364 BtorNode *result;
365 BtorBitVector *bv;
366
367 width = btor_sort_bv_get_width (btor, sort);
368 bv = btor_bv_max_signed (btor->mm, width);
369 result = btor_exp_bv_const (btor, bv);
370 btor_bv_free (btor->mm, bv);
371 return result;
372 }
373
374 BtorNode *
btor_exp_bv_int(Btor * btor,int32_t i,BtorSortId sort)375 btor_exp_bv_int (Btor *btor, int32_t i, BtorSortId sort)
376 {
377 assert (btor);
378 assert (sort);
379 assert (btor_sort_is_bv (btor, sort));
380
381 uint32_t width;
382 BtorNode *result;
383 BtorBitVector *bv;
384
385 width = btor_sort_bv_get_width (btor, sort);
386 bv = btor_bv_int64_to_bv (btor->mm, i, width);
387 result = btor_exp_bv_const (btor, bv);
388 btor_bv_free (btor->mm, bv);
389 return result;
390 }
391
392 BtorNode *
btor_exp_bv_unsigned(Btor * btor,uint32_t u,BtorSortId sort)393 btor_exp_bv_unsigned (Btor *btor, uint32_t u, BtorSortId sort)
394 {
395 assert (btor);
396 assert (sort);
397 assert (btor_sort_is_bv (btor, sort));
398
399 uint32_t width;
400 BtorNode *result;
401 BtorBitVector *bv;
402
403 width = btor_sort_bv_get_width (btor, sort);
404 bv = btor_bv_uint64_to_bv (btor->mm, u, width);
405 result = btor_exp_bv_const (btor, bv);
406 btor_bv_free (btor->mm, bv);
407 return result;
408 }
409
410 /*------------------------------------------------------------------------*/
411
412 BtorNode *
btor_exp_bv_not(Btor * btor,BtorNode * exp)413 btor_exp_bv_not (Btor *btor, BtorNode *exp)
414 {
415 assert (btor == btor_node_real_addr (exp)->btor);
416
417 exp = btor_simplify_exp (btor, exp);
418 assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
419
420 (void) btor;
421 btor_node_copy (btor, exp);
422 return btor_node_invert (exp);
423 }
424
425 BtorNode *
btor_exp_bv_neg(Btor * btor,BtorNode * exp)426 btor_exp_bv_neg (Btor *btor, BtorNode *exp)
427 {
428 assert (btor == btor_node_real_addr (exp)->btor);
429
430 BtorNode *result, *one;
431
432 exp = btor_simplify_exp (btor, exp);
433 assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
434 one = btor_exp_bv_one (btor, btor_node_get_sort_id (exp));
435 result = btor_exp_bv_add (btor, btor_node_invert (exp), one);
436 btor_node_release (btor, one);
437 return result;
438 }
439
440 BtorNode *
btor_exp_bv_redor(Btor * btor,BtorNode * exp)441 btor_exp_bv_redor (Btor *btor, BtorNode *exp)
442 {
443 assert (btor == btor_node_real_addr (exp)->btor);
444
445 BtorNode *result, *zero;
446
447 exp = btor_simplify_exp (btor, exp);
448 assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
449
450 zero = btor_exp_bv_zero (btor, btor_node_get_sort_id (exp));
451 result = btor_node_invert (btor_exp_eq (btor, exp, zero));
452 btor_node_release (btor, zero);
453 return result;
454 }
455
456 BtorNode *
btor_exp_bv_redxor(Btor * btor,BtorNode * exp)457 btor_exp_bv_redxor (Btor *btor, BtorNode *exp)
458 {
459 assert (btor == btor_node_real_addr (exp)->btor);
460
461 BtorNode *result, *slice, *xor;
462 uint32_t i, width;
463
464 exp = btor_simplify_exp (btor, exp);
465 assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
466
467 width = btor_node_bv_get_width (btor, exp);
468
469 result = btor_exp_bv_slice (btor, exp, 0, 0);
470 for (i = 1; i < width; i++)
471 {
472 slice = btor_exp_bv_slice (btor, exp, i, i);
473 xor = btor_exp_bv_xor (btor, result, slice);
474 btor_node_release (btor, slice);
475 btor_node_release (btor, result);
476 result = xor;
477 }
478 return result;
479 }
480
481 BtorNode *
btor_exp_bv_slice(Btor * btor,BtorNode * exp,uint32_t upper,uint32_t lower)482 btor_exp_bv_slice (Btor *btor, BtorNode *exp, uint32_t upper, uint32_t lower)
483 {
484 assert (btor == btor_node_real_addr (exp)->btor);
485
486 BtorNode *result;
487
488 exp = btor_simplify_exp (btor, exp);
489 assert (btor_dbg_precond_slice_exp (btor, exp, upper, lower));
490
491 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
492 result = btor_rewrite_slice_exp (btor, exp, upper, lower);
493 else
494 result = btor_node_create_bv_slice (btor, exp, upper, lower);
495
496 assert (result);
497 return result;
498 }
499
500 BtorNode *
btor_exp_bv_redand(Btor * btor,BtorNode * exp)501 btor_exp_bv_redand (Btor *btor, BtorNode *exp)
502 {
503 assert (btor == btor_node_real_addr (exp)->btor);
504
505 BtorNode *result, *ones;
506
507 exp = btor_simplify_exp (btor, exp);
508 assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
509
510 ones = btor_exp_bv_ones (btor, btor_node_get_sort_id (exp));
511 result = btor_exp_eq (btor, exp, ones);
512 btor_node_release (btor, ones);
513 return result;
514 }
515
516 BtorNode *
btor_exp_bv_uext(Btor * btor,BtorNode * exp,uint32_t width)517 btor_exp_bv_uext (Btor *btor, BtorNode *exp, uint32_t width)
518 {
519 assert (btor == btor_node_real_addr (exp)->btor);
520
521 BtorNode *result, *zero;
522 BtorSortId sort;
523
524 exp = btor_simplify_exp (btor, exp);
525 assert (btor_dbg_precond_ext_exp (btor, exp));
526
527 if (width == 0)
528 result = btor_node_copy (btor, exp);
529 else
530 {
531 assert (width > 0);
532 sort = btor_sort_bv (btor, width);
533 zero = btor_exp_bv_zero (btor, sort);
534 btor_sort_release (btor, sort);
535 result = btor_exp_bv_concat (btor, zero, exp);
536 btor_node_release (btor, zero);
537 }
538 return result;
539 }
540
541 BtorNode *
btor_exp_bv_sext(Btor * btor,BtorNode * exp,uint32_t width)542 btor_exp_bv_sext (Btor *btor, BtorNode *exp, uint32_t width)
543 {
544 assert (btor == btor_node_real_addr (exp)->btor);
545
546 BtorNode *result, *zero, *ones, *neg, *cond;
547 uint32_t exp_width;
548 BtorSortId sort;
549
550 exp = btor_simplify_exp (btor, exp);
551 assert (btor_dbg_precond_ext_exp (btor, exp));
552
553 if (width == 0)
554 result = btor_node_copy (btor, exp);
555 else
556 {
557 assert (width > 0);
558 sort = btor_sort_bv (btor, width);
559 zero = btor_exp_bv_zero (btor, sort);
560 ones = btor_exp_bv_ones (btor, sort);
561 btor_sort_release (btor, sort);
562 exp_width = btor_node_bv_get_width (btor, exp);
563 neg = btor_exp_bv_slice (btor, exp, exp_width - 1, exp_width - 1);
564 cond = btor_exp_cond (btor, neg, ones, zero);
565 result = btor_exp_bv_concat (btor, cond, exp);
566 btor_node_release (btor, zero);
567 btor_node_release (btor, ones);
568 btor_node_release (btor, neg);
569 btor_node_release (btor, cond);
570 }
571 return result;
572 }
573
574 BtorNode *
btor_exp_bv_xor(Btor * btor,BtorNode * e0,BtorNode * e1)575 btor_exp_bv_xor (Btor *btor, BtorNode *e0, BtorNode *e1)
576 {
577 assert (btor == btor_node_real_addr (e0)->btor);
578 assert (btor == btor_node_real_addr (e1)->btor);
579
580 BtorNode *result, * or, *and;
581
582 e0 = btor_simplify_exp (btor, e0);
583 e1 = btor_simplify_exp (btor, e1);
584 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
585
586 or = btor_exp_bv_or (btor, e0, e1);
587 and = btor_exp_bv_and (btor, e0, e1);
588 result = btor_exp_bv_and (btor, or, btor_node_invert (and));
589 btor_node_release (btor, or);
590 btor_node_release (btor, and);
591 return result;
592 }
593
594 BtorNode *
btor_exp_bv_xnor(Btor * btor,BtorNode * e0,BtorNode * e1)595 btor_exp_bv_xnor (Btor *btor, BtorNode *e0, BtorNode *e1)
596 {
597 assert (btor == btor_node_real_addr (e0)->btor);
598 assert (btor == btor_node_real_addr (e1)->btor);
599
600 e0 = btor_simplify_exp (btor, e0);
601 e1 = btor_simplify_exp (btor, e1);
602 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
603 return btor_node_invert (btor_exp_bv_xor (btor, e0, e1));
604 }
605
606 BtorNode *
btor_exp_bv_and(Btor * btor,BtorNode * e0,BtorNode * e1)607 btor_exp_bv_and (Btor *btor, BtorNode *e0, BtorNode *e1)
608 {
609 assert (btor == btor_node_real_addr (e0)->btor);
610 assert (btor == btor_node_real_addr (e1)->btor);
611
612 BtorNode *result;
613
614 e0 = btor_simplify_exp (btor, e0);
615 e1 = btor_simplify_exp (btor, e1);
616 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
617
618 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
619 result = btor_rewrite_binary_exp (btor, BTOR_BV_AND_NODE, e0, e1);
620 else
621 result = btor_node_create_bv_and (btor, e0, e1);
622
623 assert (result);
624 return result;
625 }
626
627 static BtorNode *
create_bin_n_exp(Btor * btor,BtorNode * (* func)(Btor *,BtorNode *,BtorNode *),BtorNode * args[],uint32_t argc)628 create_bin_n_exp (Btor *btor,
629 BtorNode *(*func) (Btor *, BtorNode *, BtorNode *),
630 BtorNode *args[],
631 uint32_t argc)
632 {
633 assert (argc > 0);
634
635 uint32_t i;
636 BtorNode *result, *tmp, *arg;
637
638 result = 0;
639 for (i = 0; i < argc; i++)
640 {
641 arg = args[i];
642 if (result)
643 {
644 tmp = func (btor, arg, result);
645 btor_node_release (btor, result);
646 result = tmp;
647 }
648 else
649 result = btor_node_copy (btor, arg);
650 }
651 assert (result);
652 return result;
653 }
654
655 BtorNode *
btor_exp_bv_and_n(Btor * btor,BtorNode * args[],uint32_t argc)656 btor_exp_bv_and_n (Btor *btor, BtorNode *args[], uint32_t argc)
657 {
658 return create_bin_n_exp (btor, btor_exp_bv_and, args, argc);
659 }
660
661 BtorNode *
btor_exp_bv_nand(Btor * btor,BtorNode * e0,BtorNode * e1)662 btor_exp_bv_nand (Btor *btor, BtorNode *e0, BtorNode *e1)
663 {
664 assert (btor == btor_node_real_addr (e0)->btor);
665 assert (btor == btor_node_real_addr (e1)->btor);
666
667 e0 = btor_simplify_exp (btor, e0);
668 e1 = btor_simplify_exp (btor, e1);
669 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
670 return btor_node_invert (btor_exp_bv_and (btor, e0, e1));
671 }
672
673 BtorNode *
btor_exp_bv_or(Btor * btor,BtorNode * e0,BtorNode * e1)674 btor_exp_bv_or (Btor *btor, BtorNode *e0, BtorNode *e1)
675 {
676 assert (btor == btor_node_real_addr (e0)->btor);
677 assert (btor == btor_node_real_addr (e1)->btor);
678
679 e0 = btor_simplify_exp (btor, e0);
680 e1 = btor_simplify_exp (btor, e1);
681 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
682 return btor_node_invert (
683 btor_exp_bv_and (btor, btor_node_invert (e0), btor_node_invert (e1)));
684 }
685
686 BtorNode *
btor_exp_bv_nor(Btor * btor,BtorNode * e0,BtorNode * e1)687 btor_exp_bv_nor (Btor *btor, BtorNode *e0, BtorNode *e1)
688 {
689 assert (btor == btor_node_real_addr (e0)->btor);
690 assert (btor == btor_node_real_addr (e1)->btor);
691
692 e0 = btor_simplify_exp (btor, e0);
693 e1 = btor_simplify_exp (btor, e1);
694 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
695 return btor_node_invert (btor_exp_bv_or (btor, e0, e1));
696 }
697 BtorNode *
btor_exp_bv_add(Btor * btor,BtorNode * e0,BtorNode * e1)698 btor_exp_bv_add (Btor *btor, BtorNode *e0, BtorNode *e1)
699 {
700 assert (btor == btor_node_real_addr (e0)->btor);
701 assert (btor == btor_node_real_addr (e1)->btor);
702
703 BtorNode *result;
704
705 e0 = btor_simplify_exp (btor, e0);
706 e1 = btor_simplify_exp (btor, e1);
707 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
708
709 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
710 result = btor_rewrite_binary_exp (btor, BTOR_BV_ADD_NODE, e0, e1);
711 else
712 result = btor_node_create_bv_add (btor, e0, e1);
713
714 assert (result);
715 return result;
716 }
717
718 BtorNode *
btor_exp_bv_add_n(Btor * btor,BtorNode * args[],uint32_t argc)719 btor_exp_bv_add_n (Btor *btor, BtorNode *args[], uint32_t argc)
720 {
721 return create_bin_n_exp (btor, btor_exp_bv_add, args, argc);
722 }
723
724 BtorNode *
btor_exp_bv_uaddo(Btor * btor,BtorNode * e0,BtorNode * e1)725 btor_exp_bv_uaddo (Btor *btor, BtorNode *e0, BtorNode *e1)
726 {
727 assert (btor == btor_node_real_addr (e0)->btor);
728 assert (btor == btor_node_real_addr (e1)->btor);
729
730 BtorNode *result, *uext_e1, *uext_e2, *add;
731 uint32_t width;
732
733 e0 = btor_simplify_exp (btor, e0);
734 e1 = btor_simplify_exp (btor, e1);
735 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
736
737 width = btor_node_bv_get_width (btor, e0);
738 uext_e1 = btor_exp_bv_uext (btor, e0, 1);
739 uext_e2 = btor_exp_bv_uext (btor, e1, 1);
740 add = btor_exp_bv_add (btor, uext_e1, uext_e2);
741 result = btor_exp_bv_slice (btor, add, width, width);
742 btor_node_release (btor, uext_e1);
743 btor_node_release (btor, uext_e2);
744 btor_node_release (btor, add);
745 return result;
746 }
747
748 BtorNode *
btor_exp_bv_saddo(Btor * btor,BtorNode * e0,BtorNode * e1)749 btor_exp_bv_saddo (Btor *btor, BtorNode *e0, BtorNode *e1)
750 {
751 assert (btor == btor_node_real_addr (e0)->btor);
752 assert (btor == btor_node_real_addr (e1)->btor);
753
754 BtorNode *result, *sign_e1, *sign_e2, *sign_result;
755 BtorNode *add, *and1, *and2, *or1, *or2;
756 uint32_t width;
757
758 e0 = btor_simplify_exp (btor, e0);
759 e1 = btor_simplify_exp (btor, e1);
760 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
761
762 width = btor_node_bv_get_width (btor, e0);
763 sign_e1 = btor_exp_bv_slice (btor, e0, width - 1, width - 1);
764 sign_e2 = btor_exp_bv_slice (btor, e1, width - 1, width - 1);
765 add = btor_exp_bv_add (btor, e0, e1);
766 sign_result = btor_exp_bv_slice (btor, add, width - 1, width - 1);
767 and1 = btor_exp_bv_and (btor, sign_e1, sign_e2);
768 or1 = btor_exp_bv_and (btor, and1, btor_node_invert (sign_result));
769 and2 = btor_exp_bv_and (
770 btor, btor_node_invert (sign_e1), btor_node_invert (sign_e2));
771 or2 = btor_exp_bv_and (btor, and2, sign_result);
772 result = btor_exp_bv_or (btor, or1, or2);
773 btor_node_release (btor, and1);
774 btor_node_release (btor, and2);
775 btor_node_release (btor, or1);
776 btor_node_release (btor, or2);
777 btor_node_release (btor, add);
778 btor_node_release (btor, sign_e1);
779 btor_node_release (btor, sign_e2);
780 btor_node_release (btor, sign_result);
781 return result;
782 }
783
784 BtorNode *
btor_exp_bv_mul(Btor * btor,BtorNode * e0,BtorNode * e1)785 btor_exp_bv_mul (Btor *btor, BtorNode *e0, BtorNode *e1)
786 {
787 assert (btor == btor_node_real_addr (e0)->btor);
788 assert (btor == btor_node_real_addr (e1)->btor);
789
790 BtorNode *result;
791
792 e0 = btor_simplify_exp (btor, e0);
793 e1 = btor_simplify_exp (btor, e1);
794 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
795
796 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
797 result = btor_rewrite_binary_exp (btor, BTOR_BV_MUL_NODE, e0, e1);
798 else
799 result = btor_node_create_bv_mul (btor, e0, e1);
800
801 assert (result);
802 return result;
803 }
804
805 BtorNode *
btor_exp_bv_umulo(Btor * btor,BtorNode * e0,BtorNode * e1)806 btor_exp_bv_umulo (Btor *btor, BtorNode *e0, BtorNode *e1)
807 {
808 assert (btor == btor_node_real_addr (e0)->btor);
809 assert (btor == btor_node_real_addr (e1)->btor);
810
811 BtorNode *result, *uext_e1, *uext_e2, *mul, *slice, *and, * or, **temps_e2;
812 BtorSortId sort;
813 uint32_t i, width;
814
815 e0 = btor_simplify_exp (btor, e0);
816 e1 = btor_simplify_exp (btor, e1);
817 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
818
819 width = btor_node_bv_get_width (btor, e0);
820 if (width == 1)
821 {
822 sort = btor_sort_bv (btor, 1);
823 result = btor_exp_bv_zero (btor, sort);
824 btor_sort_release (btor, sort);
825 return result;
826 }
827 BTOR_NEWN (btor->mm, temps_e2, width - 1);
828 temps_e2[0] = btor_exp_bv_slice (btor, e1, width - 1, width - 1);
829 for (i = 1; i < width - 1; i++)
830 {
831 slice = btor_exp_bv_slice (btor, e1, width - 1 - i, width - 1 - i);
832 temps_e2[i] = btor_exp_bv_or (btor, temps_e2[i - 1], slice);
833 btor_node_release (btor, slice);
834 }
835 slice = btor_exp_bv_slice (btor, e0, 1, 1);
836 result = btor_exp_bv_and (btor, slice, temps_e2[0]);
837 btor_node_release (btor, slice);
838 for (i = 1; i < width - 1; i++)
839 {
840 slice = btor_exp_bv_slice (btor, e0, i + 1, i + 1);
841 and = btor_exp_bv_and (btor, slice, temps_e2[i]);
842 or = btor_exp_bv_or (btor, result, and);
843 btor_node_release (btor, slice);
844 btor_node_release (btor, and);
845 btor_node_release (btor, result);
846 result = or ;
847 }
848 uext_e1 = btor_exp_bv_uext (btor, e0, 1);
849 uext_e2 = btor_exp_bv_uext (btor, e1, 1);
850 mul = btor_exp_bv_mul (btor, uext_e1, uext_e2);
851 slice = btor_exp_bv_slice (btor, mul, width, width);
852 or = btor_exp_bv_or (btor, result, slice);
853 btor_node_release (btor, uext_e1);
854 btor_node_release (btor, uext_e2);
855 btor_node_release (btor, mul);
856 btor_node_release (btor, slice);
857 btor_node_release (btor, result);
858 result = or ;
859 for (i = 0; i < width - 1; i++) btor_node_release (btor, temps_e2[i]);
860 BTOR_DELETEN (btor->mm, temps_e2, width - 1);
861 return result;
862 }
863
864 BtorNode *
btor_exp_bv_smulo(Btor * btor,BtorNode * e0,BtorNode * e1)865 btor_exp_bv_smulo (Btor *btor, BtorNode *e0, BtorNode *e1)
866 {
867 assert (btor == btor_node_real_addr (e0)->btor);
868 assert (btor == btor_node_real_addr (e1)->btor);
869
870 BtorNode *result, *sext_e1, *sext_e2, *sign_e1, *sign_e2, *sext_sign_e1;
871 BtorNode *sext_sign_e2, *xor_sign_e1, *xor_sign_e2, *mul, *slice, *slice_n;
872 BtorNode *slice_n_minus_1, *xor, *and, * or, **temps_e2;
873 uint32_t i, width;
874
875 e0 = btor_simplify_exp (btor, e0);
876 e1 = btor_simplify_exp (btor, e1);
877 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
878
879 width = btor_node_bv_get_width (btor, e0);
880 if (width == 1) return btor_exp_bv_and (btor, e0, e1);
881 if (width == 2)
882 {
883 sext_e1 = btor_exp_bv_sext (btor, e0, 1);
884 sext_e2 = btor_exp_bv_sext (btor, e1, 1);
885 mul = btor_exp_bv_mul (btor, sext_e1, sext_e2);
886 slice_n = btor_exp_bv_slice (btor, mul, width, width);
887 slice_n_minus_1 = btor_exp_bv_slice (btor, mul, width - 1, width - 1);
888 result = btor_exp_bv_xor (btor, slice_n, slice_n_minus_1);
889 btor_node_release (btor, sext_e1);
890 btor_node_release (btor, sext_e2);
891 btor_node_release (btor, mul);
892 btor_node_release (btor, slice_n);
893 btor_node_release (btor, slice_n_minus_1);
894 }
895 else
896 {
897 sign_e1 = btor_exp_bv_slice (btor, e0, width - 1, width - 1);
898 sign_e2 = btor_exp_bv_slice (btor, e1, width - 1, width - 1);
899 sext_sign_e1 = btor_exp_bv_sext (btor, sign_e1, width - 1);
900 sext_sign_e2 = btor_exp_bv_sext (btor, sign_e2, width - 1);
901 xor_sign_e1 = btor_exp_bv_xor (btor, e0, sext_sign_e1);
902 xor_sign_e2 = btor_exp_bv_xor (btor, e1, sext_sign_e2);
903 BTOR_NEWN (btor->mm, temps_e2, width - 2);
904 temps_e2[0] = btor_exp_bv_slice (btor, xor_sign_e2, width - 2, width - 2);
905 for (i = 1; i < width - 2; i++)
906 {
907 slice =
908 btor_exp_bv_slice (btor, xor_sign_e2, width - 2 - i, width - 2 - i);
909 temps_e2[i] = btor_exp_bv_or (btor, temps_e2[i - 1], slice);
910 btor_node_release (btor, slice);
911 }
912 slice = btor_exp_bv_slice (btor, xor_sign_e1, 1, 1);
913 result = btor_exp_bv_and (btor, slice, temps_e2[0]);
914 btor_node_release (btor, slice);
915 for (i = 1; i < width - 2; i++)
916 {
917 slice = btor_exp_bv_slice (btor, xor_sign_e1, i + 1, i + 1);
918 and = btor_exp_bv_and (btor, slice, temps_e2[i]);
919 or = btor_exp_bv_or (btor, result, and);
920 btor_node_release (btor, slice);
921 btor_node_release (btor, and);
922 btor_node_release (btor, result);
923 result = or ;
924 }
925 sext_e1 = btor_exp_bv_sext (btor, e0, 1);
926 sext_e2 = btor_exp_bv_sext (btor, e1, 1);
927 mul = btor_exp_bv_mul (btor, sext_e1, sext_e2);
928 slice_n = btor_exp_bv_slice (btor, mul, width, width);
929 slice_n_minus_1 = btor_exp_bv_slice (btor, mul, width - 1, width - 1);
930 xor = btor_exp_bv_xor (btor, slice_n, slice_n_minus_1);
931 or = btor_exp_bv_or (btor, result, xor);
932 btor_node_release (btor, sext_e1);
933 btor_node_release (btor, sext_e2);
934 btor_node_release (btor, sign_e1);
935 btor_node_release (btor, sign_e2);
936 btor_node_release (btor, sext_sign_e1);
937 btor_node_release (btor, sext_sign_e2);
938 btor_node_release (btor, xor_sign_e1);
939 btor_node_release (btor, xor_sign_e2);
940 btor_node_release (btor, mul);
941 btor_node_release (btor, slice_n);
942 btor_node_release (btor, slice_n_minus_1);
943 btor_node_release (btor, xor);
944 btor_node_release (btor, result);
945 result = or ;
946 for (i = 0; i < width - 2; i++) btor_node_release (btor, temps_e2[i]);
947 BTOR_DELETEN (btor->mm, temps_e2, width - 2);
948 }
949 return result;
950 }
951
952 BtorNode *
btor_exp_bv_ult(Btor * btor,BtorNode * e0,BtorNode * e1)953 btor_exp_bv_ult (Btor *btor, BtorNode *e0, BtorNode *e1)
954 {
955 assert (btor == btor_node_real_addr (e0)->btor);
956 assert (btor == btor_node_real_addr (e1)->btor);
957
958 BtorNode *result;
959
960 e0 = btor_simplify_exp (btor, e0);
961 e1 = btor_simplify_exp (btor, e1);
962 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
963
964 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
965 result = btor_rewrite_binary_exp (btor, BTOR_BV_ULT_NODE, e0, e1);
966 else
967 result = btor_node_create_bv_ult (btor, e0, e1);
968
969 assert (result);
970 return result;
971 }
972
973 BtorNode *
btor_exp_bv_slt(Btor * btor,BtorNode * e0,BtorNode * e1)974 btor_exp_bv_slt (Btor *btor, BtorNode *e0, BtorNode *e1)
975 {
976 assert (btor == btor_node_real_addr (e0)->btor);
977 assert (btor == btor_node_real_addr (e1)->btor);
978
979 BtorNode *determined_by_sign, *eq_sign, *ult, *eq_sign_and_ult;
980 BtorNode *res, *s0, *s1, *r0, *r1, *l, *r;
981
982 uint32_t width;
983
984 e0 = btor_simplify_exp (btor, e0);
985 e1 = btor_simplify_exp (btor, e1);
986 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
987
988 width = btor_node_bv_get_width (btor, e0);
989 if (width == 1) return btor_exp_bv_and (btor, e0, btor_node_invert (e1));
990 s0 = btor_exp_bv_slice (btor, e0, width - 1, width - 1);
991 s1 = btor_exp_bv_slice (btor, e1, width - 1, width - 1);
992 r0 = btor_exp_bv_slice (btor, e0, width - 2, 0);
993 r1 = btor_exp_bv_slice (btor, e1, width - 2, 0);
994 ult = btor_exp_bv_ult (btor, r0, r1);
995 determined_by_sign = btor_exp_bv_and (btor, s0, btor_node_invert (s1));
996 l = btor_node_copy (btor, determined_by_sign);
997 r = btor_exp_bv_and (btor, btor_node_invert (s0), s1);
998 eq_sign = btor_exp_bv_and (btor, btor_node_invert (l), btor_node_invert (r));
999 eq_sign_and_ult = btor_exp_bv_and (btor, eq_sign, ult);
1000 res = btor_exp_bv_or (btor, determined_by_sign, eq_sign_and_ult);
1001 btor_node_release (btor, s0);
1002 btor_node_release (btor, s1);
1003 btor_node_release (btor, r0);
1004 btor_node_release (btor, r1);
1005 btor_node_release (btor, ult);
1006 btor_node_release (btor, determined_by_sign);
1007 btor_node_release (btor, l);
1008 btor_node_release (btor, r);
1009 btor_node_release (btor, eq_sign);
1010 btor_node_release (btor, eq_sign_and_ult);
1011 return res;
1012 }
1013
1014 BtorNode *
btor_exp_bv_ulte(Btor * btor,BtorNode * e0,BtorNode * e1)1015 btor_exp_bv_ulte (Btor *btor, BtorNode *e0, BtorNode *e1)
1016 {
1017 assert (btor == btor_node_real_addr (e0)->btor);
1018 assert (btor == btor_node_real_addr (e1)->btor);
1019
1020 BtorNode *result, *ult;
1021
1022 e0 = btor_simplify_exp (btor, e0);
1023 e1 = btor_simplify_exp (btor, e1);
1024 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1025
1026 ult = btor_exp_bv_ult (btor, e1, e0);
1027 result = btor_exp_bv_not (btor, ult);
1028 btor_node_release (btor, ult);
1029 return result;
1030 }
1031
1032 BtorNode *
btor_exp_bv_slte(Btor * btor,BtorNode * e0,BtorNode * e1)1033 btor_exp_bv_slte (Btor *btor, BtorNode *e0, BtorNode *e1)
1034 {
1035 assert (btor == btor_node_real_addr (e0)->btor);
1036 assert (btor == btor_node_real_addr (e1)->btor);
1037
1038 BtorNode *result, *slt;
1039
1040 e0 = btor_simplify_exp (btor, e0);
1041 e1 = btor_simplify_exp (btor, e1);
1042 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1043
1044 slt = btor_exp_bv_slt (btor, e1, e0);
1045 result = btor_exp_bv_not (btor, slt);
1046 btor_node_release (btor, slt);
1047 return result;
1048 }
1049
1050 BtorNode *
btor_exp_bv_ugt(Btor * btor,BtorNode * e0,BtorNode * e1)1051 btor_exp_bv_ugt (Btor *btor, BtorNode *e0, BtorNode *e1)
1052 {
1053 assert (btor == btor_node_real_addr (e0)->btor);
1054 assert (btor == btor_node_real_addr (e1)->btor);
1055
1056 e0 = btor_simplify_exp (btor, e0);
1057 e1 = btor_simplify_exp (btor, e1);
1058 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1059 return btor_exp_bv_ult (btor, e1, e0);
1060 }
1061
1062 BtorNode *
btor_exp_bv_sgt(Btor * btor,BtorNode * e0,BtorNode * e1)1063 btor_exp_bv_sgt (Btor *btor, BtorNode *e0, BtorNode *e1)
1064 {
1065 assert (btor == btor_node_real_addr (e0)->btor);
1066 assert (btor == btor_node_real_addr (e1)->btor);
1067
1068 e0 = btor_simplify_exp (btor, e0);
1069 e1 = btor_simplify_exp (btor, e1);
1070 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1071 return btor_exp_bv_slt (btor, e1, e0);
1072 }
1073
1074 BtorNode *
btor_exp_bv_ugte(Btor * btor,BtorNode * e0,BtorNode * e1)1075 btor_exp_bv_ugte (Btor *btor, BtorNode *e0, BtorNode *e1)
1076 {
1077 assert (btor == btor_node_real_addr (e0)->btor);
1078 assert (btor == btor_node_real_addr (e1)->btor);
1079
1080 BtorNode *result, *ult;
1081
1082 e0 = btor_simplify_exp (btor, e0);
1083 e1 = btor_simplify_exp (btor, e1);
1084 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1085
1086 ult = btor_exp_bv_ult (btor, e0, e1);
1087 result = btor_exp_bv_not (btor, ult);
1088 btor_node_release (btor, ult);
1089 return result;
1090 }
1091
1092 BtorNode *
btor_exp_bv_sgte(Btor * btor,BtorNode * e0,BtorNode * e1)1093 btor_exp_bv_sgte (Btor *btor, BtorNode *e0, BtorNode *e1)
1094 {
1095 assert (btor == btor_node_real_addr (e0)->btor);
1096 assert (btor == btor_node_real_addr (e1)->btor);
1097
1098 BtorNode *result, *slt;
1099
1100 e0 = btor_simplify_exp (btor, e0);
1101 e1 = btor_simplify_exp (btor, e1);
1102 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1103
1104 slt = btor_exp_bv_slt (btor, e0, e1);
1105 result = btor_exp_bv_not (btor, slt);
1106 btor_node_release (btor, slt);
1107 return result;
1108 }
1109
1110 BtorNode *
btor_exp_bv_sll(Btor * btor,BtorNode * e0,BtorNode * e1)1111 btor_exp_bv_sll (Btor *btor, BtorNode *e0, BtorNode *e1)
1112 {
1113 assert (btor == btor_node_real_addr (e0)->btor);
1114 assert (btor == btor_node_real_addr (e1)->btor);
1115
1116 BtorNode *result;
1117
1118 e0 = btor_simplify_exp (btor, e0);
1119 e1 = btor_simplify_exp (btor, e1);
1120 assert (btor_dbg_precond_shift_exp (btor, e0, e1));
1121
1122 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
1123 result = btor_rewrite_binary_exp (btor, BTOR_BV_SLL_NODE, e0, e1);
1124 else
1125 result = btor_node_create_bv_sll (btor, e0, e1);
1126
1127 assert (result);
1128 return result;
1129 }
1130
1131 BtorNode *
btor_exp_bv_srl(Btor * btor,BtorNode * e0,BtorNode * e1)1132 btor_exp_bv_srl (Btor *btor, BtorNode *e0, BtorNode *e1)
1133 {
1134 assert (btor == btor_node_real_addr (e0)->btor);
1135 assert (btor == btor_node_real_addr (e1)->btor);
1136
1137 BtorNode *result;
1138
1139 e0 = btor_simplify_exp (btor, e0);
1140 e1 = btor_simplify_exp (btor, e1);
1141 assert (btor_dbg_precond_shift_exp (btor, e0, e1));
1142
1143 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
1144 result = btor_rewrite_binary_exp (btor, BTOR_BV_SRL_NODE, e0, e1);
1145 else
1146 result = btor_node_create_bv_srl (btor, e0, e1);
1147
1148 assert (result);
1149 return result;
1150 }
1151
1152 BtorNode *
btor_exp_bv_sra(Btor * btor,BtorNode * e0,BtorNode * e1)1153 btor_exp_bv_sra (Btor *btor, BtorNode *e0, BtorNode *e1)
1154 {
1155 assert (btor == btor_node_real_addr (e0)->btor);
1156 assert (btor == btor_node_real_addr (e1)->btor);
1157
1158 BtorNode *result, *sign_e1, *srl1, *srl2;
1159 uint32_t width;
1160
1161 e0 = btor_simplify_exp (btor, e0);
1162 e1 = btor_simplify_exp (btor, e1);
1163 assert (btor_dbg_precond_shift_exp (btor, e0, e1));
1164
1165 width = btor_node_bv_get_width (btor, e0);
1166 sign_e1 = btor_exp_bv_slice (btor, e0, width - 1, width - 1);
1167 srl1 = btor_exp_bv_srl (btor, e0, e1);
1168 srl2 = btor_exp_bv_srl (btor, btor_node_invert (e0), e1);
1169 result = btor_exp_cond (btor, sign_e1, btor_node_invert (srl2), srl1);
1170 btor_node_release (btor, sign_e1);
1171 btor_node_release (btor, srl1);
1172 btor_node_release (btor, srl2);
1173 return result;
1174 }
1175
1176 static BtorNode *
exp_rotate(Btor * btor,BtorNode * e0,BtorNode * e1,bool left)1177 exp_rotate (Btor *btor, BtorNode *e0, BtorNode *e1, bool left)
1178 {
1179 assert (btor);
1180 assert (e0);
1181 assert (e1);
1182 assert (btor == btor_node_real_addr (e0)->btor);
1183 assert (btor == btor_node_real_addr (e1)->btor);
1184
1185 uint32_t width;
1186 BtorNode *w, *nbits, *dbits, *cond, *zero, *lshift, *rshift, *rot;
1187 BtorNode *res;
1188 BtorSortId sort;
1189
1190 e0 = btor_simplify_exp (btor, e0);
1191 e1 = btor_simplify_exp (btor, e1);
1192 assert (btor_dbg_precond_shift_exp (btor, e0, e1));
1193
1194 width = btor_node_bv_get_width (btor, e0);
1195 assert (width > 0);
1196 if (width == 1) return btor_node_copy (btor, e0);
1197
1198 /* actual number of bits to rotate is e1 % width */
1199 sort = btor_node_get_sort_id (e0);
1200 w = btor_exp_bv_unsigned (btor, width, sort);
1201 nbits = btor_exp_bv_urem (btor, e1, w);
1202 dbits = btor_exp_bv_sub (btor, w, nbits); /* width - nbits */
1203
1204 /* rotate left: (e0 << nbits) | (e0 >> (dbits))
1205 * rotate right: (e0 >> nbits) | (e0 << (dbits)) */
1206 if (left)
1207 {
1208 lshift = btor_exp_bv_sll (btor, e0, nbits);
1209 rshift = btor_exp_bv_srl (btor, e0, dbits);
1210 }
1211 else
1212 {
1213 lshift = btor_exp_bv_sll (btor, e0, dbits);
1214 rshift = btor_exp_bv_srl (btor, e0, nbits);
1215 }
1216 rot = btor_exp_bv_or (btor, lshift, rshift);
1217
1218 /* if nbits == 0 -> exp, else we have to rotate */
1219 zero = btor_exp_bv_zero (btor, sort);
1220 cond = btor_exp_eq (btor, nbits, zero);
1221 res = btor_exp_cond (btor, cond, e0, rot);
1222
1223 btor_node_release (btor, rot);
1224 btor_node_release (btor, rshift);
1225 btor_node_release (btor, lshift);
1226 btor_node_release (btor, zero);
1227 btor_node_release (btor, cond);
1228 btor_node_release (btor, dbits);
1229 btor_node_release (btor, nbits);
1230 btor_node_release (btor, w);
1231 return res;
1232 }
1233
1234 BtorNode *
btor_exp_bv_rol(Btor * btor,BtorNode * e0,BtorNode * e1)1235 btor_exp_bv_rol (Btor *btor, BtorNode *e0, BtorNode *e1)
1236 {
1237 return exp_rotate (btor, e0, e1, true);
1238 }
1239
1240 BtorNode *
btor_exp_bv_ror(Btor * btor,BtorNode * e0,BtorNode * e1)1241 btor_exp_bv_ror (Btor *btor, BtorNode *e0, BtorNode *e1)
1242 {
1243 return exp_rotate (btor, e0, e1, false);
1244 }
1245
1246 static BtorNode *
exp_bv_rotate_i(Btor * btor,BtorNode * exp,uint32_t nbits,bool is_left)1247 exp_bv_rotate_i (Btor *btor, BtorNode *exp, uint32_t nbits, bool is_left)
1248 {
1249 assert (btor == btor_node_real_addr (exp)->btor);
1250 BtorNode *left, *right, *res;
1251 uint32_t width;
1252
1253 width = btor_node_bv_get_width (btor, exp);
1254 assert (width > 0);
1255 nbits %= width;
1256
1257 if (nbits)
1258 {
1259 if (is_left) nbits = width - nbits;
1260
1261 assert (1 <= nbits && nbits < width);
1262
1263 left = btor_exp_bv_slice (btor, exp, nbits - 1, 0);
1264 right = btor_exp_bv_slice (btor, exp, width - 1, nbits);
1265
1266 res = btor_exp_bv_concat (btor, left, right);
1267
1268 btor_node_release (btor, left);
1269 btor_node_release (btor, right);
1270 }
1271 else
1272 {
1273 res = btor_node_copy (btor, exp);
1274 }
1275 assert (btor_node_bv_get_width (btor, res) == width);
1276 return res;
1277 }
1278
1279 BtorNode *
btor_exp_bv_roli(Btor * btor,BtorNode * exp,uint32_t nbits)1280 btor_exp_bv_roli (Btor *btor, BtorNode *exp, uint32_t nbits)
1281 {
1282 return exp_bv_rotate_i (btor, exp, nbits, true);
1283 }
1284
1285 BtorNode *
btor_exp_bv_rori(Btor * btor,BtorNode * exp,uint32_t nbits)1286 btor_exp_bv_rori (Btor *btor, BtorNode *exp, uint32_t nbits)
1287 {
1288 return exp_bv_rotate_i (btor, exp, nbits, false);
1289 }
1290
1291 BtorNode *
btor_exp_bv_sub(Btor * btor,BtorNode * e0,BtorNode * e1)1292 btor_exp_bv_sub (Btor *btor, BtorNode *e0, BtorNode *e1)
1293 {
1294 assert (btor == btor_node_real_addr (e0)->btor);
1295 assert (btor == btor_node_real_addr (e1)->btor);
1296
1297 BtorNode *result, *neg_e2;
1298
1299 e0 = btor_simplify_exp (btor, e0);
1300 e1 = btor_simplify_exp (btor, e1);
1301 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1302
1303 neg_e2 = btor_exp_bv_neg (btor, e1);
1304 result = btor_exp_bv_add (btor, e0, neg_e2);
1305 btor_node_release (btor, neg_e2);
1306 return result;
1307 }
1308
1309 BtorNode *
btor_exp_bv_usubo(Btor * btor,BtorNode * e0,BtorNode * e1)1310 btor_exp_bv_usubo (Btor *btor, BtorNode *e0, BtorNode *e1)
1311 {
1312 assert (btor == btor_node_real_addr (e0)->btor);
1313 assert (btor == btor_node_real_addr (e1)->btor);
1314
1315 BtorNode *result, *uext_e1, *uext_e2, *add1, *add2, *one;
1316 BtorSortId sort;
1317 uint32_t width;
1318
1319 e0 = btor_simplify_exp (btor, e0);
1320 e1 = btor_simplify_exp (btor, e1);
1321 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1322
1323 width = btor_node_bv_get_width (btor, e0);
1324 uext_e1 = btor_exp_bv_uext (btor, e0, 1);
1325 uext_e2 = btor_exp_bv_uext (btor, btor_node_invert (e1), 1);
1326 assert (width < INT32_MAX);
1327 sort = btor_sort_bv (btor, width + 1);
1328 one = btor_exp_bv_one (btor, sort);
1329 btor_sort_release (btor, sort);
1330 add1 = btor_exp_bv_add (btor, uext_e2, one);
1331 add2 = btor_exp_bv_add (btor, uext_e1, add1);
1332 result = btor_node_invert (btor_exp_bv_slice (btor, add2, width, width));
1333 btor_node_release (btor, uext_e1);
1334 btor_node_release (btor, uext_e2);
1335 btor_node_release (btor, add1);
1336 btor_node_release (btor, add2);
1337 btor_node_release (btor, one);
1338 return result;
1339 }
1340
1341 BtorNode *
btor_exp_bv_ssubo(Btor * btor,BtorNode * e0,BtorNode * e1)1342 btor_exp_bv_ssubo (Btor *btor, BtorNode *e0, BtorNode *e1)
1343 {
1344 assert (btor == btor_node_real_addr (e0)->btor);
1345 assert (btor == btor_node_real_addr (e1)->btor);
1346
1347 BtorNode *result, *sign_e1, *sign_e2, *sign_result;
1348 BtorNode *sub, *and1, *and2, *or1, *or2;
1349 uint32_t width;
1350
1351 e0 = btor_simplify_exp (btor, e0);
1352 e1 = btor_simplify_exp (btor, e1);
1353 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1354
1355 width = btor_node_bv_get_width (btor, e0);
1356 sign_e1 = btor_exp_bv_slice (btor, e0, width - 1, width - 1);
1357 sign_e2 = btor_exp_bv_slice (btor, e1, width - 1, width - 1);
1358 sub = btor_exp_bv_sub (btor, e0, e1);
1359 sign_result = btor_exp_bv_slice (btor, sub, width - 1, width - 1);
1360 and1 = btor_exp_bv_and (btor, btor_node_invert (sign_e1), sign_e2);
1361 or1 = btor_exp_bv_and (btor, and1, sign_result);
1362 and2 = btor_exp_bv_and (btor, sign_e1, btor_node_invert (sign_e2));
1363 or2 = btor_exp_bv_and (btor, and2, btor_node_invert (sign_result));
1364 result = btor_exp_bv_or (btor, or1, or2);
1365 btor_node_release (btor, and1);
1366 btor_node_release (btor, and2);
1367 btor_node_release (btor, or1);
1368 btor_node_release (btor, or2);
1369 btor_node_release (btor, sub);
1370 btor_node_release (btor, sign_e1);
1371 btor_node_release (btor, sign_e2);
1372 btor_node_release (btor, sign_result);
1373 return result;
1374 }
1375
1376 BtorNode *
btor_exp_bv_udiv(Btor * btor,BtorNode * e0,BtorNode * e1)1377 btor_exp_bv_udiv (Btor *btor, BtorNode *e0, BtorNode *e1)
1378 {
1379 assert (btor == btor_node_real_addr (e0)->btor);
1380 assert (btor == btor_node_real_addr (e1)->btor);
1381
1382 BtorNode *result;
1383
1384 e0 = btor_simplify_exp (btor, e0);
1385 e1 = btor_simplify_exp (btor, e1);
1386 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1387
1388 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
1389 result = btor_rewrite_binary_exp (btor, BTOR_BV_UDIV_NODE, e0, e1);
1390 else
1391 result = btor_node_create_bv_udiv (btor, e0, e1);
1392
1393 assert (result);
1394 return result;
1395 }
1396
1397 BtorNode *
btor_exp_bv_sdiv(Btor * btor,BtorNode * e0,BtorNode * e1)1398 btor_exp_bv_sdiv (Btor *btor, BtorNode *e0, BtorNode *e1)
1399 {
1400 assert (btor == btor_node_real_addr (e0)->btor);
1401 assert (btor == btor_node_real_addr (e1)->btor);
1402
1403 BtorNode *result, *sign_e1, *sign_e2, *xor, *neg_e1, *neg_e2;
1404 BtorNode *cond_e1, *cond_e2, *udiv, *neg_udiv;
1405 uint32_t width;
1406
1407 e0 = btor_simplify_exp (btor, e0);
1408 e1 = btor_simplify_exp (btor, e1);
1409 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1410
1411 width = btor_node_bv_get_width (btor, e0);
1412
1413 if (width == 1)
1414 return btor_node_invert (btor_exp_bv_and (btor, btor_node_invert (e0), e1));
1415
1416 sign_e1 = btor_exp_bv_slice (btor, e0, width - 1, width - 1);
1417 sign_e2 = btor_exp_bv_slice (btor, e1, width - 1, width - 1);
1418 /* xor: must result be signed? */
1419 xor = btor_exp_bv_xor (btor, sign_e1, sign_e2);
1420 neg_e1 = btor_exp_bv_neg (btor, e0);
1421 neg_e2 = btor_exp_bv_neg (btor, e1);
1422 /* normalize e0 and e1 if necessary */
1423 cond_e1 = btor_exp_cond (btor, sign_e1, neg_e1, e0);
1424 cond_e2 = btor_exp_cond (btor, sign_e2, neg_e2, e1);
1425 udiv = btor_exp_bv_udiv (btor, cond_e1, cond_e2);
1426 neg_udiv = btor_exp_bv_neg (btor, udiv);
1427 /* sign result if necessary */
1428 result = btor_exp_cond (btor, xor, neg_udiv, udiv);
1429 btor_node_release (btor, sign_e1);
1430 btor_node_release (btor, sign_e2);
1431 btor_node_release (btor, xor);
1432 btor_node_release (btor, neg_e1);
1433 btor_node_release (btor, neg_e2);
1434 btor_node_release (btor, cond_e1);
1435 btor_node_release (btor, cond_e2);
1436 btor_node_release (btor, udiv);
1437 btor_node_release (btor, neg_udiv);
1438 return result;
1439 }
1440
1441 BtorNode *
btor_exp_bv_sdivo(Btor * btor,BtorNode * e0,BtorNode * e1)1442 btor_exp_bv_sdivo (Btor *btor, BtorNode *e0, BtorNode *e1)
1443 {
1444 assert (btor == btor_node_real_addr (e0)->btor);
1445 assert (btor == btor_node_real_addr (e1)->btor);
1446
1447 BtorNode *result, *int_min, *ones, *eq1, *eq2;
1448
1449 e0 = btor_simplify_exp (btor, e0);
1450 e1 = btor_simplify_exp (btor, e1);
1451 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1452
1453 int_min = int_min_exp (btor, btor_node_bv_get_width (btor, e0));
1454 ones = btor_exp_bv_ones (btor, btor_node_get_sort_id (e1));
1455 eq1 = btor_exp_eq (btor, e0, int_min);
1456 eq2 = btor_exp_eq (btor, e1, ones);
1457 result = btor_exp_bv_and (btor, eq1, eq2);
1458 btor_node_release (btor, int_min);
1459 btor_node_release (btor, ones);
1460 btor_node_release (btor, eq1);
1461 btor_node_release (btor, eq2);
1462 return result;
1463 }
1464
1465 BtorNode *
btor_exp_bv_urem(Btor * btor,BtorNode * e0,BtorNode * e1)1466 btor_exp_bv_urem (Btor *btor, BtorNode *e0, BtorNode *e1)
1467 {
1468 assert (btor == btor_node_real_addr (e0)->btor);
1469 assert (btor == btor_node_real_addr (e1)->btor);
1470
1471 BtorNode *result;
1472
1473 e0 = btor_simplify_exp (btor, e0);
1474 e1 = btor_simplify_exp (btor, e1);
1475 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1476
1477 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
1478 result = btor_rewrite_binary_exp (btor, BTOR_BV_UREM_NODE, e0, e1);
1479 else
1480 result = btor_node_create_bv_urem (btor, e0, e1);
1481
1482 assert (result);
1483 return result;
1484 }
1485
1486 BtorNode *
btor_exp_bv_srem(Btor * btor,BtorNode * e0,BtorNode * e1)1487 btor_exp_bv_srem (Btor *btor, BtorNode *e0, BtorNode *e1)
1488 {
1489 assert (btor == btor_node_real_addr (e0)->btor);
1490 assert (btor == btor_node_real_addr (e1)->btor);
1491
1492 BtorNode *result, *sign_e0, *sign_e1, *neg_e0, *neg_e1;
1493 BtorNode *cond_e0, *cond_e1, *urem, *neg_urem;
1494 uint32_t width;
1495
1496 e0 = btor_simplify_exp (btor, e0);
1497 e1 = btor_simplify_exp (btor, e1);
1498 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1499
1500 width = btor_node_bv_get_width (btor, e0);
1501
1502 if (width == 1) return btor_exp_bv_and (btor, e0, btor_node_invert (e1));
1503
1504 sign_e0 = btor_exp_bv_slice (btor, e0, width - 1, width - 1);
1505 sign_e1 = btor_exp_bv_slice (btor, e1, width - 1, width - 1);
1506 neg_e0 = btor_exp_bv_neg (btor, e0);
1507 neg_e1 = btor_exp_bv_neg (btor, e1);
1508 /* normalize e0 and e1 if necessary */
1509 cond_e0 = btor_exp_cond (btor, sign_e0, neg_e0, e0);
1510 cond_e1 = btor_exp_cond (btor, sign_e1, neg_e1, e1);
1511 urem = btor_exp_bv_urem (btor, cond_e0, cond_e1);
1512 neg_urem = btor_exp_bv_neg (btor, urem);
1513 /* sign result if necessary */
1514 /* result is negative if e0 is negative */
1515 result = btor_exp_cond (btor, sign_e0, neg_urem, urem);
1516 btor_node_release (btor, sign_e0);
1517 btor_node_release (btor, sign_e1);
1518 btor_node_release (btor, neg_e0);
1519 btor_node_release (btor, neg_e1);
1520 btor_node_release (btor, cond_e0);
1521 btor_node_release (btor, cond_e1);
1522 btor_node_release (btor, urem);
1523 btor_node_release (btor, neg_urem);
1524 return result;
1525 }
1526
1527 BtorNode *
btor_exp_bv_smod(Btor * btor,BtorNode * e0,BtorNode * e1)1528 btor_exp_bv_smod (Btor *btor, BtorNode *e0, BtorNode *e1)
1529 {
1530 assert (btor == btor_node_real_addr (e0)->btor);
1531 assert (btor == btor_node_real_addr (e1)->btor);
1532
1533 BtorNode *result, *sign_e0, *sign_e1, *neg_e0, *neg_e1, *cond_e0, *cond_e1;
1534 BtorNode *neg_e0_and_e1, *neg_e0_and_neg_e1, *zero, *e0_zero;
1535 BtorNode *neg_urem, *add1, *add2, *or1, *or2, *e0_and_e1, *e0_and_neg_e1;
1536 BtorNode *cond_case1, *cond_case2, *cond_case3, *cond_case4, *urem;
1537 BtorNode *urem_zero, *gadd1, *gadd2;
1538 uint32_t width;
1539
1540 e0 = btor_simplify_exp (btor, e0);
1541 e1 = btor_simplify_exp (btor, e1);
1542 assert (btor_dbg_precond_regular_binary_bv_exp (btor, e0, e1));
1543
1544 width = btor_node_bv_get_width (btor, e0);
1545 zero = btor_exp_bv_zero (btor, btor_node_get_sort_id (e0));
1546 e0_zero = btor_exp_eq (btor, zero, e0);
1547 sign_e0 = btor_exp_bv_slice (btor, e0, width - 1, width - 1);
1548 sign_e1 = btor_exp_bv_slice (btor, e1, width - 1, width - 1);
1549 neg_e0 = btor_exp_bv_neg (btor, e0);
1550 neg_e1 = btor_exp_bv_neg (btor, e1);
1551 e0_and_e1 = btor_exp_bv_and (
1552 btor, btor_node_invert (sign_e0), btor_node_invert (sign_e1));
1553 e0_and_neg_e1 = btor_exp_bv_and (btor, btor_node_invert (sign_e0), sign_e1);
1554 neg_e0_and_e1 = btor_exp_bv_and (btor, sign_e0, btor_node_invert (sign_e1));
1555 neg_e0_and_neg_e1 = btor_exp_bv_and (btor, sign_e0, sign_e1);
1556 /* normalize e0 and e1 if necessary */
1557 cond_e0 = btor_exp_cond (btor, sign_e0, neg_e0, e0);
1558 cond_e1 = btor_exp_cond (btor, sign_e1, neg_e1, e1);
1559 urem = btor_exp_bv_urem (btor, cond_e0, cond_e1);
1560 urem_zero = btor_exp_eq (btor, urem, zero);
1561 neg_urem = btor_exp_bv_neg (btor, urem);
1562 add1 = btor_exp_bv_add (btor, neg_urem, e1);
1563 add2 = btor_exp_bv_add (btor, urem, e1);
1564 gadd1 = btor_exp_cond (btor, urem_zero, zero, add1);
1565 gadd2 = btor_exp_cond (btor, urem_zero, zero, add2);
1566 cond_case1 = btor_exp_cond (btor, e0_and_e1, urem, zero);
1567 cond_case2 = btor_exp_cond (btor, neg_e0_and_e1, gadd1, zero);
1568 cond_case3 = btor_exp_cond (btor, e0_and_neg_e1, gadd2, zero);
1569 cond_case4 = btor_exp_cond (btor, neg_e0_and_neg_e1, neg_urem, zero);
1570 or1 = btor_exp_bv_or (btor, cond_case1, cond_case2);
1571 or2 = btor_exp_bv_or (btor, cond_case3, cond_case4);
1572 result = btor_exp_bv_or (btor, or1, or2);
1573 btor_node_release (btor, zero);
1574 btor_node_release (btor, e0_zero);
1575 btor_node_release (btor, sign_e0);
1576 btor_node_release (btor, sign_e1);
1577 btor_node_release (btor, neg_e0);
1578 btor_node_release (btor, neg_e1);
1579 btor_node_release (btor, cond_e0);
1580 btor_node_release (btor, cond_e1);
1581 btor_node_release (btor, urem_zero);
1582 btor_node_release (btor, cond_case1);
1583 btor_node_release (btor, cond_case2);
1584 btor_node_release (btor, cond_case3);
1585 btor_node_release (btor, cond_case4);
1586 btor_node_release (btor, urem);
1587 btor_node_release (btor, neg_urem);
1588 btor_node_release (btor, add1);
1589 btor_node_release (btor, add2);
1590 btor_node_release (btor, gadd1);
1591 btor_node_release (btor, gadd2);
1592 btor_node_release (btor, or1);
1593 btor_node_release (btor, or2);
1594 btor_node_release (btor, e0_and_e1);
1595 btor_node_release (btor, neg_e0_and_e1);
1596 btor_node_release (btor, e0_and_neg_e1);
1597 btor_node_release (btor, neg_e0_and_neg_e1);
1598 return result;
1599 }
1600
1601 BtorNode *
btor_exp_bv_concat(Btor * btor,BtorNode * e0,BtorNode * e1)1602 btor_exp_bv_concat (Btor *btor, BtorNode *e0, BtorNode *e1)
1603 {
1604 assert (btor == btor_node_real_addr (e0)->btor);
1605 assert (btor == btor_node_real_addr (e1)->btor);
1606
1607 BtorNode *result;
1608
1609 e0 = btor_simplify_exp (btor, e0);
1610 e1 = btor_simplify_exp (btor, e1);
1611 assert (btor_dbg_precond_concat_exp (btor, e0, e1));
1612
1613 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
1614 result = btor_rewrite_binary_exp (btor, BTOR_BV_CONCAT_NODE, e0, e1);
1615 else
1616 result = btor_node_create_bv_concat (btor, e0, e1);
1617
1618 assert (result);
1619 return result;
1620 }
1621
1622 BtorNode *
btor_exp_bv_repeat(Btor * btor,BtorNode * exp,uint32_t n)1623 btor_exp_bv_repeat (Btor *btor, BtorNode *exp, uint32_t n)
1624 {
1625 assert (btor == btor_node_real_addr (exp)->btor);
1626 assert (((uint32_t) UINT32_MAX / n) >= btor_node_bv_get_width (btor, exp));
1627
1628 BtorNode *result, *tmp;
1629 uint32_t i;
1630
1631 result = btor_node_copy (btor, exp);
1632 for (i = 1; i < n; i++)
1633 {
1634 tmp = result;
1635 result = btor_exp_bv_concat (btor, tmp, exp);
1636 btor_node_release (btor, tmp);
1637 }
1638 assert (result);
1639 return result;
1640 }
1641
1642 BtorNode *
btor_exp_bv_inc(Btor * btor,BtorNode * exp)1643 btor_exp_bv_inc (Btor *btor, BtorNode *exp)
1644 {
1645 BtorNode *one, *result;
1646
1647 exp = btor_simplify_exp (btor, exp);
1648 assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
1649
1650 one = btor_exp_bv_one (btor, btor_node_get_sort_id (exp));
1651 result = btor_exp_bv_add (btor, exp, one);
1652 btor_node_release (btor, one);
1653 return result;
1654 }
1655
1656 BtorNode *
btor_exp_bv_dec(Btor * btor,BtorNode * exp)1657 btor_exp_bv_dec (Btor *btor, BtorNode *exp)
1658 {
1659 assert (btor == btor_node_real_addr (exp)->btor);
1660
1661 BtorNode *one, *result;
1662
1663 exp = btor_simplify_exp (btor, exp);
1664 assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
1665
1666 one = btor_exp_bv_one (btor, btor_node_get_sort_id (exp));
1667 result = btor_exp_bv_sub (btor, exp, one);
1668 btor_node_release (btor, one);
1669 return result;
1670 }
1671
1672 /*------------------------------------------------------------------------*/
1673
1674 BtorNode *
btor_exp_read(Btor * btor,BtorNode * e_array,BtorNode * e_index)1675 btor_exp_read (Btor *btor, BtorNode *e_array, BtorNode *e_index)
1676 {
1677 assert (btor == btor_node_real_addr (e_array)->btor);
1678 assert (btor == btor_node_real_addr (e_index)->btor);
1679
1680 e_array = btor_simplify_exp (btor, e_array);
1681 e_index = btor_simplify_exp (btor, e_index);
1682 assert (btor_dbg_precond_read_exp (btor, e_array, e_index));
1683 return btor_exp_apply_n (btor, e_array, &e_index, 1);
1684 }
1685
1686 BtorNode *
btor_exp_write(Btor * btor,BtorNode * e_array,BtorNode * e_index,BtorNode * e_value)1687 btor_exp_write (Btor *btor,
1688 BtorNode *e_array,
1689 BtorNode *e_index,
1690 BtorNode *e_value)
1691 {
1692 assert (btor);
1693 assert (btor_node_is_array (btor_simplify_exp (btor, e_array)));
1694 assert (btor == btor_node_real_addr (e_array)->btor);
1695 assert (btor == btor_node_real_addr (e_index)->btor);
1696 assert (btor == btor_node_real_addr (e_value)->btor);
1697
1698 e_array = btor_simplify_exp (btor, e_array);
1699 e_index = btor_simplify_exp (btor, e_index);
1700 e_value = btor_simplify_exp (btor, e_value);
1701 assert (btor_dbg_precond_write_exp (btor, e_array, e_index, e_value));
1702
1703 if (btor_opt_get (btor, BTOR_OPT_FUN_STORE_LAMBDAS)
1704 || btor_node_real_addr (e_index)->parameterized
1705 || btor_node_real_addr (e_value)->parameterized)
1706 {
1707 return btor_exp_lambda_write (btor, e_array, e_index, e_value);
1708 }
1709 else
1710 {
1711 BtorNode *args = btor_exp_args (btor, &e_index, 1);
1712 BtorNode *res = btor_exp_update (btor, e_array, args, e_value);
1713 btor_node_release (btor, args);
1714 res->is_array = 1;
1715 return res;
1716 }
1717 }
1718
1719 /*------------------------------------------------------------------------*/
1720
1721 BtorNode *
btor_exp_fun(Btor * btor,BtorNode * params[],uint32_t paramc,BtorNode * exp)1722 btor_exp_fun (Btor *btor, BtorNode *params[], uint32_t paramc, BtorNode *exp)
1723 {
1724 assert (btor);
1725 assert (paramc > 0);
1726 assert (params);
1727 assert (exp);
1728 assert (btor == btor_node_real_addr (exp)->btor);
1729 assert (!btor_node_is_uf (exp));
1730
1731 uint32_t i, j;
1732 BtorNode *fun = btor_simplify_exp (btor, exp);
1733 BtorNode *prev_fun = 0;
1734
1735 for (i = 1; i <= paramc; i++)
1736 {
1737 j = paramc - i;
1738 assert (params[j]);
1739 assert (btor == btor_node_real_addr (params[j])->btor);
1740 assert (btor_node_is_param (params[j]));
1741 fun = btor_exp_lambda (btor, params[j], fun);
1742 if (prev_fun) btor_node_release (btor, prev_fun);
1743 prev_fun = fun;
1744 }
1745
1746 return fun;
1747 }
1748
1749 BtorNode *
btor_exp_apply(Btor * btor,BtorNode * fun,BtorNode * args)1750 btor_exp_apply (Btor *btor, BtorNode *fun, BtorNode *args)
1751 {
1752 assert (btor);
1753 assert (fun);
1754 assert (args);
1755 assert (btor == btor_node_real_addr (fun)->btor);
1756 assert (btor == btor_node_real_addr (args)->btor);
1757
1758 fun = btor_simplify_exp (btor, fun);
1759 args = btor_simplify_exp (btor, args);
1760 assert (btor_node_is_fun (fun));
1761 assert (btor_node_is_args (args));
1762
1763 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
1764 return btor_rewrite_binary_exp (btor, BTOR_APPLY_NODE, fun, args);
1765
1766 return btor_node_create_apply (btor, fun, args);
1767 }
1768
1769 BtorNode *
btor_exp_apply_n(Btor * btor,BtorNode * fun,BtorNode * args[],uint32_t argc)1770 btor_exp_apply_n (Btor *btor, BtorNode *fun, BtorNode *args[], uint32_t argc)
1771 {
1772 assert (btor);
1773 assert (argc > 0);
1774 assert (args);
1775 assert (fun);
1776
1777 BtorNode *exp, *_args;
1778
1779 _args = btor_exp_args (btor, args, argc);
1780 fun = btor_simplify_exp (btor, fun);
1781 _args = btor_simplify_exp (btor, _args);
1782
1783 exp = btor_exp_apply (btor, fun, _args);
1784 btor_node_release (btor, _args);
1785
1786 return exp;
1787 }
1788
1789 BtorNode *
btor_exp_args(Btor * btor,BtorNode * args[],uint32_t argc)1790 btor_exp_args (Btor *btor, BtorNode *args[], uint32_t argc)
1791 {
1792 return btor_node_create_args (btor, args, argc);
1793 }
1794
1795 BtorNode *
btor_exp_update(Btor * btor,BtorNode * fun,BtorNode * args,BtorNode * value)1796 btor_exp_update (Btor *btor, BtorNode *fun, BtorNode *args, BtorNode *value)
1797 {
1798 return btor_node_create_update (btor, fun, args, value);
1799 }
1800
1801 BtorNode *
btor_exp_lambda(Btor * btor,BtorNode * e_param,BtorNode * e_exp)1802 btor_exp_lambda (Btor *btor, BtorNode *e_param, BtorNode *e_exp)
1803 {
1804 assert (btor);
1805 assert (btor_node_is_regular (e_param));
1806 assert (btor == e_param->btor);
1807 assert (btor_node_is_param (e_param));
1808 assert (e_exp);
1809 assert (btor == btor_node_real_addr (e_exp)->btor);
1810
1811 e_param = btor_simplify_exp (btor, e_param);
1812 e_exp = btor_simplify_exp (btor, e_exp);
1813
1814 BtorNode *result;
1815 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
1816 result = btor_rewrite_binary_exp (btor, BTOR_LAMBDA_NODE, e_param, e_exp);
1817 else
1818 result = btor_node_create_lambda (btor, e_param, e_exp);
1819 assert (btor_node_is_fun (result));
1820 return result;
1821 }
1822
1823 BtorNode *
btor_exp_lambda_write(Btor * btor,BtorNode * e_array,BtorNode * e_index,BtorNode * e_value)1824 btor_exp_lambda_write (Btor *btor,
1825 BtorNode *e_array,
1826 BtorNode *e_index,
1827 BtorNode *e_value)
1828 {
1829 BtorNode *param, *e_cond, *e_if, *e_else, *bvcond, *args;
1830 BtorLambdaNode *lambda;
1831 BtorPtrHashBucket *b;
1832
1833 param = btor_exp_param (btor, btor_node_get_sort_id (e_index), 0);
1834 e_cond = btor_exp_eq (btor, param, e_index);
1835 e_if = btor_node_copy (btor, e_value);
1836 e_else = btor_exp_read (btor, e_array, param);
1837 bvcond = btor_exp_cond (btor, e_cond, e_if, e_else);
1838 lambda = (BtorLambdaNode *) btor_exp_lambda (btor, param, bvcond);
1839 if (!lambda->static_rho)
1840 {
1841 lambda->static_rho =
1842 btor_hashptr_table_new (btor->mm,
1843 (BtorHashPtr) btor_node_hash_by_id,
1844 (BtorCmpPtr) btor_node_compare_by_id);
1845 args = btor_exp_args (btor, &e_index, 1);
1846 b = btor_hashptr_table_add (lambda->static_rho, args);
1847 b->data.as_ptr = btor_node_copy (btor, e_value);
1848 }
1849 btor_node_release (btor, e_if);
1850 btor_node_release (btor, e_else);
1851 btor_node_release (btor, e_cond);
1852 btor_node_release (btor, bvcond);
1853 btor_node_release (btor, param);
1854
1855 lambda->is_array = 1;
1856 return (BtorNode *) lambda;
1857 }
1858
1859 /*------------------------------------------------------------------------*/
1860
1861 static BtorNode *
quantifier_exp(Btor * btor,BtorNodeKind kind,BtorNode * param,BtorNode * body)1862 quantifier_exp (Btor *btor, BtorNodeKind kind, BtorNode *param, BtorNode *body)
1863 {
1864 assert (btor);
1865 assert (kind == BTOR_FORALL_NODE || kind == BTOR_EXISTS_NODE);
1866 assert (param);
1867
1868 param = btor_simplify_exp (btor, param);
1869 body = btor_simplify_exp (btor, body);
1870
1871 assert (btor_node_is_regular (param));
1872 assert (btor_node_is_param (param));
1873 assert (body);
1874 assert (btor_sort_is_bool (btor, btor_node_real_addr (body)->sort_id));
1875 if (btor_opt_get (btor, BTOR_OPT_REWRITE_LEVEL) > 0)
1876 return btor_rewrite_binary_exp (btor, kind, param, body);
1877 return btor_node_create_quantifier (btor, kind, param, body);
1878 }
1879
1880 static BtorNode *
quantifier_n_exp(Btor * btor,BtorNodeKind kind,BtorNode * params[],uint32_t n,BtorNode * body)1881 quantifier_n_exp (Btor *btor,
1882 BtorNodeKind kind,
1883 BtorNode *params[],
1884 uint32_t n,
1885 BtorNode *body)
1886 {
1887 assert (btor);
1888 assert (kind == BTOR_FORALL_NODE || kind == BTOR_EXISTS_NODE);
1889 assert (params);
1890 assert (n > 0);
1891 assert (body);
1892 assert (btor == btor_node_real_addr (body)->btor);
1893
1894 uint32_t i, j;
1895 BtorNode *res, *tmp;
1896
1897 res = btor_node_copy (btor, body);
1898 for (j = 1, i = n - 1; j <= n; j++, i--)
1899 {
1900 assert (params[i]);
1901 assert (btor == btor_node_real_addr (params[i])->btor);
1902 assert (btor_node_is_param (params[i]));
1903 tmp = quantifier_exp (btor, kind, params[i], res);
1904 btor_node_release (btor, res);
1905 res = tmp;
1906 }
1907 return res;
1908 }
1909
1910 BtorNode *
btor_exp_forall(Btor * btor,BtorNode * param,BtorNode * body)1911 btor_exp_forall (Btor *btor, BtorNode *param, BtorNode *body)
1912 {
1913 return quantifier_exp (btor, BTOR_FORALL_NODE, param, body);
1914 }
1915
1916 BtorNode *
btor_exp_forall_n(Btor * btor,BtorNode * params[],uint32_t n,BtorNode * body)1917 btor_exp_forall_n (Btor *btor, BtorNode *params[], uint32_t n, BtorNode *body)
1918 {
1919 return quantifier_n_exp (btor, BTOR_FORALL_NODE, params, n, body);
1920 }
1921
1922 BtorNode *
btor_exp_exists(Btor * btor,BtorNode * param,BtorNode * body)1923 btor_exp_exists (Btor *btor, BtorNode *param, BtorNode *body)
1924 {
1925 return quantifier_exp (btor, BTOR_EXISTS_NODE, param, body);
1926 }
1927
1928 BtorNode *
btor_exp_exists_n(Btor * btor,BtorNode * params[],uint32_t n,BtorNode * body)1929 btor_exp_exists_n (Btor *btor, BtorNode *params[], uint32_t n, BtorNode *body)
1930 {
1931 return quantifier_n_exp (btor, BTOR_EXISTS_NODE, params, n, body);
1932 }
1933
1934