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 "btorsort.h"
10
11 #include "btorabort.h"
12 #include "btorcore.h"
13 #include "btornode.h"
14 #include "utils/btorutil.h"
15
16 #include <assert.h>
17 #include <limits.h>
18 #include <stdio.h>
19
20 #define BTOR_SORT_UNIQUE_TABLE_LIMIT 30
21
22 #define BTOR_FULL_SORT_UNIQUE_TABLE(table) \
23 ((table)->num_elements >= (table)->size \
24 && btor_util_log_2 ((table)->size) < BTOR_SORT_UNIQUE_TABLE_LIMIT)
25
26 static void
inc_sort_ref_counter(BtorSort * sort)27 inc_sort_ref_counter (BtorSort *sort)
28 {
29 assert (sort);
30 BTOR_ABORT (sort->refs == INT32_MAX, "Sort reference counter overflow");
31 sort->refs++;
32 }
33
34 static uint32_t
compute_hash_sort(const BtorSort * sort,uint32_t table_size)35 compute_hash_sort (const BtorSort *sort, uint32_t table_size)
36 {
37 assert (sort);
38 assert (table_size);
39 assert (btor_util_is_power_of_2 (table_size));
40
41 uint32_t i, res, tmp;
42
43 tmp = 0;
44
45 switch (sort->kind)
46 {
47 default:
48 #if 0
49 case BTOR_BOOL_SORT:
50 assert (sort->kind == BTOR_BOOL_SORT);
51 res = 0;
52 break;
53 #endif
54 case BTOR_BV_SORT: res = sort->bitvec.width; break;
55 #if 0
56 case BTOR_ARRAY_SORT:
57 res = sort->array.index->id;
58 tmp = sort->array.element->id;
59 break;
60
61 case BTOR_LST_SORT:
62 res = sort->lst.head->id;
63 tmp = sort->lst.tail->id;
64 break;
65 #endif
66 case BTOR_FUN_SORT:
67 res = sort->fun.domain->id;
68 tmp = sort->fun.codomain->id;
69 break;
70
71 case BTOR_TUPLE_SORT:
72 res = 0;
73 for (i = 0; i < sort->tuple.num_elements; i++)
74 {
75 if ((i & 1) == 0)
76 res += sort->tuple.elements[i]->id;
77 else
78 tmp += sort->tuple.elements[i]->id;
79 }
80 break;
81 }
82
83 res *= 444555667u;
84
85 if (tmp)
86 {
87 res += tmp;
88 res *= 123123137u;
89 }
90
91 res &= table_size - 1;
92
93 return res;
94 }
95
96 static void
remove_from_sorts_unique_table_sort(BtorSortUniqueTable * table,BtorSort * sort)97 remove_from_sorts_unique_table_sort (BtorSortUniqueTable *table, BtorSort *sort)
98 {
99 assert (table);
100 assert (sort);
101 assert (!sort->refs);
102 assert (table->num_elements > 0);
103
104 uint32_t hash;
105 BtorSort *prev, *cur;
106
107 hash = compute_hash_sort (sort, table->size);
108 prev = 0;
109 cur = table->chains[hash];
110
111 while (cur != sort)
112 {
113 assert (cur);
114 prev = cur;
115 cur = cur->next;
116 }
117
118 assert (cur);
119 if (!prev)
120 table->chains[hash] = cur->next;
121 else
122 prev->next = cur->next;
123
124 table->num_elements--;
125 }
126
127 static int32_t
equal_sort(const BtorSort * a,const BtorSort * b)128 equal_sort (const BtorSort *a, const BtorSort *b)
129 {
130 assert (a);
131 assert (b);
132
133 uint32_t i;
134
135 if (a->kind != b->kind) return 0;
136
137 switch (a->kind)
138 {
139 default:
140 #if 0
141 case BTOR_BOOL_SORT:
142 default:
143 assert (a->kind == BTOR_BOOL_SORT);
144 break;
145 #endif
146 case BTOR_BV_SORT:
147 if (a->bitvec.width != b->bitvec.width) return 0;
148 break;
149 #if 0
150 case BTOR_ARRAY_SORT:
151 if (a->array.index->id != b->array.index->id) return 0;
152 if (a->array.element->id != b->array.element->id) return 0;
153 break;
154
155 case BTOR_LST_SORT:
156 if (a->lst.head->id != b->lst.head->id) return 0;
157 if (a->lst.tail->id != b->lst.tail->id) return 0;
158 break;
159 #endif
160 case BTOR_FUN_SORT:
161 if (a->fun.domain->id != b->fun.domain->id) return 0;
162 if (a->fun.codomain->id != b->fun.codomain->id) return 0;
163 break;
164
165 case BTOR_TUPLE_SORT:
166 if (a->tuple.num_elements != b->tuple.num_elements) return 0;
167 for (i = 0; i < a->tuple.num_elements; i++)
168 if (a->tuple.elements[i]->id != b->tuple.elements[i]->id) return 0;
169 break;
170 }
171
172 return 1;
173 }
174
175 static BtorSort **
find_sort(BtorSortUniqueTable * table,const BtorSort * pattern)176 find_sort (BtorSortUniqueTable *table, const BtorSort *pattern)
177 {
178 assert (table);
179 assert (pattern);
180
181 BtorSort **res, *sort;
182 uint32_t hash;
183 hash = compute_hash_sort (pattern, table->size);
184 assert (hash < (uint32_t) table->size);
185 for (res = table->chains + hash; (sort = *res) && !equal_sort (sort, pattern);
186 res = &sort->next)
187 assert (sort->refs > 0);
188 return res;
189 }
190
191 static void
enlarge_sorts_unique_table(BtorSortUniqueTable * table)192 enlarge_sorts_unique_table (BtorSortUniqueTable *table)
193 {
194 assert (table);
195
196 BtorSort *cur, *temp, **new_chains;
197 uint32_t size, new_size, i, hash;
198 BtorMemMgr *mm;
199
200 mm = table->mm;
201 size = table->size;
202 new_size = size << 1;
203 assert (new_size / size == 2);
204 BTOR_CNEWN (mm, new_chains, new_size);
205 for (i = 0; i < size; i++)
206 {
207 cur = table->chains[i];
208 while (cur)
209 {
210 temp = cur->next;
211 hash = compute_hash_sort (cur, new_size);
212 cur->next = new_chains[hash];
213 new_chains[hash] = cur;
214 cur = temp;
215 }
216 }
217 BTOR_DELETEN (mm, table->chains, size);
218 table->size = new_size;
219 table->chains = new_chains;
220 }
221
222 static void
release_sort(BtorSortUniqueTable * table,BtorSort * sort)223 release_sort (BtorSortUniqueTable *table, BtorSort *sort)
224 {
225 assert (table);
226 assert (sort);
227 assert (sort->refs > 0);
228
229 uint32_t i;
230
231 if (--sort->refs > 0) return;
232
233 remove_from_sorts_unique_table_sort (table, sort);
234
235 switch (sort->kind)
236 {
237 default: break;
238 #if 0
239 case BTOR_LST_SORT:
240 #ifndef NDEBUG
241 sort->lst.head->parents--;
242 sort->lst.tail->parents--;
243 #endif
244 release_sort (table, sort->lst.head);
245 release_sort (table, sort->lst.tail);
246 break;
247
248 case BTOR_ARRAY_SORT:
249 #ifndef NDEBUG
250 sort->array.index->parents--;
251 sort->array.element->parents--;
252 #endif
253 release_sort (table, sort->array.index);
254 release_sort (table, sort->array.element);
255 break;
256 #endif
257 case BTOR_FUN_SORT:
258 #ifndef NDEBUG
259 sort->fun.domain->parents--;
260 sort->fun.codomain->parents--;
261 #endif
262 release_sort (table, sort->fun.domain);
263 release_sort (table, sort->fun.codomain);
264 break;
265
266 case BTOR_TUPLE_SORT:
267 for (i = 0; i < sort->tuple.num_elements; i++)
268 {
269 #ifndef NDEBUG
270 sort->tuple.elements[i]->parents--;
271 #endif
272 release_sort (table, sort->tuple.elements[i]);
273 }
274 BTOR_DELETEN (table->mm, sort->tuple.elements, sort->tuple.num_elements);
275 break;
276 }
277
278 assert (BTOR_PEEK_STACK (table->id2sort, sort->id) == sort);
279 BTOR_POKE_STACK (table->id2sort, sort->id, 0);
280 BTOR_DELETE (table->mm, sort);
281 }
282
283 BtorSort *
btor_sort_get_by_id(Btor * btor,BtorSortId id)284 btor_sort_get_by_id (Btor *btor, BtorSortId id)
285 {
286 assert (btor);
287 assert (id < BTOR_COUNT_STACK (btor->sorts_unique_table.id2sort));
288 return BTOR_PEEK_STACK (btor->sorts_unique_table.id2sort, id);
289 }
290
291 BtorSortId
btor_sort_copy(Btor * btor,BtorSortId id)292 btor_sort_copy (Btor *btor, BtorSortId id)
293 {
294 assert (btor);
295 BtorSort *sort;
296 sort = btor_sort_get_by_id (btor, id);
297 inc_sort_ref_counter (sort);
298 return id;
299 }
300
301 void
btor_sort_release(Btor * btor,BtorSortId id)302 btor_sort_release (Btor *btor, BtorSortId id)
303 {
304 assert (btor);
305
306 BtorSort *sort;
307
308 sort = btor_sort_get_by_id (btor, id);
309 assert (sort);
310 assert (sort->refs > 0);
311 release_sort (&btor->sorts_unique_table, sort);
312 }
313
314 static BtorSort *
copy_sort(BtorSort * sort)315 copy_sort (BtorSort *sort)
316 {
317 inc_sort_ref_counter (sort);
318 return sort;
319 }
320
321 static BtorSort *
create_sort(Btor * btor,BtorSortUniqueTable * table,BtorSort * pattern)322 create_sort (Btor *btor, BtorSortUniqueTable *table, BtorSort *pattern)
323 {
324 assert (table);
325 assert (pattern);
326
327 uint32_t i;
328 BtorSort *res;
329
330 BTOR_CNEW (table->mm, res);
331
332 #ifndef NDEBUG
333 res->btor = btor;
334 #else
335 (void) btor;
336 #endif
337
338 switch (pattern->kind)
339 {
340 #if 0
341 case BTOR_BOOL_SORT:
342 res->kind = BTOR_BOOL_SORT;
343 break;
344 #endif
345 case BTOR_BV_SORT:
346 res->kind = BTOR_BV_SORT;
347 res->bitvec.width = pattern->bitvec.width;
348 break;
349 #if 0
350 case BTOR_ARRAY_SORT:
351 res->kind = BTOR_ARRAY_SORT;
352 res->array.index = copy_sort (pattern->array.index);
353 res->array.element = copy_sort (pattern->array.element);
354 #ifndef NDEBUG
355 res->array.index->parents++;
356 res->array.element->parents++;
357 #endif
358 break;
359
360 case BTOR_LST_SORT:
361 res->kind = BTOR_LST_SORT;
362 res->lst.head = copy_sort (pattern->lst.head);
363 res->lst.tail = copy_sort (pattern->lst.tail);
364 #ifndef NDEBUG
365 res->lst.head->parents++;
366 res->lst.tail->parents++;
367 #endif
368 break;
369 #endif
370 case BTOR_FUN_SORT:
371 res->kind = BTOR_FUN_SORT;
372 res->fun.domain = copy_sort (pattern->fun.domain);
373 res->fun.codomain = copy_sort (pattern->fun.codomain);
374 #ifndef NDEBUG
375 res->fun.domain->parents++;
376 res->fun.codomain->parents++;
377 #endif
378 break;
379
380 case BTOR_TUPLE_SORT:
381 res->kind = BTOR_TUPLE_SORT;
382 res->tuple.num_elements = pattern->tuple.num_elements;
383 BTOR_NEWN (table->mm, res->tuple.elements, res->tuple.num_elements);
384 for (i = 0; i < res->tuple.num_elements; i++)
385 {
386 res->tuple.elements[i] = copy_sort (pattern->tuple.elements[i]);
387 #ifndef NDEBUG
388 res->tuple.elements[i]->parents++;
389 #endif
390 }
391 break;
392
393 default: break;
394 }
395 assert (res->kind);
396 res->id = BTOR_COUNT_STACK (table->id2sort);
397 BTOR_PUSH_STACK (table->id2sort, res);
398 assert (BTOR_COUNT_STACK (table->id2sort) == res->id + 1);
399 assert (BTOR_PEEK_STACK (table->id2sort, res->id) == res);
400
401 table->num_elements++;
402 res->table = table;
403
404 return res;
405 }
406
407 BtorSortId
btor_sort_bool(Btor * btor)408 btor_sort_bool (Btor *btor)
409 {
410 return btor_sort_bv (btor, 1);
411 }
412
413 BtorSortId
btor_sort_bv(Btor * btor,uint32_t width)414 btor_sort_bv (Btor *btor, uint32_t width)
415 {
416 assert (btor);
417 assert (width > 0);
418
419 BtorSort *res, **pos, pattern;
420 BtorSortUniqueTable *table;
421
422 table = &btor->sorts_unique_table;
423
424 BTOR_CLR (&pattern);
425 pattern.kind = BTOR_BV_SORT;
426 pattern.bitvec.width = width;
427 pos = find_sort (table, &pattern);
428 assert (pos);
429 res = *pos;
430 if (!res)
431 {
432 if (BTOR_FULL_SORT_UNIQUE_TABLE (table))
433 {
434 enlarge_sorts_unique_table (table);
435 pos = find_sort (table, &pattern);
436 assert (pos);
437 res = *pos;
438 assert (!res);
439 }
440 res = create_sort (btor, table, &pattern);
441 *pos = res;
442 }
443 inc_sort_ref_counter (res);
444 return res->id;
445 }
446
447 BtorSortId
btor_sort_array(Btor * btor,BtorSortId index_id,BtorSortId element_id)448 btor_sort_array (Btor *btor, BtorSortId index_id, BtorSortId element_id)
449 {
450 assert (btor);
451 assert (index_id < BTOR_COUNT_STACK (btor->sorts_unique_table.id2sort));
452 assert (element_id < BTOR_COUNT_STACK (btor->sorts_unique_table.id2sort));
453
454 BtorSortId tup, res;
455 BtorSort *s;
456
457 tup = btor_sort_tuple (btor, &index_id, 1);
458 res = btor_sort_fun (btor, tup, element_id);
459 btor_sort_release (btor, tup);
460 s = btor_sort_get_by_id (btor, res);
461 s->fun.is_array = true;
462 return res;
463 #if 0
464 BtorSort * res, ** pos, pattern, *index, *element;
465 BtorSortUniqueTable *table;
466
467 table = &btor->sorts_unique_table;
468
469 index = btor_sort_get_by_id (btor, index_id);
470 assert (index);
471 assert (index->refs > 0);
472 assert (index->table == table);
473 element = btor_sort_get_by_id (btor, element_id);
474 assert (element);
475 assert (element->refs > 0);
476 assert (element->table == table);
477
478 BTOR_CLR (&pattern);
479 pattern.kind = BTOR_ARRAY_SORT;
480 pattern.array.index = index;
481 pattern.array.element = element;
482 pos = find_sort (table, &pattern);
483 assert (pos);
484 res = *pos;
485 if (!res)
486 {
487 if (BTOR_FULL_SORT_UNIQUE_TABLE (table))
488 {
489 enlarge_sorts_unique_table (table);
490 pos = find_sort (table, &pattern);
491 assert (pos);
492 res = *pos;
493 assert (!res);
494 }
495 res = create_sort (btor, table, &pattern);
496 *pos = res;
497 }
498 inc_sort_ref_counter (res);
499 return res->id;
500 #endif
501 }
502
503 #if 0
504 BtorSortId
505 btor_sort_lst (Btor * btor,
506 BtorSortId head_id,
507 BtorSortId tail_id)
508 {
509 assert (btor);
510 assert (head_id < BTOR_COUNT_STACK (btor->sorts_unique_table.id2sort));
511 assert (tail_id < BTOR_COUNT_STACK (btor->sorts_unique_table.id2sort));
512
513 BtorSort * res, ** pos, pattern, *head, *tail;
514 BtorSortUniqueTable *table;
515
516 table = &btor->sorts_unique_table;
517
518 head = btor_sort_get_by_id (btor, head_id);
519 assert (head);
520 assert (head->refs > 0);
521 assert (head->table == table);
522 tail = btor_sort_get_by_id (btor, tail_id);
523 assert (tail);
524 assert (tail->refs > 0);
525 assert (tail->table == table);
526
527 BTOR_CLR (&pattern);
528 pattern.kind = BTOR_LST_SORT;
529 pattern.lst.head = head;
530 pattern.lst.tail = tail;
531 pos = find_sort (table, &pattern);
532 assert (pos);
533 res = *pos;
534 if (!res)
535 {
536 if (BTOR_FULL_SORT_UNIQUE_TABLE (table))
537 {
538 enlarge_sorts_unique_table (table);
539 pos = find_sort (table, &pattern);
540 assert (pos);
541 res = *pos;
542 assert (!res);
543 }
544 res = create_sort (btor, table, &pattern);
545 *pos = res;
546 }
547 inc_sort_ref_counter (res);
548 return res->id;
549 }
550 #endif
551
552 BtorSortId
btor_sort_fun(Btor * btor,BtorSortId domain_id,BtorSortId codomain_id)553 btor_sort_fun (Btor *btor, BtorSortId domain_id, BtorSortId codomain_id)
554 {
555 assert (btor);
556 assert (domain_id);
557
558 BtorSort *domain, *codomain, *res, **pos, pattern;
559 BtorSortUniqueTable *table;
560
561 table = &btor->sorts_unique_table;
562
563 domain = btor_sort_get_by_id (btor, domain_id);
564 assert (domain);
565 assert (domain->refs > 0);
566 assert (domain->table == table);
567 assert (domain->kind == BTOR_TUPLE_SORT);
568 codomain = btor_sort_get_by_id (btor, codomain_id);
569 assert (codomain);
570 assert (codomain->refs > 0);
571 assert (codomain->table == table);
572
573 BTOR_CLR (&pattern);
574 pattern.kind = BTOR_FUN_SORT;
575 pattern.fun.domain = domain;
576 pattern.fun.codomain = codomain;
577 pos = find_sort (table, &pattern);
578 assert (pos);
579 res = *pos;
580 if (!res)
581 {
582 if (BTOR_FULL_SORT_UNIQUE_TABLE (table))
583 {
584 enlarge_sorts_unique_table (table);
585 pos = find_sort (table, &pattern);
586 assert (pos);
587 res = *pos;
588 assert (!res);
589 }
590 res = create_sort (btor, table, &pattern);
591 res->fun.arity = domain->tuple.num_elements;
592 *pos = res;
593 }
594 inc_sort_ref_counter (res);
595
596 return res->id;
597 }
598
599 BtorSortId
btor_sort_tuple(Btor * btor,BtorSortId * element_ids,size_t num_elements)600 btor_sort_tuple (Btor *btor, BtorSortId *element_ids, size_t num_elements)
601 {
602 assert (btor);
603 assert (element_ids);
604 assert (num_elements > 0);
605
606 size_t i;
607 BtorSort *elements[num_elements], *res, **pos, pattern;
608 BtorSortUniqueTable *table;
609
610 table = &btor->sorts_unique_table;
611
612 for (i = 0; i < num_elements; i++)
613 {
614 elements[i] = btor_sort_get_by_id (btor, element_ids[i]);
615 assert (elements[i]);
616 assert (elements[i]->table == table);
617 }
618
619 BTOR_CLR (&pattern);
620 pattern.kind = BTOR_TUPLE_SORT;
621 pattern.tuple.num_elements = num_elements;
622 pattern.tuple.elements = elements;
623 pos = find_sort (table, &pattern);
624 assert (pos);
625 res = *pos;
626 if (!res)
627 {
628 if (BTOR_FULL_SORT_UNIQUE_TABLE (table))
629 {
630 enlarge_sorts_unique_table (table);
631 pos = find_sort (table, &pattern);
632 assert (pos);
633 res = *pos;
634 assert (!res);
635 }
636 res = create_sort (btor, table, &pattern);
637 *pos = res;
638 }
639 inc_sort_ref_counter (res);
640 return res->id;
641 }
642
643 uint32_t
btor_sort_bv_get_width(Btor * btor,BtorSortId id)644 btor_sort_bv_get_width (Btor *btor, BtorSortId id)
645 {
646 BtorSort *sort;
647 sort = btor_sort_get_by_id (btor, id);
648 assert (sort->kind != BTOR_BOOL_SORT);
649 #if 0
650 /* special case for Boolector as boolean are treated as bv of width 1 */
651 if (sort->kind == BTOR_BOOL_SORT)
652 return 1;
653 #endif
654 assert (sort->kind == BTOR_BV_SORT);
655 return sort->bitvec.width;
656 }
657
658 uint32_t
btor_sort_tuple_get_arity(Btor * btor,BtorSortId id)659 btor_sort_tuple_get_arity (Btor *btor, BtorSortId id)
660 {
661 BtorSort *sort;
662 sort = btor_sort_get_by_id (btor, id);
663 assert (sort->kind == BTOR_TUPLE_SORT);
664 return sort->tuple.num_elements;
665 }
666
667 BtorSortId
btor_sort_fun_get_codomain(Btor * btor,BtorSortId id)668 btor_sort_fun_get_codomain (Btor *btor, BtorSortId id)
669 {
670 BtorSort *sort;
671 sort = btor_sort_get_by_id (btor, id);
672 assert (sort->kind == BTOR_FUN_SORT);
673 return sort->fun.codomain->id;
674 }
675
676 BtorSortId
btor_sort_fun_get_domain(Btor * btor,BtorSortId id)677 btor_sort_fun_get_domain (Btor *btor, BtorSortId id)
678 {
679 BtorSort *sort;
680 sort = btor_sort_get_by_id (btor, id);
681 assert (sort->kind == BTOR_FUN_SORT);
682 return sort->fun.domain->id;
683 }
684
685 uint32_t
btor_sort_fun_get_arity(Btor * btor,BtorSortId id)686 btor_sort_fun_get_arity (Btor *btor, BtorSortId id)
687 {
688 BtorSort *sort;
689 sort = btor_sort_get_by_id (btor, id);
690 assert (sort->kind == BTOR_FUN_SORT);
691 assert (sort->fun.domain->kind == BTOR_TUPLE_SORT);
692 return sort->fun.domain->tuple.num_elements;
693 }
694
695 BtorSortId
btor_sort_array_get_index(Btor * btor,BtorSortId id)696 btor_sort_array_get_index (Btor *btor, BtorSortId id)
697 {
698 BtorSort *sort;
699 sort = btor_sort_get_by_id (btor, id);
700 assert (sort->kind != BTOR_ARRAY_SORT);
701 #if 0
702 if (sort->kind == BTOR_ARRAY_SORT)
703 return sort->array.index->id;
704 #endif
705 assert (sort->kind == BTOR_FUN_SORT);
706 assert (sort->fun.domain->tuple.num_elements == 1);
707 return sort->fun.domain->tuple.elements[0]->id;
708 }
709
710 BtorSortId
btor_sort_array_get_element(Btor * btor,BtorSortId id)711 btor_sort_array_get_element (Btor *btor, BtorSortId id)
712 {
713 BtorSort *sort;
714 sort = btor_sort_get_by_id (btor, id);
715 assert (sort->kind != BTOR_ARRAY_SORT);
716 #if 0
717 if (sort->kind == BTOR_ARRAY_SORT)
718 return sort->array.element->id;
719 #endif
720 assert (sort->kind == BTOR_FUN_SORT);
721 return sort->fun.codomain->id;
722 }
723
724 bool
btor_sort_is_valid(Btor * btor,BtorSortId id)725 btor_sort_is_valid (Btor *btor, BtorSortId id)
726 {
727 return id < BTOR_COUNT_STACK (btor->sorts_unique_table.id2sort)
728 && BTOR_PEEK_STACK (btor->sorts_unique_table.id2sort, id) != 0;
729 }
730
731 bool
btor_sort_is_bool(Btor * btor,BtorSortId id)732 btor_sort_is_bool (Btor *btor, BtorSortId id)
733 {
734 return btor_sort_is_bv (btor, id) && btor_sort_bv_get_width (btor, id) == 1;
735 }
736
737 bool
btor_sort_is_bv(Btor * btor,BtorSortId id)738 btor_sort_is_bv (Btor *btor, BtorSortId id)
739 {
740 BtorSort *sort;
741 sort = btor_sort_get_by_id (btor, id);
742 assert (sort);
743 return sort->kind == BTOR_BV_SORT;
744 }
745
746 bool
btor_sort_is_array(Btor * btor,BtorSortId id)747 btor_sort_is_array (Btor *btor, BtorSortId id)
748 {
749 BtorSort *sort;
750 sort = btor_sort_get_by_id (btor, id);
751 assert (sort);
752 return btor_sort_is_fun (btor, id) && sort->fun.is_array;
753 }
754
755 bool
btor_sort_is_tuple(Btor * btor,BtorSortId id)756 btor_sort_is_tuple (Btor *btor, BtorSortId id)
757 {
758 BtorSort *sort;
759 sort = btor_sort_get_by_id (btor, id);
760 assert (sort);
761 return sort->kind == BTOR_TUPLE_SORT;
762 }
763
764 bool
btor_sort_is_fun(Btor * btor,BtorSortId id)765 btor_sort_is_fun (Btor *btor, BtorSortId id)
766 {
767 BtorSort *sort;
768 sort = btor_sort_get_by_id (btor, id);
769 assert (sort);
770 return sort->kind == BTOR_FUN_SORT;
771 }
772
773 void
btor_iter_tuple_sort_init(BtorTupleSortIterator * it,Btor * btor,BtorSortId id)774 btor_iter_tuple_sort_init (BtorTupleSortIterator *it, Btor *btor, BtorSortId id)
775 {
776 assert (it);
777 assert (btor);
778 assert (btor_sort_is_tuple (btor, id));
779 it->pos = 0;
780 it->tuple = btor_sort_get_by_id (btor, id);
781 }
782
783 bool
btor_iter_tuple_sort_has_next(const BtorTupleSortIterator * it)784 btor_iter_tuple_sort_has_next (const BtorTupleSortIterator *it)
785 {
786 assert (it);
787 return it->pos < it->tuple->tuple.num_elements;
788 }
789
790 BtorSortId
btor_iter_tuple_sort_next(BtorTupleSortIterator * it)791 btor_iter_tuple_sort_next (BtorTupleSortIterator *it)
792 {
793 assert (it);
794 assert (it->pos < it->tuple->tuple.num_elements);
795
796 BtorSortId result;
797 result = it->tuple->tuple.elements[it->pos]->id;
798 it->pos += 1;
799 return result;
800 }
801