1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * Concrete values = constants of different types.
21 * This is used to build models: a model is a mapping from terms to concrete values.
22 */
23
24 #include <inttypes.h>
25
26 #include "model/concrete_values.h"
27 #include "terms/bv64_constants.h"
28 #include "utils/hash_functions.h"
29 #include "utils/int_array_sort.h"
30 #include "utils/memalloc.h"
31
32 #ifdef HAVE_MCSAT
33 #include <poly/algebraic_number.h>
34 #endif
35
36
37
38 /************************
39 * AUXILIARY HASH MAP *
40 ***********************/
41
42 /*
43 * Initialize table: empty table of default size
44 */
init_map_htbl(map_htbl_t * htbl)45 static void init_map_htbl(map_htbl_t *htbl) {
46 uint32_t i, n;
47 map_pair_t *tmp;
48
49 n = MAP_HTBL_DEFAULT_SIZE;
50 assert(n < MAP_HTBL_MAX_SIZE);
51
52 tmp = (map_pair_t *) safe_malloc(n * sizeof(map_pair_t));
53 for (i=0; i<n; i++) {
54 tmp[i].function = null_value; // mark as empty
55 }
56
57 htbl->data = tmp;
58 htbl->size = n;
59 htbl->nelems = 0;
60 htbl->resize_threshold = (uint32_t) (MAP_HTBL_RESIZE_RATIO * n);
61 }
62
63
64
65 /*
66 * Delete the table
67 */
delete_map_htbl(map_htbl_t * htbl)68 static void delete_map_htbl(map_htbl_t *htbl) {
69 safe_free(htbl->data);
70 htbl->data = NULL;
71 }
72
73
74 /*
75 * Empty the table
76 */
reset_map_htbl(map_htbl_t * htbl)77 static void reset_map_htbl(map_htbl_t *htbl) {
78 uint32_t i, n;
79
80 n = htbl->size;
81 for (i=0; i<n; i++) {
82 htbl->data[i].function = null_value; // mark as empty
83 }
84 htbl->nelems = 0;
85 }
86
87
88
89
90 /*
91 * Compute the hash code of (f a[0] ... a[n-1])
92 * - f and a[0] ... a[n-1] must all be valid objects in vtbl
93 */
hash_fun_app(value_t f,uint32_t n,value_t * a)94 static uint32_t hash_fun_app(value_t f, uint32_t n, value_t *a) {
95 uint32_t h;
96
97 h = jenkins_hash_intarray2(a, n, 0x83421bca);
98 return jenkins_hash_pair(f, 0, h);
99 }
100
101
102
103 /*
104 * Compute the hash code of a pair (f, i)
105 * - f must be a function object
106 * - i must be a mapping object of same arity as f
107 */
hash_map_pair(value_table_t * table,value_t f,value_t i)108 static uint32_t hash_map_pair(value_table_t *table, value_t f, value_t i) {
109 value_map_t *map;
110
111 assert(object_is_map(table, i) && object_is_function(table, f));
112 map = (value_map_t *) table->desc[i].ptr;
113 assert(map->arity == ((value_fun_t *) table->desc[f].ptr)->arity);
114 return hash_fun_app(f, map->arity, map->arg);
115 }
116
117
118
119
120 /*
121 * Check whether object i matches a[0] ... a[n-1]
122 * - i must be a mapping object with n arguments
123 * - i matches if a[0] = arg[0] ... a[n-1] = arg[n-1]
124 */
mapping_matches_array(value_table_t * table,value_t i,uint32_t n,value_t * a)125 static bool mapping_matches_array(value_table_t *table, value_t i, uint32_t n, value_t *a) {
126 value_map_t *map;
127 uint32_t j;
128
129 assert(object_is_map(table, i));
130 map = (value_map_t *) table->desc[i].ptr;
131 assert(map->arity == n);
132
133 for (j=0; j<n; j++) {
134 if (a[j] != map->arg[j]) return false;
135 }
136
137 return true;
138 }
139
140
141
142 /*
143 * Check whether object i and j match each other
144 * - both must be mapping objects with the same number of arguments
145 */
mappings_match(value_table_t * table,value_t i,value_t j)146 static bool mappings_match(value_table_t *table, value_t i, value_t j) {
147 value_map_t *map1, *map2;
148 uint32_t k, n;
149
150 assert(object_is_map(table, i) && object_is_map(table, j));
151 map1 = (value_map_t *) table->desc[i].ptr;
152 map2 = (value_map_t *) table->desc[j].ptr;
153 n = map1->arity;
154 assert(map2->arity == n);
155
156 for (k=0; k<n; k++) {
157 if (map1->arg[k] != map2->arg[k]) return false;
158 }
159
160 return true;
161 }
162
163
164 /*
165 * Search for a pair (f, k) in table such that k is of the form
166 * (a[0] ... a[n-1] |-> v)
167 * - vtbl = the value table where all objects are defined
168 * - return v if such a pair is found, null_value otherwise
169 */
hash_eval_app(value_table_t * table,value_t f,uint32_t n,value_t * a)170 static value_t hash_eval_app(value_table_t *table, value_t f, uint32_t n, value_t *a) {
171 map_pair_t *d;
172 uint32_t i, mask;
173 value_t j;
174
175 assert(table->mtbl.nelems < table->mtbl.size);
176
177 mask = table->mtbl.size - 1;
178 d = table->mtbl.data;
179 i = hash_fun_app(f, n, a) & mask;
180 for (;;) {
181 if (d[i].function < 0) return null_value;
182 if (d[i].function == f) {
183 j = d[i].map;
184 if (mapping_matches_array(table, j, n, a)) {
185 return vtbl_map_result(table, j);
186 }
187 }
188 i ++;
189 i &= mask;
190 }
191 }
192
193
194
195 /*
196 * Copy pair p into a clean data array
197 * - mask = size of data - 1 (data's size must be a power of 2)
198 * - p must be a valid pair (i.e., p->function >= 0)
199 * - there must be an empty slot in data
200 */
map_htbl_clean_copy(value_table_t * table,map_pair_t * data,map_pair_t * p,uint32_t mask)201 static void map_htbl_clean_copy(value_table_t *table, map_pair_t *data,
202 map_pair_t *p, uint32_t mask) {
203 uint32_t i;
204
205 i = hash_map_pair(table, p->function, p->map) & mask;
206 while (data[i].function >= 0) {
207 i ++;
208 i &= mask;
209 }
210 data[i] = *p;
211 }
212
213
214
215 /*
216 * Make the hash table twice as large
217 */
map_htbl_extend(value_table_t * table)218 static void map_htbl_extend(value_table_t *table) {
219 uint32_t n, n2;
220 map_pair_t *tmp, *p;
221 uint32_t i, mask;
222
223 n = table->mtbl.size;
224 n2 = n << 1;
225 if (n2 >= MAP_HTBL_MAX_SIZE) {
226 out_of_memory();
227 }
228
229 tmp = (map_pair_t *) safe_malloc(n2 * sizeof(map_pair_t));
230 for (i=0; i<n2; i++) {
231 tmp[i].function = null_value;
232 }
233
234 mask = n2 - 1;
235 p = table->mtbl.data;
236 for (i=0; i<n; i++) {
237 if (p->function >= 0) {
238 map_htbl_clean_copy(table, tmp, p, mask);
239 }
240 p ++;
241 }
242
243 safe_free(table->mtbl.data);
244 table->mtbl.data = tmp;
245 table->mtbl.size = n2;
246 table->mtbl.resize_threshold = (uint32_t) (MAP_HTBL_RESIZE_RATIO * n2);
247 }
248
249
250
251 /*
252 * Add the pair (f, i) to the hash table
253 * - there must not be a matching (f, j) in the table already
254 */
add_hash_pair(value_table_t * table,value_t f,value_t i)255 static void add_hash_pair(value_table_t *table, value_t f, value_t i) {
256 map_pair_t *d;
257 uint32_t j, mask;
258
259 assert(table->mtbl.nelems < table->mtbl.size);
260
261 mask = table->mtbl.size - 1;
262 d = table->mtbl.data;
263 j = hash_map_pair(table, f, i) & mask;
264 while (d[j].function >= 0) {
265 assert(d[j].function != f || !mappings_match(table, i, d[j].map));
266 j ++;
267 j &= mask;
268 }
269
270 assert(d[j].function == null_value);
271 d[j].function = f;
272 d[j].map = i;
273
274 table->mtbl.nelems ++;
275 if (table->mtbl.nelems > table->mtbl.resize_threshold) {
276 map_htbl_extend(table);
277 }
278
279 }
280
281
282
283 /********************************
284 * QUEUE FOR DELAYED PRINTING *
285 *******************************/
286
287 /*
288 * Initialize: don't allocate the mark vector yet
289 */
init_vtbl_queue(vtbl_queue_t * vq)290 static void init_vtbl_queue(vtbl_queue_t *vq) {
291 init_int_queue(&vq->queue, 0);
292 vq->mark = NULL;
293 vq->size = 0;
294 }
295
296 /*
297 * Reset: empty the queue and delete the mark vector
298 */
reset_vtbl_queue(vtbl_queue_t * vq)299 static void reset_vtbl_queue(vtbl_queue_t *vq) {
300 int_queue_reset(&vq->queue);
301 delete_bitvector(vq->mark);
302 vq->mark = NULL;
303 vq->size = 0;
304 }
305
306 /*
307 * Delete
308 */
delete_vtbl_queue(vtbl_queue_t * vq)309 static void delete_vtbl_queue(vtbl_queue_t *vq) {
310 delete_int_queue(&vq->queue);
311 delete_bitvector(vq->mark);
312 vq->mark = NULL;
313 }
314
315
316 /*
317 * Extend the mark vector to at least size n
318 * - n must be larger than vq->size
319 */
resize_vtbl_queue(vtbl_queue_t * vq,uint32_t n)320 static void resize_vtbl_queue(vtbl_queue_t *vq, uint32_t n) {
321 uint32_t new_size;
322
323 assert(vq->size < n && n <= MAX_VALUE_TABLE_SIZE);
324
325 n = (n + 63) & ~63u; // round n up to a multiple of 64
326 if (n < DEF_VTBL_QUEUE_SIZE) {
327 n = DEF_VTBL_QUEUE_SIZE;
328 }
329
330 new_size = vq->size << 1; // double the size
331 if (new_size < n) new_size = n;
332
333 vq->mark = extend_bitvector0(vq->mark, new_size, vq->size);
334 vq->size = new_size;
335
336 assert((vq->size & 63u) == 0);
337 }
338
339
340 /*
341 * Add v to the queue if it's not marked then mark v
342 */
vtbl_queue_push(vtbl_queue_t * vq,value_t v)343 static void vtbl_queue_push(vtbl_queue_t *vq, value_t v) {
344 assert(0 <= v && v < (int32_t) MAX_VALUE_TABLE_SIZE);
345
346 if (v >= vq->size) {
347 resize_vtbl_queue(vq, v+1);
348 assert(v < vq->size);
349 }
350 if (!tst_bit(vq->mark, v)) {
351 set_bit(vq->mark, v);
352 int_queue_push(&vq->queue, v);
353 }
354 }
355
356
357
358 /****************************************
359 * HASH SETS FOR UPDATE NORMALIZATION *
360 ***************************************/
361
362 /*
363 * Initialize hset: use the default size
364 */
init_map_hset(map_hset_t * hset)365 static void init_map_hset(map_hset_t *hset) {
366 uint32_t i, n;
367 value_t *tmp;
368
369 n = MAP_HSET_DEFAULT_SIZE;
370 assert(n < MAP_HSET_MAX_SIZE);
371
372 tmp = (value_t *) safe_malloc(n * sizeof(value_t));
373 for (i=0; i<n; i++) {
374 tmp[i] = null_value;
375 }
376
377 hset->data = tmp;
378 hset->size = n;
379 hset->nelems = 0;
380 hset->resize_threshold = (uint32_t) (MAP_HSET_RESIZE_RATIO * n);
381 }
382
383
384 /*
385 * Delete hset
386 */
delete_map_hset(map_hset_t * hset)387 static void delete_map_hset(map_hset_t *hset) {
388 safe_free(hset->data);
389 hset->data = NULL;
390 }
391
392
393 /*
394 * Empty hset
395 */
reset_map_hset(map_hset_t * hset)396 static void reset_map_hset(map_hset_t *hset) {
397 uint32_t i, n;
398
399 n = hset->size;
400 if (n >= MAP_HSET_REDUCE_THRESHOLD) {
401 // reduce data to an array of default size
402 safe_free(hset->data);
403
404 n = MAP_HSET_DEFAULT_SIZE;
405 assert(n < MAP_HSET_MAX_SIZE && n < MAP_HSET_REDUCE_THRESHOLD);
406 hset->data = (value_t *) safe_malloc(n * sizeof(value_t));
407 hset->size = n;
408 hset->resize_threshold = (uint32_t) (MAP_HSET_RESIZE_RATIO * n);
409 }
410
411 // empty data
412 for (i=0; i<n; i++) {
413 hset->data[i] = null_value;
414 }
415 hset->nelems = 0;
416 }
417
418
419 /*
420 * Hash code for a tuple of objects a[0 ... n]
421 */
hash_map_tuple(value_t * a,uint32_t n)422 static inline uint32_t hash_map_tuple(value_t *a, uint32_t n) {
423 return jenkins_hash_intarray2(a, n, 0x543f1a83);
424 }
425
426
427 /*
428 * Hash code for mapping object i
429 */
hash_map_object(value_table_t * table,value_t i)430 static uint32_t hash_map_object(value_table_t *table, value_t i) {
431 value_map_t *map;
432
433 assert(object_is_map(table, i));
434 map = (value_map_t *) table->desc[i].ptr;
435 return hash_map_tuple(map->arg, map->arity);
436 }
437
438
439 /*
440 * Copy v into clean array d
441 * - mask = size of d - 1, where size of d is a power of 2
442 */
map_hset_clean_copy(value_table_t * table,value_t * d,value_t v,uint32_t mask)443 static void map_hset_clean_copy(value_table_t *table, value_t *d, value_t v, uint32_t mask) {
444 uint32_t i;
445
446 i = hash_map_object(table, v) & mask;
447 while (d[i] >= 0) {
448 i++;
449 i &= mask;
450 }
451 d[i] = v;
452 }
453
454
455 /*
456 * Make the hset twice as large. Keep its content.
457 */
map_hset_extend(value_table_t * table,map_hset_t * hset)458 static void map_hset_extend(value_table_t *table, map_hset_t *hset) {
459 uint32_t n, n2;
460 value_t *d, *p;
461 uint32_t i, mask;
462
463 n = hset->size;
464 n2 = n<<1;
465 if (n2 >= MAP_HSET_MAX_SIZE) {
466 out_of_memory();
467 }
468
469 d = (value_t *) safe_malloc(n2 * sizeof(value_t));
470 for (i=0; i<n2; i++) {
471 d[i] = null_value;
472 }
473
474 mask = n2 - 1;
475 p = hset->data;
476 for (i=0; i<n; i++) {
477 if (p[i] >= 0) {
478 map_hset_clean_copy(table, d, p[i], mask);
479 }
480 }
481
482 safe_free(p);
483 hset->data = d;
484 hset->size = n2;
485 hset->resize_threshold = (uint32_t) (MAP_HSET_RESIZE_RATIO * n2);
486 }
487
488
489 /*
490 * Add mapping object i to hset:
491 * - no change if i matches an existing element in hset
492 */
hset_add_map(value_table_t * table,map_hset_t * hset,value_t i)493 static void hset_add_map(value_table_t *table, map_hset_t *hset, value_t i) {
494 value_t *d;
495 value_t k;
496 uint32_t j, mask;
497
498 assert(hset->nelems < hset->size);
499
500 mask = hset->size - 1;
501 d = hset->data;
502 j = hash_map_object(table, i) & mask;
503 for (;;) {
504 k = d[j];
505 if (k < 0) break; // add i
506 if (mappings_match(table, i, k)) return; // k has precedence
507 j ++;
508 j &= mask;
509 }
510
511 d[j] = i;
512 hset->nelems ++;
513 if (hset->nelems > hset->resize_threshold) {
514 map_hset_extend(table, hset);
515 }
516 }
517
518
519 /*
520 * Return the map_object that matches tuple a[0... n-1]
521 * - return null_value if there's no such object
522 */
hset_find_map(value_table_t * table,map_hset_t * hset,value_t * a,uint32_t n)523 static value_t hset_find_map(value_table_t *table, map_hset_t *hset, value_t *a, uint32_t n) {
524 value_t *d;
525 value_t k;
526 uint32_t j, mask;
527
528 assert(hset->nelems < hset->size);
529 mask = hset->size - 1;
530 d = hset->data;
531 j = hash_map_tuple(a, n) & mask;
532 for (;;) {
533 k = d[j];
534 if (k < 0) break; // nothing matches
535 if (mapping_matches_array(table, k, n, a)) return k;
536 j ++;
537 j &= mask;
538 }
539
540 return null_value;
541 }
542
543 /*
544 * Normalize: collect all elements of hset into hset->data[0 ... n-1]
545 * where n = hset->nelems and sort the elements.
546 *
547 * No addition is possible after normalization.
548 */
hset_normalize(map_hset_t * hset)549 static void hset_normalize(map_hset_t *hset) {
550 value_t *d;
551 uint32_t i, j, n;
552
553 d = hset->data;
554 n = hset->size;
555 j = 0;
556 for (i=0; i<n; i++) {
557 if (d[i] >= 0) {
558 d[j] = d[i];
559 j ++;
560 }
561 }
562 assert(j == hset->nelems);
563 int_array_sort(d, j);
564 }
565
566
567
568
569
570
571 /*****************************************
572 * TABLE INITIALIZATION/DELETION/RESET *
573 ****************************************/
574
575 /*
576 * Initialize a table;
577 * - n = initial size. If n is zero, the default size is used.
578 * - ttbl = attached type table.
579 */
init_value_table(value_table_t * table,uint32_t n,type_table_t * ttbl)580 void init_value_table(value_table_t *table, uint32_t n, type_table_t *ttbl) {
581 if (n == 0) {
582 n = DEF_VALUE_TABLE_SIZE;
583 }
584 if (n >= MAX_VALUE_TABLE_SIZE) {
585 out_of_memory();
586 }
587
588 table->size = n;
589 table->nobjects = 0;
590 table->kind = (uint8_t *) safe_malloc(n * sizeof(uint8_t));
591 table->desc = (value_desc_t *) safe_malloc(n * sizeof(value_desc_t));
592 table->canonical = allocate_bitvector0(n);
593
594 table->type_table = ttbl;
595 init_int_htbl(&table->htbl, 0);
596 init_bvconstant(&table->buffer);
597 init_ivector(&table->aux_vector, 0);
598 init_map_htbl(&table->mtbl);
599 init_vtbl_queue(&table->queue);
600
601 table->hset1 = NULL;
602 table->hset2 = NULL;
603
604 table->unknown_value = null_value;
605 table->true_value = null_value;
606 table->false_value = null_value;
607
608 table->zero_rdiv_fun = null_value;
609 table->zero_idiv_fun = null_value;
610 table->zero_mod_fun = null_value;
611
612 table->first_tmp = -1; // no temporary objects
613
614 table->aux_namer = NULL;
615 table->unint_namer = NULL;
616 }
617
618
619 /*
620 * Make the table larger (by 50%)
621 */
extend_value_table(value_table_t * table)622 static void extend_value_table(value_table_t *table) {
623 uint32_t n;
624
625 n = table->size + 1;
626 n += n>>1;
627 assert(n > table->size);
628
629 if (n >= MAX_VALUE_TABLE_SIZE) {
630 out_of_memory();
631 }
632
633 table->size = n;
634 table->kind = (uint8_t *) safe_realloc(table->kind, n * sizeof(uint8_t));
635 table->desc = (value_desc_t *) safe_realloc(table->desc, n * sizeof(value_desc_t));
636 table->canonical = extend_bitvector0(table->canonical, n, table->size);
637 }
638
639
640 /*
641 * Allocate a new object index
642 * - kind and descriptor are not initialized
643 */
allocate_object(value_table_t * table)644 static value_t allocate_object(value_table_t *table) {
645 value_t i;
646
647 i = table->nobjects;
648 if (i == table->size) {
649 extend_value_table(table);
650 }
651 assert(i < table->size);
652 table->nobjects = i+1;
653 return i;
654 }
655
656
657 /*
658 * Return hset1 or hset2 (allocate and initialize it if needed)
659 */
get_hset1(value_table_t * table)660 static map_hset_t *get_hset1(value_table_t *table) {
661 map_hset_t *set;
662
663 set = table->hset1;
664 if (set == NULL) {
665 set = (map_hset_t *) safe_malloc(sizeof(map_hset_t));
666 init_map_hset(set);
667 table->hset1 = set;
668 }
669 return set;
670 }
671
get_hset2(value_table_t * table)672 static map_hset_t *get_hset2(value_table_t *table) {
673 map_hset_t *set;
674
675 set = table->hset2;
676 if (set == NULL) {
677 set = (map_hset_t *) safe_malloc(sizeof(map_hset_t));
678 init_map_hset(set);
679 table->hset2 = set;
680 }
681 return set;
682 }
683
684
685 /*
686 * Delete hset1 and hset2 if they exist
687 */
delete_hsets(value_table_t * table)688 static void delete_hsets(value_table_t *table) {
689 if (table->hset1 != NULL) {
690 delete_map_hset(table->hset1);
691 safe_free(table->hset1);
692 table->hset1 = NULL;
693 }
694
695 if (table->hset2 != NULL) {
696 delete_map_hset(table->hset2);
697 safe_free(table->hset2);
698 table->hset2 = NULL;
699 }
700 }
701
702
703 /*
704 * Reset hset1 and hset2 if they exist
705 */
reset_hsets(value_table_t * table)706 static void reset_hsets(value_table_t *table) {
707 if (table->hset1 != NULL) {
708 reset_map_hset(table->hset1);
709 }
710 if (table->hset2 != NULL) {
711 reset_map_hset(table->hset2);
712 }
713 }
714
715
716 /*
717 * Delete object descriptors
718 */
delete_value_unint(value_unint_t * d)719 static inline void delete_value_unint(value_unint_t *d) {
720 safe_free(d->name);
721 safe_free(d);
722 }
723
delete_value_fun(value_fun_t * d)724 static inline void delete_value_fun(value_fun_t *d) {
725 safe_free(d->name);
726 safe_free(d);
727 }
728
729 /*
730 * Delete descriptors for objects k ... nobjects - 1
731 */
vtbl_delete_descriptors(value_table_t * table,uint32_t k)732 static void vtbl_delete_descriptors(value_table_t *table, uint32_t k) {
733 uint32_t i, n;
734
735 n = table->nobjects;
736 table->nobjects = k;
737
738 assert(k <= n);
739 for (i=k; i<n; i++) {
740 switch (table->kind[i]) {
741 case UNKNOWN_VALUE:
742 case BOOLEAN_VALUE:
743 break;
744 case RATIONAL_VALUE:
745 q_clear(&table->desc[i].rational);
746 break;
747 case ALGEBRAIC_VALUE:
748 #ifdef HAVE_MCSAT
749 lp_algebraic_number_destruct(table->desc[i].ptr);
750 safe_free(table->desc[i].ptr);
751 #else
752 assert(false);
753 #endif
754 break;
755 case UNINTERPRETED_VALUE:
756 delete_value_unint(table->desc[i].ptr);
757 break;
758 case FUNCTION_VALUE:
759 delete_value_fun(table->desc[i].ptr);
760 break;
761 case BITVECTOR_VALUE:
762 case TUPLE_VALUE:
763 case MAP_VALUE:
764 case UPDATE_VALUE:
765 safe_free(table->desc[i].ptr);
766 break;
767 }
768 }
769 }
770
771
772 /*
773 * Reset the table:
774 * - delete all descriptors
775 * - empty the table.
776 */
reset_value_table(value_table_t * table)777 void reset_value_table(value_table_t *table) {
778 vtbl_delete_descriptors(table, 0);
779 reset_int_htbl(&table->htbl);
780 reset_map_htbl(&table->mtbl);
781 reset_vtbl_queue(&table->queue);
782 reset_hsets(table);
783
784 ivector_reset(&table->aux_vector);
785
786 table->nobjects = 0;
787 table->unknown_value = null_value;
788 table->true_value = null_value;
789 table->false_value = null_value;
790 table->first_tmp = -1;
791 }
792
793
794 /*
795 * Delete the table
796 */
delete_value_table(value_table_t * table)797 void delete_value_table(value_table_t *table) {
798 vtbl_delete_descriptors(table, 0);
799 safe_free(table->kind);
800 safe_free(table->desc);
801 delete_bitvector(table->canonical);
802 delete_int_htbl(&table->htbl);
803 delete_bvconstant(&table->buffer);
804 delete_ivector(&table->aux_vector);
805 delete_map_htbl(&table->mtbl);
806 delete_vtbl_queue(&table->queue);
807 delete_hsets(table);
808 table->kind = NULL;
809 table->desc = NULL;
810 table->canonical = NULL;
811 }
812
813
814
815
816
817 /******************************************************
818 * CONSTRUCTORS: VALUES THAT DON'T USE HASH CONSING *
819 *****************************************************/
820
821 /*
822 * Unknown value: for undefined stuff
823 */
vtbl_mk_unknown(value_table_t * table)824 value_t vtbl_mk_unknown(value_table_t *table) {
825 value_t i;
826
827 i = table->unknown_value;
828 if (i < 0) {
829 i = allocate_object(table);
830 table->kind[i] = UNKNOWN_VALUE;
831 table->desc[i].ptr = NULL;
832 table->unknown_value = i;
833 set_bit(table->canonical, i);
834 }
835 return i;
836 }
837
838
839 /*
840 * True and false
841 */
vtbl_mk_true(value_table_t * table)842 value_t vtbl_mk_true(value_table_t *table) {
843 value_t i;
844
845 i = table->true_value;
846 if (i < 0) {
847 i = allocate_object(table);
848 table->kind[i] = BOOLEAN_VALUE;
849 table->desc[i].integer = 1; // non-zero means true
850 table->true_value = i;
851 set_bit(table->canonical, i);
852 }
853 return i;
854 }
855
vtbl_mk_false(value_table_t * table)856 value_t vtbl_mk_false(value_table_t *table) {
857 value_t i;
858
859 i = table->false_value;
860 if (i < 0) {
861 i = allocate_object(table);
862 table->kind[i] = BOOLEAN_VALUE;
863 table->desc[i].integer = 0; // zero means false
864 table->false_value = i;
865 set_bit(table->canonical, i);
866 }
867 return i;
868 }
869
870
871 /*
872 * Booleans: val = 0 means false, val != 0 means true
873 */
vtbl_mk_bool(value_table_t * table,int32_t val)874 value_t vtbl_mk_bool(value_table_t *table, int32_t val) {
875 if (val) {
876 return vtbl_mk_true(table);
877 } else {
878 return vtbl_mk_false(table);
879 }
880 }
881
882
883 /*
884 * Negation of v
885 */
vtbl_mk_not(value_table_t * table,value_t v)886 value_t vtbl_mk_not(value_table_t *table, value_t v) {
887 assert(v >= 0 && (v == table->true_value || v == table->false_value));
888
889 if (v == table->true_value) {
890 return vtbl_mk_false(table);
891 } else {
892 return vtbl_mk_true(table);
893 }
894 }
895
896
897
898
899 /********************************************
900 * NORMALIZATION OF FUNCTIONS AND UPDATES *
901 *******************************************/
902
903 /*
904 * Normalize an array of mapping objects a[0 ... n-1]
905 * - sort a and remove duplicates
906 * - return the number of elements left in a
907 */
normalize_map_array(uint32_t n,value_t * a)908 static uint32_t normalize_map_array(uint32_t n, value_t *a) {
909 uint32_t i, j;
910 value_t v, w;
911
912 if (n > 1) {
913 int_array_sort(a, n);
914 j = 1;
915 v = a[0];
916 for (i=1; i<n; i++) {
917 w = a[i];
918 if (v != w) {
919 a[j] = w;
920 j ++;
921 v = w;
922 }
923 }
924 n = j;
925 }
926
927 return n;
928 }
929
930
931
932 /*
933 * Remove all elements in array a[0 ... n-1] that give the same
934 * value as def.
935 * - return the number of elements left in a
936 */
remove_redundant_mappings(value_table_t * table,uint32_t n,value_t * a,value_t def)937 static uint32_t remove_redundant_mappings(value_table_t *table, uint32_t n, value_t *a, value_t def) {
938 uint32_t i, j;
939 value_t v;
940
941 j = 0;
942 for (i=0; i<n; i++) {
943 v = a[i];
944 if (vtbl_map_result(table, v) != def) {
945 a[j] = v;
946 j++;
947 }
948 }
949
950 return j;
951 }
952
953
954
955 /*
956 * Compute the set of mapping objects for i
957 * - i must be an update value or a function
958 * - hset = where the set is stored
959 * - def = address where default value will be copied
960 * - tau = address where the function type will be copied
961 *
962 * The mapping objects are added to hset then hset is normalized.
963 * Whatever is in hset when the function is called is kept.
964 * The default value and type of the function are copied into
965 * *def and *tau
966 */
normalize_update(value_table_t * table,value_t i,map_hset_t * hset,value_t * def,type_t * tau)967 static void normalize_update(value_table_t *table, value_t i, map_hset_t *hset, value_t *def, type_t *tau) {
968 value_update_t *upd;
969 value_fun_t *fun;
970 uint32_t j, n;
971
972 while (object_is_update(table, i)) {
973 upd = (value_update_t *) table->desc[i].ptr;
974 hset_add_map(table, hset, upd->map);
975 i = upd->fun;
976 }
977
978 assert(object_is_function(table, i));
979 fun = (value_fun_t *) table->desc[i].ptr;
980 *def = fun->def;
981 *tau = fun->type;
982 n = fun->map_size;
983 for (j=0; j<n; j++) {
984 hset_add_map(table, hset, fun->map[j]);
985 }
986
987 hset_normalize(hset);
988
989 // the mappings are in hset->data[0.. nelems-1]
990 if (! object_is_unknown(table, *def)) {
991 n = remove_redundant_mappings(table, hset->nelems, hset->data, *def);
992 hset->nelems = n;
993 }
994 }
995
996
997
998 /*
999 * Exported version: expand update object i.
1000 * - store the mappings in table->hset1
1001 */
vtbl_expand_update(value_table_t * table,value_t i,value_t * def,type_t * tau)1002 void vtbl_expand_update(value_table_t *table, value_t i, value_t *def, type_t *tau) {
1003 map_hset_t *hset;
1004
1005 assert(0 <= i && i < table->nobjects && table->kind[i] == UPDATE_VALUE);
1006
1007 hset = get_hset1(table);
1008 reset_map_hset(hset);
1009 normalize_update(table, i, hset, def, tau);
1010 }
1011
1012
1013 /*
1014 * Get the type of a function or update object i
1015 */
vtbl_function_type(value_table_t * table,value_t i)1016 type_t vtbl_function_type(value_table_t *table, value_t i) {
1017 value_update_t *upd;
1018 value_fun_t *fun;
1019
1020 while (object_is_update(table, i)) {
1021 upd = (value_update_t *) table->desc[i].ptr;
1022 i = upd->fun;
1023 }
1024
1025 assert(object_is_function(table, i));
1026 fun = (value_fun_t *) table->desc[i].ptr;
1027
1028 return fun->type;
1029 }
1030
1031
1032
1033
1034 /**********************************************************
1035 * MORE NORMALIZATION FOR FUNCTIONS WITH FINITE DOMAINS *
1036 *********************************************************/
1037
1038 /*
1039 * A function is defined by a set of mappings + a default value
1040 * - that may be ambiguous if the domain is finite and the default is not unknown
1041 * - to ensure a normal representation, we force the default value to be
1042 * the most common value for f (ties are breaking by selecting as default
1043 * value the one with the smallest id).
1044 */
1045
1046 /*
1047 * Return the element x of a that occurs most often
1048 * - ties are broken by selecting elements with smaller index
1049 * - a must be nonempty and sorted in increasing order
1050 * - return the number of occurrences of x in *count
1051 */
majority_element(value_t * a,uint32_t n,uint32_t * count)1052 static value_t majority_element(value_t *a, uint32_t n, uint32_t *count) {
1053 uint32_t i;
1054 value_t b, x;
1055 uint32_t nb, nx;
1056
1057 assert(n > 0);
1058
1059 // b = best so far, nb = best count so far
1060 b = null_value;
1061 nb = 0;
1062
1063 x = a[0];
1064 nx = 1;
1065 for (i=1; i<n; i++) {
1066 if (x == a[i]) {
1067 nx ++;
1068 } else {
1069 if (nx > nb) {
1070 b = x;
1071 nb = nx;
1072 }
1073 x = a[i];
1074 nx = 1;
1075 }
1076 }
1077
1078 // last element
1079 if (nx > nb) {
1080 b = x;
1081 nb = nx;
1082 }
1083
1084 *count = nb;
1085 return b;
1086 }
1087
1088 /*
1089 * Get the most frequent value in the range of map[0 ... n-1]
1090 * - n must be positive
1091 * - if there are ties, the value with smallest id is returned
1092 * - store the number of occurrences in *count.
1093 */
get_default_for_map(value_table_t * table,uint32_t n,value_t * a,uint32_t * count)1094 static value_t get_default_for_map(value_table_t *table, uint32_t n, value_t *a, uint32_t *count) {
1095 ivector_t *v;
1096 uint32_t i;
1097 value_t x;
1098
1099 assert(n > 0);
1100
1101 v = &table->aux_vector;
1102 resize_ivector(v, n);
1103 for (i=0; i<n; i++) {
1104 v->data[i] = vtbl_map_result(table, a[i]);
1105 }
1106 int_array_sort(v->data, n);
1107
1108 x = majority_element(v->data, n, count);
1109 ivector_reset(v);
1110
1111 return x;
1112 }
1113
1114
1115 /*
1116 * Change the default value for a function definition
1117 * - tau = function type
1118 * - a = function mappings
1119 * - n = number of elements in a
1120 * - old_def = current default
1121 * - new_def = new default
1122 *
1123 * This removes mappings from a and creates new ones but a's size
1124 * does not increase. Return the number of mappings in a after
1125 * swapping.
1126 */
swap_default_for_map(value_table_t * table,type_t tau,uint32_t n,value_t * a,value_t old_def,value_t new_def)1127 static uint32_t swap_default_for_map(value_table_t *table, type_t tau, uint32_t n, value_t *a, value_t old_def, value_t new_def) {
1128 value_t buffer[10];
1129 value_t *aux;
1130 function_type_t *ft;
1131 map_hset_t *hset;
1132 uint32_t i, j, m, dsize;
1133 value_t k;
1134
1135 assert(old_def != new_def);
1136
1137 // add all the current maps of a to hset2
1138 hset = get_hset2(table);
1139 reset_map_hset(hset);
1140 for (i=0; i<n; i++) {
1141 hset_add_map(table, hset, a[i]);
1142 }
1143
1144 ft = function_type_desc(table->type_table, tau);
1145 m = ft->ndom; // function arity
1146
1147 aux = buffer;
1148 if (m > 10) {
1149 assert(m < UINT32_MAX/sizeof(value_t));
1150 aux = (value_t *) safe_malloc(m * sizeof(value_t));
1151 }
1152
1153 dsize = card_of_domain_type(table->type_table, tau);
1154 assert(dsize < UINT32_MAX); // i.e., dsize is the exact cardinality
1155
1156 /*
1157 * scan all tuples in domain of tau
1158 * for each tuple: search for a matching map in hset2
1159 * - if there's none add the map [tuple -> old_def] to a
1160 * - if the map's value is equal to new_def skip it
1161 * - otherwise, add it to a
1162 */
1163 j = 0;
1164 for (i=0; i<dsize; i++) {
1165 vtbl_gen_object_tuple(table, m, ft->domain, i, aux);
1166 k = hset_find_map(table, hset, aux, m);
1167 if (k < 0) {
1168 k = vtbl_mk_map(table, m, aux, old_def);
1169 a[j] = k;
1170 j ++;
1171 } else if (vtbl_map_result(table, k) != new_def) {
1172 a[j] = k;
1173 j ++;
1174 }
1175 }
1176
1177 if (m > 10) {
1178 safe_free(aux);
1179 }
1180
1181 assert(j <= n);
1182 int_array_sort(a, j);
1183
1184 return j;
1185 }
1186
1187
1188 /*
1189 * Normalize a function with finite domain
1190 * - tau = function type
1191 * - a = mappings for the function
1192 * - n = number of elements in a
1193 * - *def = current default value
1194 *
1195 * If the representation is changed then a and *def are modified and
1196 * the function returns the number of elements in a. Otherwise, the function returns n.
1197 *
1198 * NOTE: this must be called after the standard normalization procedure:
1199 * - array a must not contain duplicate maps nor any map that gives the same value as def
1200 */
normalize_finite_domain_function(value_table_t * table,type_t tau,uint32_t n,value_t * a,value_t * def)1201 static uint32_t normalize_finite_domain_function(value_table_t *table, type_t tau, uint32_t n, value_t *a, value_t *def) {
1202 uint32_t dsize, def_count, new_count;
1203 value_t new_def;
1204
1205 assert(!object_is_unknown(table, *def) && type_has_finite_domain(table->type_table, tau));
1206
1207 dsize = card_of_domain_type(table->type_table, tau);
1208 def_count = dsize - n;
1209 if (n >= def_count) {
1210 /*
1211 * Check whether some other v in the range of a[0 ... n] occurs more
1212 * often than def_count
1213 */
1214 new_def = get_default_for_map(table, n, a, &new_count);
1215 if (new_count > def_count || (new_count == def_count && new_def < *def)) {
1216 n = swap_default_for_map(table, tau, n, a, *def, new_def);
1217 *def = new_def;
1218 }
1219 }
1220
1221 return n;
1222 }
1223
1224
1225 /***************
1226 * UTILITIES *
1227 **************/
1228
1229 /*
1230 * Check whether a and b are equal arrays
1231 * - both must have size n
1232 */
equal_arrays(value_t * a,value_t * b,uint32_t n)1233 static bool equal_arrays(value_t *a, value_t *b, uint32_t n) {
1234 uint32_t i;
1235
1236 for (i=0; i<n; i++) {
1237 if (a[i] != b[i]) return false;
1238 }
1239 return true;
1240 }
1241
1242
1243 /*
1244 * Check whether all elements in a are canonical
1245 */
canonical_array(value_table_t * table,value_t * a,uint32_t n)1246 static bool canonical_array(value_table_t *table, value_t *a, uint32_t n) {
1247 uint32_t i;
1248
1249 for (i=0; i<n; i++) {
1250 if (! object_is_canonical(table, a[i])) {
1251 return false;
1252 }
1253 }
1254
1255 return true;
1256 }
1257
1258
1259
1260
1261 /********************
1262 * HASH CONSING *
1263 *******************/
1264
1265 /*
1266 * There's a hobj for rationals, unint, bitvectors, tuples, and map objects.
1267 * Each hobj structure starts with a function descriptor m
1268 * with three fields:
1269 * m.hash = compute hash code
1270 * m.eq = check equality
1271 * m.build = build a fresh value
1272 *
1273 * For map objects, hash-consing relies only on the function and arguments:
1274 * - all map objects with the same function must have the same number of arguments.
1275 * - two maps objects with the same function and arguments must also have the
1276 * same result.
1277 */
1278 typedef struct {
1279 int_hobj_t m;
1280 value_table_t *table;
1281 rational_t *v;
1282 } rational_hobj_t;
1283
1284 typedef struct {
1285 int_hobj_t m;
1286 value_table_t *table;
1287 void *a;
1288 } algebraic_hobj_t;
1289
1290 typedef struct {
1291 int_hobj_t m;
1292 value_table_t *table;
1293 type_t tau;
1294 int32_t id;
1295 } const_hobj_t;
1296
1297 typedef struct {
1298 int_hobj_t m;
1299 value_table_t *table;
1300 uint32_t nbits;
1301 uint32_t *data; // must be normalized modulo (2^nbits)
1302 } bv_hobj_t;
1303
1304 typedef struct {
1305 int_hobj_t m;
1306 value_table_t *table;
1307 uint32_t nelems;
1308 value_t *elem;
1309 } tuple_hobj_t;
1310
1311 typedef struct {
1312 int_hobj_t m;
1313 value_table_t *table;
1314 uint32_t arity;
1315 value_t *arg;
1316 value_t val;
1317 } map_hobj_t;
1318
1319
1320
1321 /*
1322 * Function representation:
1323 * - a default value (can be unknown)
1324 * - an array map[0... n-1] of mapping objects sorted
1325 */
1326 typedef struct {
1327 int_hobj_t m;
1328 value_table_t *table;
1329 type_t type;
1330 uint32_t arity;
1331 value_t def;
1332 uint32_t map_size;
1333 value_t *map;
1334 bool ambiguous;
1335 } fun_hobj_t;
1336
1337
1338 /*
1339 * Function update: for hash-consing, the update
1340 * is converted into a function representation as above
1341 * - default value + map array
1342 */
1343 typedef struct {
1344 int_hobj_t m;
1345 value_table_t *table;
1346 type_t type;
1347 uint32_t arity;
1348 value_t fun;
1349 value_t updt;
1350
1351 value_t def;
1352 uint32_t map_size;
1353 value_t *map;
1354 bool ambiguous;
1355 } update_hobj_t;
1356
1357
1358 /*
1359 * Hash functions
1360 */
hash_rational_value(rational_hobj_t * o)1361 static uint32_t hash_rational_value(rational_hobj_t *o) {
1362 uint32_t h_num, h_den;
1363 q_hash_decompose(o->v, &h_num, &h_den);
1364 return jenkins_hash_mix2(h_num, h_den);
1365 }
1366
hash_algebraic_value(void * a)1367 static uint32_t hash_algebraic_value(void *a) {
1368 // Can't hash, internal representation can change and they are not canonical
1369 // We just return 0 and hope for the best
1370 return 0;
1371 }
1372
hash_const_value(const_hobj_t * o)1373 static uint32_t hash_const_value(const_hobj_t *o) {
1374 return jenkins_hash_pair(o->tau, o->id, 0x417a6eca);
1375 }
1376
hash_bv_value(bv_hobj_t * o)1377 static uint32_t hash_bv_value(bv_hobj_t *o) {
1378 return bvconst_hash(o->data, o->nbits);
1379 }
1380
hash_tuple_value(tuple_hobj_t * o)1381 static uint32_t hash_tuple_value(tuple_hobj_t *o) {
1382 return jenkins_hash_intarray2(o->elem, o->nelems, 0x21398aba);
1383 }
1384
hash_map_value(map_hobj_t * o)1385 static uint32_t hash_map_value(map_hobj_t *o) {
1386 uint32_t h;
1387
1388 h = jenkins_hash_intarray2(o->arg, o->arity, 0xabde6320);
1389 return jenkins_hash_pair(o->val, 0, h);
1390 }
1391
hash_fun_value(fun_hobj_t * o)1392 static uint32_t hash_fun_value(fun_hobj_t *o) {
1393 uint32_t h;
1394
1395 h = jenkins_hash_intarray2(o->map, o->map_size, 0x9765aef5);
1396 return jenkins_hash_pair(o->def, 0, h);
1397 }
1398
hash_update_value(update_hobj_t * o)1399 static uint32_t hash_update_value(update_hobj_t *o) {
1400 uint32_t h;
1401
1402 h = jenkins_hash_intarray2(o->map, o->map_size, 0x9765aef5);
1403 return jenkins_hash_pair(o->def, 0, h);
1404 }
1405
1406
1407
1408 /*
1409 * Equality testing: compare the object being constructed with
1410 * an existing value of index i in the table.
1411 */
equal_rational_value(rational_hobj_t * o,value_t i)1412 static bool equal_rational_value(rational_hobj_t *o, value_t i) {
1413 value_table_t *table;
1414
1415 table = o->table;
1416 return table->kind[i] == RATIONAL_VALUE && q_eq(&table->desc[i].rational, o->v);
1417 }
1418
equal_algebraic_value(algebraic_hobj_t * o,value_t i)1419 static bool equal_algebraic_value(algebraic_hobj_t *o, value_t i) {
1420 #ifdef HAVE_MCSAT
1421 value_table_t *table;
1422
1423 table = o->table;
1424 return table->kind[i] == ALGEBRAIC_VALUE && lp_algebraic_number_cmp(table->desc[i].ptr, o->a) == 0;
1425 #else
1426 assert(false);
1427 return false;
1428 #endif
1429
1430 }
1431
equal_const_value(const_hobj_t * o,value_t i)1432 static bool equal_const_value(const_hobj_t *o, value_t i) {
1433 value_table_t *table;
1434 value_unint_t *d;
1435
1436 table = o->table;
1437 if (table->kind[i] != UNINTERPRETED_VALUE) {
1438 return false;
1439 }
1440 d = table->desc[i].ptr;
1441 return d->type == o->tau && d->index == o->id;
1442 }
1443
equal_bv_value(bv_hobj_t * o,value_t i)1444 static bool equal_bv_value(bv_hobj_t *o, value_t i) {
1445 value_table_t *table;
1446 value_bv_t *d;
1447
1448 table = o->table;
1449 if (table->kind[i] != BITVECTOR_VALUE) {
1450 return false;
1451 }
1452 d = table->desc[i].ptr;
1453 return d->nbits == o->nbits && bvconst_eq(d->data, o->data, d->width);
1454 }
1455
1456
equal_tuple_value(tuple_hobj_t * o,value_t i)1457 static bool equal_tuple_value(tuple_hobj_t *o, value_t i) {
1458 value_table_t *table;
1459 value_tuple_t *d;
1460
1461 table = o->table;
1462 if (table->kind[i] != TUPLE_VALUE) {
1463 return false;
1464 }
1465 d = table->desc[i].ptr;
1466 return d->nelems == o->nelems && equal_arrays(o->elem, d->elem, d->nelems);
1467 }
1468
equal_map_value(map_hobj_t * o,value_t i)1469 static bool equal_map_value(map_hobj_t *o, value_t i) {
1470 value_table_t *table;
1471 value_map_t *d;
1472
1473 table = o->table;
1474 if (table->kind[i] != MAP_VALUE) {
1475 return false;
1476 }
1477 d = table->desc[i].ptr;
1478 return d->val == o->val && d->arity == o->arity && equal_arrays(o->arg, d->arg, d->arity);
1479 }
1480
1481
equal_fun_value(fun_hobj_t * o,value_t i)1482 static bool equal_fun_value(fun_hobj_t *o, value_t i) {
1483 value_table_t *table;
1484 value_fun_t *f;
1485 map_hset_t *hset;
1486 type_t tau;
1487 value_t def;
1488
1489 table = o->table;
1490 switch (table->kind[i]) {
1491 case FUNCTION_VALUE:
1492 f = (value_fun_t *) table->desc[i].ptr;
1493 return f->type == o->type && f->def == o->def
1494 && f->map_size == o->map_size
1495 && equal_arrays(f->map, o->map, o->map_size);
1496
1497 case UPDATE_VALUE:
1498 hset = get_hset2(table);
1499 reset_map_hset(hset);
1500 normalize_update(table, i, hset, &def, &tau);
1501 return tau == o->type && def == o->def
1502 && o->map_size == hset->nelems
1503 && equal_arrays(hset->data, o->map, o->map_size);
1504
1505 default:
1506 return false;
1507 }
1508 }
1509
1510
equal_update_value(update_hobj_t * o,value_t i)1511 static bool equal_update_value(update_hobj_t *o, value_t i) {
1512 value_table_t *table;
1513 value_fun_t *f;
1514 map_hset_t *hset;
1515 type_t tau;
1516 value_t def;
1517
1518 table = o->table;
1519 switch (table->kind[i]) {
1520 case FUNCTION_VALUE:
1521 f = (value_fun_t *) table->desc[i].ptr;
1522 return f->type == o->type && f->def == o->def
1523 && f->map_size == o->map_size
1524 && equal_arrays(f->map, o->map, o->map_size);
1525
1526 case UPDATE_VALUE:
1527 hset = get_hset2(table);
1528 reset_map_hset(hset);
1529 normalize_update(table, i, hset, &def, &tau);
1530 return tau == o->type && def == o->def
1531 && o->map_size == hset->nelems
1532 && equal_arrays(hset->data, o->map, o->map_size);
1533
1534 default:
1535 return false;
1536 }
1537 }
1538
1539
1540
1541 /*
1542 * Constructors
1543 */
build_rational_value(rational_hobj_t * o)1544 static value_t build_rational_value(rational_hobj_t *o) {
1545 value_table_t *table;
1546 value_t i;
1547
1548 table = o->table;
1549 i = allocate_object(table);
1550 table->kind[i] = RATIONAL_VALUE;
1551 q_init(&table->desc[i].rational);
1552 q_set(&table->desc[i].rational, o->v);
1553 set_bit(table->canonical, i);
1554
1555 return i;
1556 }
1557
build_algebraic_value(algebraic_hobj_t * o)1558 static value_t build_algebraic_value(algebraic_hobj_t *o) {
1559 #ifdef HAVE_MCSAT
1560 value_table_t *table;
1561 value_t i;
1562
1563 table = o->table;
1564 i = allocate_object(table);
1565 table->kind[i] = ALGEBRAIC_VALUE;
1566 table->desc[i].ptr = safe_malloc(sizeof(lp_algebraic_number_t));
1567 lp_algebraic_number_construct_copy(table->desc[i].ptr, o->a);
1568 clr_bit(table->canonical, i);
1569
1570 return i;
1571 #else
1572 return null_value;
1573 #endif
1574 }
1575
1576
build_const_value(const_hobj_t * o)1577 static value_t build_const_value(const_hobj_t *o) {
1578 value_table_t *table;
1579 value_unint_t *d;
1580 value_t i;
1581
1582 d = (value_unint_t *) safe_malloc(sizeof(value_unint_t));
1583 d->type = o->tau;
1584 d->index = o->id;
1585 d->name = NULL;
1586
1587
1588 table = o->table;
1589 i = allocate_object(table);
1590 table->kind[i] = UNINTERPRETED_VALUE;
1591 table->desc[i].ptr = d;
1592 set_bit(table->canonical, i);
1593
1594 return i;
1595 }
1596
build_bv_value(bv_hobj_t * o)1597 static value_t build_bv_value(bv_hobj_t *o) {
1598 value_table_t *table;
1599 value_bv_t *d;
1600 uint32_t w;
1601 value_t i;
1602
1603 w = (o->nbits + 31) >> 5; // ceil(nbits/32)
1604 d = (value_bv_t *) safe_malloc(sizeof(value_bv_t) + w * sizeof(uint32_t));
1605 d->nbits = o->nbits;
1606 d->width = w;
1607 bvconst_set(d->data, w, o->data);
1608
1609 table = o->table;
1610 i = allocate_object(table);
1611 table->kind[i] = BITVECTOR_VALUE;
1612 table->desc[i].ptr = d;
1613 set_bit(table->canonical, i);
1614
1615 return i;
1616 }
1617
1618
build_tuple_value(tuple_hobj_t * o)1619 static value_t build_tuple_value(tuple_hobj_t *o) {
1620 value_table_t *table;
1621 value_tuple_t *d;
1622 uint32_t j, n;
1623 value_t i;
1624
1625
1626 n = o->nelems;
1627 if (n >= VTBL_MAX_TUPLE_SIZE) {
1628 out_of_memory();
1629 }
1630 d = (value_tuple_t *) safe_malloc(sizeof(value_tuple_t) + n * sizeof(value_t));
1631 d->nelems = n;
1632 for (j=0; j<n; j++) {
1633 d->elem[j] = o->elem[j];
1634
1635 }
1636
1637 table = o->table;
1638 i = allocate_object(table);
1639 table->kind[i] = TUPLE_VALUE;
1640 table->desc[i].ptr = d;
1641
1642 if (canonical_array(table, d->elem, n)) {
1643 set_bit(table->canonical, i);
1644 } else {
1645 clr_bit(table->canonical, i);
1646 }
1647
1648 return i;
1649 }
1650
1651
build_map_value(map_hobj_t * o)1652 static value_t build_map_value(map_hobj_t *o) {
1653 value_table_t *table;
1654 value_map_t *d;
1655 uint32_t j, n;
1656 value_t i;
1657
1658 n = o->arity;
1659 if (n >= VTBL_MAX_MAP_ARITY) {
1660 out_of_memory();
1661 }
1662 d = (value_map_t *) safe_malloc(sizeof(value_map_t) + n * sizeof(value_t));
1663 d->arity = n;
1664 d->val = o->val;
1665 for (j=0; j<n; j++) {
1666 d->arg[j] = o->arg[j];
1667 }
1668
1669 table = o->table;
1670 i = allocate_object(table);
1671 table->kind[i] = MAP_VALUE;
1672 table->desc[i].ptr = d;
1673
1674 if (canonical_array(table, d->arg, n) && object_is_canonical(table, d->val)) {
1675 set_bit(table->canonical, i);
1676 } else {
1677 clr_bit(table->canonical, i);
1678 }
1679
1680 return i;
1681 }
1682
1683
build_fun_value(fun_hobj_t * o)1684 static value_t build_fun_value(fun_hobj_t *o) {
1685 value_table_t *table;
1686 value_fun_t *fun;
1687 value_t f, i;
1688 uint32_t j, n;
1689
1690 table = o->table;
1691
1692 n = o->map_size;
1693 if (n >= VTBL_MAX_MAP_SIZE) {
1694 out_of_memory();
1695 }
1696 fun = (value_fun_t *) safe_malloc(sizeof(value_fun_t) + n * sizeof(value_t));
1697 fun->name = NULL;
1698 fun->type = o->type;
1699 fun->arity = o->arity;
1700 fun->map_size = n;
1701 fun->def = o->def;
1702
1703 f = allocate_object(table);
1704 table->kind[f] = FUNCTION_VALUE;
1705 table->desc[f].ptr = fun;
1706
1707 for (j=0; j<n; j++) {
1708 i = o->map[j];
1709 fun->map[j] = i;
1710 add_hash_pair(table, f, i);
1711 }
1712
1713 // set the canonical flag
1714 if (!o->ambiguous && object_is_canonical(table, fun->def) &&
1715 canonical_array(table, fun->map, n)) {
1716 set_bit(table->canonical, f);
1717 } else {
1718 clr_bit(table->canonical, f);
1719 }
1720
1721 return f;
1722 }
1723
1724
build_update_value(update_hobj_t * o)1725 static value_t build_update_value(update_hobj_t *o) {
1726 value_table_t *table;
1727 value_update_t *d;
1728 value_t i;
1729
1730 d = (value_update_t *) safe_malloc(sizeof(value_update_t));
1731 d->arity = o->arity;
1732 d->fun = o->fun;
1733 d->map = o->updt;
1734
1735 table = o->table;
1736 i = allocate_object(table);
1737 table->kind[i] = UPDATE_VALUE;
1738 table->desc[i].ptr = d;
1739
1740 // set the canonical flag
1741 if (!o->ambiguous && object_is_canonical(table, o->def) &&
1742 canonical_array(table, o->map, o->map_size)) {
1743 set_bit(table->canonical, i);
1744 } else {
1745 clr_bit(table->canonical, i);
1746 }
1747
1748 return i;
1749 }
1750
1751 /*
1752 * Return a rational constant = v
1753 */
vtbl_mk_rational(value_table_t * table,rational_t * v)1754 value_t vtbl_mk_rational(value_table_t *table, rational_t *v) {
1755 rational_hobj_t rational_hobj;
1756 rational_hobj.m.hash = (hobj_hash_t) hash_rational_value;
1757 rational_hobj.m.eq = (hobj_eq_t) equal_rational_value;
1758 rational_hobj.m.build = (hobj_build_t) build_rational_value;
1759 rational_hobj.table = table;
1760 rational_hobj.v = v;
1761
1762 return int_htbl_get_obj(&table->htbl, (int_hobj_t *) &rational_hobj);
1763 }
1764
1765 /*
1766 * Return a rational constant equal to i
1767 */
vtbl_mk_int32(value_table_t * table,int32_t i)1768 value_t vtbl_mk_int32(value_table_t *table, int32_t i) {
1769 rational_t aux;
1770 value_t k;
1771 rational_hobj_t rational_hobj;
1772
1773 q_init(&aux);
1774 q_set32(&aux, i);
1775
1776 rational_hobj.m.hash = (hobj_hash_t) hash_rational_value;
1777 rational_hobj.m.eq = (hobj_eq_t) equal_rational_value;
1778 rational_hobj.m.build = (hobj_build_t) build_rational_value;
1779 rational_hobj.table = table;
1780 rational_hobj.v = &aux;
1781
1782 k = int_htbl_get_obj(&table->htbl, (int_hobj_t *) &rational_hobj);
1783 q_clear(&aux);
1784
1785 return k;
1786 }
1787
1788
1789 /*
1790 * Copy of the algebraic number
1791 */
vtbl_mk_algebraic(value_table_t * table,void * a)1792 value_t vtbl_mk_algebraic(value_table_t *table, void* a) {
1793 #ifdef HAVE_MCSAT
1794 algebraic_hobj_t algebraic_hobj;
1795
1796 algebraic_hobj.m.hash = (hobj_hash_t) hash_algebraic_value;
1797 algebraic_hobj.m.eq = (hobj_eq_t) equal_algebraic_value;
1798 algebraic_hobj.m.build = (hobj_build_t) build_algebraic_value;
1799 algebraic_hobj.table = table;
1800 algebraic_hobj.a = a;
1801
1802 return int_htbl_get_obj(&table->htbl, (int_hobj_t *) &algebraic_hobj);
1803 #else
1804 return null_value;
1805 #endif
1806 }
1807
1808
1809 /*
1810 * Bit vector constant: defined by array a:
1811 * - a[i] = 0 means bit[i] = 0
1812 * - a[i] != 0 means bit[i] = 1
1813 */
vtbl_mk_bv(value_table_t * table,uint32_t n,int32_t * a)1814 value_t vtbl_mk_bv(value_table_t *table, uint32_t n, int32_t *a) {
1815 bvconstant_t *b;
1816 bv_hobj_t bv_hobj;
1817
1818 // copy the constant in table's buffer
1819 b = &table->buffer;
1820 bvconstant_set_bitsize(b, n);
1821 bvconst_set_array(b->data, a, n);
1822 bvconst_normalize(b->data, n);
1823
1824 // hash-consing
1825 bv_hobj.m.hash = (hobj_hash_t) hash_bv_value;
1826 bv_hobj.m.eq = (hobj_eq_t) equal_bv_value;
1827 bv_hobj.m.build = (hobj_build_t) build_bv_value;
1828 bv_hobj.table = table;
1829 bv_hobj.nbits = n;
1830 bv_hobj.data = b->data;
1831 return int_htbl_get_obj(&table->htbl, (int_hobj_t *) &bv_hobj);
1832 }
1833
1834
1835
1836 /*
1837 * Bit vector constant defined by an array of words
1838 * - n = number of bits
1839 * - a = array of w words (w = ceil(n/32)
1840 */
vtbl_mk_bv_from_bv(value_table_t * table,uint32_t n,uint32_t * a)1841 value_t vtbl_mk_bv_from_bv(value_table_t *table, uint32_t n, uint32_t *a) {
1842 bv_hobj_t bv_hobj;
1843
1844 bvconst_normalize(a, n);
1845
1846 bv_hobj.m.hash = (hobj_hash_t) hash_bv_value;
1847 bv_hobj.m.eq = (hobj_eq_t) equal_bv_value;
1848 bv_hobj.m.build = (hobj_build_t) build_bv_value;
1849 bv_hobj.table = table;
1850 bv_hobj.nbits = n;
1851 bv_hobj.data = a;
1852 return int_htbl_get_obj(&table->htbl, (int_hobj_t*) &bv_hobj);
1853 }
1854
1855
1856 /*
1857 * Bit vector constant defined by a bvconstant_t object
1858 * - b->bitsize = number of bits
1859 * - b->data = array of 32bit words
1860 */
vtbl_mk_bv_from_constant(value_table_t * table,bvconstant_t * b)1861 value_t vtbl_mk_bv_from_constant(value_table_t *table, bvconstant_t *b) {
1862 return vtbl_mk_bv_from_bv(table, b->bitsize, b->data);
1863 }
1864
1865
1866 /*
1867 * Bit vector constant defined by a 64bit integer c
1868 * - n = number of bits to use
1869 */
vtbl_mk_bv_from_bv64(value_table_t * table,uint32_t n,uint64_t c)1870 value_t vtbl_mk_bv_from_bv64(value_table_t *table, uint32_t n, uint64_t c) {
1871 uint32_t aux[2];
1872
1873 aux[0] = (uint32_t) c;
1874 aux[1] = (uint32_t) (c >> 32);
1875 return vtbl_mk_bv_from_bv(table, n, aux);
1876 }
1877
1878
1879 /*
1880 * Bitvector constant with all bits 0
1881 * - n = number of bits
1882 */
vtbl_mk_bv_zero(value_table_t * table,uint32_t n)1883 value_t vtbl_mk_bv_zero(value_table_t *table, uint32_t n) {
1884 bvconstant_t *b;
1885 bv_hobj_t bv_hobj;
1886
1887 assert(n > 0);
1888
1889 // store 0b000...0 in the buffer
1890 b = &table->buffer;
1891 bvconstant_set_all_zero(b, n);
1892
1893 bv_hobj.m.hash = (hobj_hash_t) hash_bv_value;
1894 bv_hobj.m.eq = (hobj_eq_t) equal_bv_value;
1895 bv_hobj.m.build = (hobj_build_t) build_bv_value;
1896 bv_hobj.table = table;
1897 bv_hobj.nbits = n;
1898 bv_hobj.data = b->data;
1899
1900 return int_htbl_get_obj(&table->htbl, (int_hobj_t *) &bv_hobj);
1901 }
1902
1903
1904 /*
1905 * Bitvector constant with all bits 0, except the low-order bit
1906 * - n = number of bits
1907 */
vtbl_mk_bv_one(value_table_t * table,uint32_t n)1908 value_t vtbl_mk_bv_one(value_table_t *table, uint32_t n) {
1909 bvconstant_t *b;
1910 bv_hobj_t bv_hobj;
1911
1912 assert(n > 0);
1913
1914 // store 0b000..01 in the buffer
1915 b = &table->buffer;
1916 bvconstant_set_all_zero(b, n);
1917 bvconst_set_bit(b->data, 0);
1918
1919 bv_hobj.m.hash = (hobj_hash_t) hash_bv_value;
1920 bv_hobj.m.eq = (hobj_eq_t) equal_bv_value;
1921 bv_hobj.m.build = (hobj_build_t) build_bv_value;
1922 bv_hobj.table = table;
1923 bv_hobj.nbits = n;
1924 bv_hobj.data = b->data;
1925
1926 return int_htbl_get_obj(&table->htbl, (int_hobj_t *) &bv_hobj);
1927 }
1928
1929
1930 /*
1931 * Tuple (e[0] ... e[n-1])
1932 */
vtbl_mk_tuple(value_table_t * table,uint32_t n,value_t * e)1933 value_t vtbl_mk_tuple(value_table_t *table, uint32_t n, value_t *e) {
1934 tuple_hobj_t tuple_hobj;
1935
1936 tuple_hobj.m.hash = (hobj_hash_t) hash_tuple_value;
1937 tuple_hobj.m.eq = (hobj_eq_t) equal_tuple_value;
1938 tuple_hobj.m.build = (hobj_build_t) build_tuple_value;
1939 tuple_hobj.table = table;
1940 tuple_hobj.nelems = n;
1941 tuple_hobj.elem = e;
1942
1943 return int_htbl_get_obj(&table->htbl, (int_hobj_t *) &tuple_hobj);
1944 }
1945
1946
1947 /*
1948 * Constant of type tau and index id
1949 * - name = optional name
1950 */
vtbl_mk_const(value_table_t * table,type_t tau,int32_t id,char * name)1951 value_t vtbl_mk_const(value_table_t *table, type_t tau, int32_t id, char *name) {
1952 value_unint_t *d;
1953 value_t v;
1954 const_hobj_t const_hobj;
1955
1956 assert(type_kind(table->type_table, tau) == SCALAR_TYPE ||
1957 type_kind(table->type_table, tau) == UNINTERPRETED_TYPE ||
1958 type_kind(table->type_table, tau) == INSTANCE_TYPE);
1959 assert(0 <= id);
1960
1961 const_hobj.m.hash = (hobj_hash_t) hash_const_value;
1962 const_hobj.m.eq = (hobj_eq_t) equal_const_value;
1963 const_hobj.m.build = (hobj_build_t) build_const_value;
1964 const_hobj.table = table;
1965 const_hobj.tau = tau;
1966 const_hobj.id = id;
1967 v = int_htbl_get_obj(&table->htbl, (int_hobj_t *) &const_hobj);
1968
1969 // set the name if needed
1970 assert(table->kind[v] == UNINTERPRETED_VALUE);
1971 d = table->desc[v].ptr;
1972 if (name != NULL && d->name == NULL) {
1973 d->name = (char *) safe_malloc(strlen(name) + 1);
1974 strcpy(d->name, name);
1975 }
1976
1977 return v;
1978 }
1979
1980
1981
1982
1983 /*
1984 * Mapping object (a[0] ... a[n-1] |-> v)
1985 * - return a mapping object
1986 */
vtbl_mk_map(value_table_t * table,uint32_t n,value_t * a,value_t v)1987 value_t vtbl_mk_map(value_table_t *table, uint32_t n, value_t *a, value_t v) {
1988 map_hobj_t map_hobj;
1989
1990 map_hobj.m.hash = (hobj_hash_t) hash_map_value;
1991 map_hobj.m.eq = (hobj_eq_t) equal_map_value;
1992 map_hobj.m.build = (hobj_build_t) build_map_value;
1993 map_hobj.table = table;
1994 map_hobj.arity = n;
1995 map_hobj.arg = a;
1996 map_hobj.val = v;
1997
1998 return int_htbl_get_obj(&table->htbl, (int_hobj_t *) &map_hobj);
1999 }
2000
2001
2002
2003
2004 /*
2005 * Function defined by the array a[0...n-1] and default value def
2006 * - tau = its type
2007 * - a = array of n mapping objects.
2008 * The array must not contain conflicting mappings and all elements in a
2009 * must have the right arity (same as defined by type tau). It's allowed
2010 * to have duplicate elements in a.
2011 * - def = default value (must be unknown if no default is given)
2012 *
2013 * NOTE: a is modified by the function.
2014 */
vtbl_mk_function(value_table_t * table,type_t tau,uint32_t n,value_t * a,value_t def)2015 value_t vtbl_mk_function(value_table_t *table, type_t tau, uint32_t n, value_t *a, value_t def) {
2016 fun_hobj_t fun_hobj;
2017
2018 assert(good_object(table, def));
2019
2020 // normalize a
2021 n = normalize_map_array(n, a);
2022 if (! object_is_unknown(table, def)) {
2023 n = remove_redundant_mappings(table, n, a, def);
2024 }
2025
2026 // if the function has finite domain and the default is something other than unknown
2027 // we may need more normalization
2028 if (type_has_finite_domain(table->type_table, tau) && !object_is_unknown(table, def)) {
2029 n = normalize_finite_domain_function(table, tau, n, a, &def);
2030 }
2031
2032 fun_hobj.m.hash = (hobj_hash_t) hash_fun_value;
2033 fun_hobj.m.eq = (hobj_eq_t) equal_fun_value;
2034 fun_hobj.m.build = (hobj_build_t) build_fun_value;
2035 fun_hobj.table = table;
2036 fun_hobj.type = tau;
2037 fun_hobj.arity = function_type_arity(table->type_table, tau);
2038 fun_hobj.def = def;
2039 fun_hobj.map_size = n;
2040 fun_hobj.map = a;
2041 fun_hobj.ambiguous = false;
2042
2043 return int_htbl_get_obj(&table->htbl, (int_hobj_t*) &fun_hobj);
2044 }
2045
2046
2047
2048 /*
2049 * Create (update f (a[0] ... a[n-1]) v)
2050 */
vtbl_mk_update(value_table_t * table,value_t f,uint32_t n,value_t * a,value_t v)2051 value_t vtbl_mk_update(value_table_t *table, value_t f, uint32_t n, value_t *a, value_t v) {
2052 map_hset_t *hset;
2053 value_t u;
2054 value_t def;
2055 type_t tau;
2056 update_hobj_t update_hobj;
2057
2058 // build the mapping [a[0] ... a[n-1] --> v]
2059 u = vtbl_mk_map(table, n, a, v);
2060
2061 // normalize: add mapping u + normalization of f
2062 hset = get_hset1(table);
2063 reset_map_hset(hset);
2064 hset_add_map(table, hset, u);
2065 normalize_update(table, f, hset, &def, &tau);
2066
2067
2068 // hash consing
2069 update_hobj.m.hash = (hobj_hash_t) hash_update_value;
2070 update_hobj.m.eq = (hobj_eq_t) equal_update_value;
2071 update_hobj.m.build = (hobj_build_t) build_update_value;
2072
2073 update_hobj.table = table;
2074 update_hobj.type = tau;
2075 update_hobj.arity = function_type_arity(table->type_table, tau);
2076 update_hobj.fun = f;
2077 update_hobj.updt = u;
2078 update_hobj.def = def;
2079 update_hobj.map_size = hset->nelems;
2080 update_hobj.map = hset->data;
2081 update_hobj.ambiguous = type_has_finite_domain(table->type_table, tau) &&
2082 !object_is_unknown(table, def);
2083
2084 return int_htbl_get_obj(&table->htbl, (int_hobj_t*) &update_hobj);
2085 }
2086
2087
2088
2089 /***********************************************
2090 * LOCAL INTERPRETATION FOR DIVISION BY ZERO *
2091 **********************************************/
2092
2093 /*
2094 * In SMT-LIB 2.x, the division operators have an uninterpreted
2095 * semantics if the divisor is zero. The value table can store
2096 * a mapping that gives an interpretation for these operations.
2097 *
2098 * Example: if mcsat says (/ 1 0) = 5 then we can build a function f
2099 * that maps 1 to 5, then assign f to table->zero_rdiv_fun. We store
2100 * this information in the value table so that model_eval can use it.
2101 */
2102
2103 #ifndef NDEBUG
is_arith_map_type(type_table_t * tbl,type_t tau)2104 static bool is_arith_map_type(type_table_t *tbl, type_t tau) {
2105 function_type_t *d;
2106
2107 if (is_function_type(tbl, tau)) {
2108 d = function_type_desc(tbl, tau);
2109 return d->ndom == 1 && is_arithmetic_type(d->range) && is_arithmetic_type(d->domain[0]);
2110 }
2111
2112 return false;
2113 }
2114
is_plausible_div_by_zero(value_table_t * table,value_t f)2115 static bool is_plausible_div_by_zero(value_table_t *table, value_t f) {
2116 value_fun_t *fun;
2117 value_update_t *upd;
2118
2119 while (object_is_update(table, f)) {
2120 upd = vtbl_update(table, f);
2121 if (upd->arity != 1) return false;
2122 f = upd->fun;
2123 }
2124
2125 if (object_is_function(table, f)) {
2126 fun = vtbl_function(table, f);
2127 return fun->arity == 1 && is_arith_map_type(table->type_table, fun->type);
2128 }
2129
2130 return false;
2131 }
2132 #endif
2133
2134 /*
2135 * Give a meaning to real division by zero
2136 */
vtbl_set_zero_rdiv(value_table_t * table,value_t f)2137 void vtbl_set_zero_rdiv(value_table_t *table, value_t f) {
2138 assert(is_plausible_div_by_zero(table, f));
2139 assert(table->zero_rdiv_fun == null_value);
2140 table->zero_rdiv_fun = f;
2141 }
2142
2143 /*
2144 * Integer division
2145 */
vtbl_set_zero_idiv(value_table_t * table,value_t f)2146 void vtbl_set_zero_idiv(value_table_t *table, value_t f) {
2147 assert(is_plausible_div_by_zero(table, f));
2148 assert(table->zero_idiv_fun == null_value);
2149 table->zero_idiv_fun = f;
2150 }
2151
2152 /*
2153 * Modulo
2154 */
vtbl_set_zero_mod(value_table_t * table,value_t f)2155 void vtbl_set_zero_mod(value_table_t *table, value_t f) {
2156 assert(is_plausible_div_by_zero(table, f));
2157 assert(table->zero_mod_fun == null_value);
2158 table->zero_mod_fun = f;
2159 }
2160
2161
2162
2163
2164 /********************
2165 * DEFAULT VALUES *
2166 *******************/
2167
2168 /*
2169 * Tuple object for the given type
2170 */
vtbl_make_tuple(value_table_t * vtbl,tuple_type_t * d)2171 static value_t vtbl_make_tuple(value_table_t *vtbl, tuple_type_t *d) {
2172 value_t buffer[10];
2173 value_t *aux;
2174 uint32_t i, n;
2175 value_t v;
2176
2177 n = d->nelem;
2178 aux = buffer;
2179 if (n > 10) {
2180 aux = (value_t *) safe_malloc(n * sizeof(value_t));
2181 }
2182
2183 for (i=0; i<n; i++) {
2184 aux[i] = vtbl_make_object(vtbl, d->elem[i]);
2185 }
2186 v = vtbl_mk_tuple(vtbl, n, aux);
2187
2188 if (n > 10) {
2189 safe_free(aux);
2190 }
2191
2192 return v;
2193 }
2194
2195
2196 /*
2197 * Return some value of type tau
2198 */
vtbl_make_object(value_table_t * vtbl,type_t tau)2199 value_t vtbl_make_object(value_table_t *vtbl, type_t tau) {
2200 type_table_t *types;
2201 value_t v;
2202
2203 types = vtbl->type_table;
2204
2205 switch (type_kind(types, tau)) {
2206 case BOOL_TYPE:
2207 v = vtbl_mk_false(vtbl);
2208 break;
2209
2210 case INT_TYPE:
2211 case REAL_TYPE:
2212 v = vtbl_mk_int32(vtbl, 0);
2213 break;
2214
2215 case BITVECTOR_TYPE:
2216 v = vtbl_mk_bv_zero(vtbl, bv_type_size(types, tau));
2217 break;
2218
2219 case SCALAR_TYPE:
2220 case UNINTERPRETED_TYPE:
2221 case INSTANCE_TYPE:
2222 // we treat an instance type as an uninterpreted tyoe
2223 v = vtbl_mk_const(vtbl, tau, 0, NULL);
2224 break;
2225
2226 case TUPLE_TYPE:
2227 v = vtbl_make_tuple(vtbl, tuple_type_desc(types, tau));
2228 break;
2229
2230 case FUNCTION_TYPE:
2231 v = vtbl_make_object(vtbl, function_type_range(types, tau));
2232 v = vtbl_mk_function(vtbl, tau, 0, NULL, v); // constant function
2233 break;
2234
2235 case VARIABLE_TYPE:
2236 default:
2237 // should not happen
2238 assert(false);
2239 v = vtbl_mk_unknown(vtbl);
2240 break;
2241 }
2242
2243 return v;
2244 }
2245
2246
2247
2248 /*
2249 * Create two distinct tuples of the given type
2250 */
vtbl_make_two_tuples(value_table_t * vtbl,tuple_type_t * d,value_t a[2])2251 static bool vtbl_make_two_tuples(value_table_t *vtbl, tuple_type_t *d, value_t a[2]) {
2252 value_t buffer[10];
2253 value_t *aux;
2254 uint32_t i, j, n;
2255 bool done;
2256
2257 done = false;
2258
2259 n = d->nelem;
2260 aux = buffer;
2261 if (n > 10) {
2262 aux = (value_t *) safe_malloc(n * sizeof(value_t));
2263 }
2264
2265 for (i=0; i<n; i++) {
2266 if (vtbl_make_two_objects(vtbl, d->elem[i], a)) {
2267 break;
2268 }
2269 }
2270 if (i < n) {
2271 // we have two elements for index i in a[0] and a[1]
2272 // fill in aux[0 ... n-1] except at position i
2273 for (j=0; j<n; j++) {
2274 if (j != i) {
2275 aux[j] = vtbl_make_object(vtbl, d->elem[j]);
2276 }
2277 }
2278
2279 // first tuple: aux[i] = a[0]
2280 aux[i] = a[0];
2281 a[0] = vtbl_mk_tuple(vtbl, n, aux);
2282 // second tuple: aux[i] = a[1]
2283 aux[i] = a[1];
2284 a[1] = vtbl_mk_tuple(vtbl, n, aux);
2285
2286 done = true;
2287 }
2288
2289 if (n > 10) {
2290 safe_free(aux);
2291 }
2292
2293 return done;
2294 }
2295
2296
2297 /*
2298 * Attempt to construct two distinct objects of type tau.
2299 * - return true if that succeeds, false if tau is a singleton type
2300 * - store the two objects in a[0] and a[1]
2301 */
vtbl_make_two_objects(value_table_t * vtbl,type_t tau,value_t a[2])2302 bool vtbl_make_two_objects(value_table_t *vtbl, type_t tau, value_t a[2]) {
2303 type_table_t *types;
2304
2305 types = vtbl->type_table;
2306
2307 switch (type_kind(types, tau)) {
2308 case BOOL_TYPE:
2309 a[0] = vtbl_mk_false(vtbl);
2310 a[1] = vtbl_mk_true(vtbl);
2311 break;
2312
2313 case INT_TYPE:
2314 case REAL_TYPE:
2315 a[0] = vtbl_mk_int32(vtbl, 0);
2316 a[1] = vtbl_mk_int32(vtbl, 1);
2317 break;
2318
2319 case BITVECTOR_TYPE:
2320 a[0] = vtbl_mk_bv_zero(vtbl, bv_type_size(types, tau));
2321 a[1] = vtbl_mk_bv_one(vtbl, bv_type_size(types, tau));
2322 break;
2323
2324 case SCALAR_TYPE:
2325 if (is_unit_type(types, tau)) return false;
2326 assert(type_card(types, tau) >= 2);
2327 // fall-through intended
2328
2329 case UNINTERPRETED_TYPE:
2330 case INSTANCE_TYPE:
2331 a[0] = vtbl_mk_const(vtbl, tau, 0, NULL);
2332 a[1] = vtbl_mk_const(vtbl, tau, 1, NULL);
2333 break;
2334
2335 case TUPLE_TYPE:
2336 return vtbl_make_two_tuples(vtbl, tuple_type_desc(types, tau), a);
2337
2338 case FUNCTION_TYPE:
2339 // try to create two constant functions
2340 if (! vtbl_make_two_objects(vtbl, function_type_range(types, tau), a)) {
2341 return false;
2342 }
2343 // a[0] and a[1] are two objects of type sigma = range of tau
2344 a[0] = vtbl_mk_function(vtbl, tau, 0, NULL, a[0]);
2345 a[1] = vtbl_mk_function(vtbl, tau, 0, NULL, a[1]);
2346 break;
2347
2348 case VARIABLE_TYPE:
2349 default:
2350 assert(false);
2351 return false;
2352 }
2353
2354 return true;
2355 }
2356
2357
2358
2359
2360 /**************************************
2361 * TEST WHETHER OBJECTS ARE PRESENT *
2362 *************************************/
2363
2364 /*
2365 * Check whether a rational or integer constant is in the table
2366 * - return the object if found, -1 (i.e., null_value otherwise)
2367 */
vtbl_find_rational(value_table_t * table,rational_t * v)2368 value_t vtbl_find_rational(value_table_t *table, rational_t *v) {
2369 rational_hobj_t rational_hobj;
2370 rational_hobj.m.hash = (hobj_hash_t) hash_rational_value;
2371 rational_hobj.m.eq = (hobj_eq_t) equal_rational_value;
2372 rational_hobj.m.build = (hobj_build_t) build_rational_value;
2373 rational_hobj.table = table;
2374 rational_hobj.v = v;
2375
2376 return int_htbl_find_obj(&table->htbl, (int_hobj_t *) &rational_hobj);
2377 }
2378
vtbl_find_int32(value_table_t * table,int32_t x)2379 value_t vtbl_find_int32(value_table_t *table, int32_t x) {
2380 rational_t aux;
2381 value_t k;
2382 rational_hobj_t rational_hobj;
2383
2384 q_init(&aux);
2385 q_set32(&aux, x);
2386
2387 rational_hobj.m.hash = (hobj_hash_t) hash_rational_value;
2388 rational_hobj.m.eq = (hobj_eq_t) equal_rational_value;
2389 rational_hobj.m.build = (hobj_build_t) build_rational_value;
2390 rational_hobj.table = table;
2391 rational_hobj.v = &aux;
2392
2393 k = int_htbl_find_obj(&table->htbl, (int_hobj_t *) &rational_hobj);
2394 q_clear(&aux);
2395
2396 return k;
2397 }
2398
2399 /*
2400 * Check whether the algebraic number is in the table.
2401 */
vtbl_find_algebraic(value_table_t * table,void * a)2402 value_t vtbl_find_algebraic(value_table_t *table, void* a) {
2403 algebraic_hobj_t algebraic_hobj;
2404
2405 algebraic_hobj.m.hash = (hobj_hash_t) hash_algebraic_value;
2406 algebraic_hobj.m.eq = (hobj_eq_t) equal_algebraic_value;
2407 algebraic_hobj.m.build = (hobj_build_t) build_algebraic_value;
2408 algebraic_hobj.table = table;
2409 algebraic_hobj.a = a;
2410
2411 return int_htbl_find_obj(&table->htbl, (int_hobj_t *) &algebraic_hobj);
2412 }
2413
2414
2415 /*
2416 * Check presence of a bitvector constant defined by array of n integers:
2417 * - bit i is 0 if a[i] == 0
2418 * - bit i is 1 otherwise
2419 * - n = number of bits (must be positive).
2420 */
vtbl_find_bv(value_table_t * table,uint32_t n,int32_t * a)2421 value_t vtbl_find_bv(value_table_t *table, uint32_t n, int32_t *a) {
2422 bvconstant_t *b;
2423 bv_hobj_t bv_hobj;
2424
2425 // copy the constant in table's buffer
2426 b = &table->buffer;
2427 bvconstant_set_bitsize(b, n);
2428 bvconst_set_array(b->data, a, n);
2429 bvconst_normalize(b->data, n);
2430
2431 // hash-consing
2432 bv_hobj.m.hash = (hobj_hash_t) hash_bv_value;
2433 bv_hobj.m.eq = (hobj_eq_t) equal_bv_value;
2434 bv_hobj.m.build = (hobj_build_t) build_bv_value;
2435 bv_hobj.table = table;
2436 bv_hobj.nbits = n;
2437 bv_hobj.data = b->data;
2438
2439 return int_htbl_find_obj(&table->htbl, (int_hobj_t *) &bv_hobj);
2440 }
2441
2442 /*
2443 * Same thing for the bitvector defined by c:
2444 * - n = number of bits (must be <= 64)
2445 */
vtbl_find_bv64(value_table_t * table,uint32_t n,uint64_t c)2446 value_t vtbl_find_bv64(value_table_t *table, uint32_t n, uint64_t c) {
2447 uint32_t aux[2];
2448 bv_hobj_t bv_hobj;
2449
2450 c = norm64(c, n);
2451 aux[0] = (uint32_t) c;
2452 aux[1] = (uint32_t) (c >> 32);
2453
2454 bv_hobj.m.hash = (hobj_hash_t) hash_bv_value;
2455 bv_hobj.m.eq = (hobj_eq_t) equal_bv_value;
2456 bv_hobj.m.build = (hobj_build_t) build_bv_value;
2457 bv_hobj.table = table;
2458 bv_hobj.nbits = n;
2459 bv_hobj.data = aux;
2460 return int_htbl_find_obj(&table->htbl, (int_hobj_t *) &bv_hobj);
2461 }
2462
2463 /*
2464 * Same thing for the bitvector constant defined by b
2465 */
vtbl_find_bvconstant(value_table_t * table,bvconstant_t * b)2466 value_t vtbl_find_bvconstant(value_table_t *table, bvconstant_t *b) {
2467 uint32_t n;
2468 bv_hobj_t bv_hobj;
2469
2470 n = b->bitsize;
2471 bvconst_normalize(b->data, n);
2472 bv_hobj.m.hash = (hobj_hash_t) hash_bv_value;
2473 bv_hobj.m.eq = (hobj_eq_t) equal_bv_value;
2474 bv_hobj.m.build = (hobj_build_t) build_bv_value;
2475 bv_hobj.table = table;
2476 bv_hobj.nbits = n;
2477 bv_hobj.data = b->data;
2478 return int_htbl_find_obj(&table->htbl, (int_hobj_t *) &bv_hobj);
2479 }
2480
2481 /*
2482 * Check whether the constant of type tau and index i is present
2483 */
vtbl_find_const(value_table_t * table,type_t tau,int32_t id)2484 value_t vtbl_find_const(value_table_t *table, type_t tau, int32_t id) {
2485 const_hobj_t const_hobj;
2486
2487 assert(type_kind(table->type_table, tau) == SCALAR_TYPE ||
2488 type_kind(table->type_table, tau) == UNINTERPRETED_TYPE ||
2489 type_kind(table->type_table, tau) == INSTANCE_TYPE);
2490 assert(0 <= id);
2491
2492 const_hobj.m.hash = (hobj_hash_t) hash_const_value;
2493 const_hobj.m.eq = (hobj_eq_t) equal_const_value;
2494 const_hobj.m.build = (hobj_build_t) build_const_value;
2495 const_hobj.table = table;
2496 const_hobj.tau = tau;
2497 const_hobj.id = id;
2498
2499 return int_htbl_find_obj(&table->htbl, (int_hobj_t *) &const_hobj);
2500 }
2501
2502 /*
2503 * Check whether the tuple e[0] ... e[n-1] is present
2504 */
vtbl_find_tuple(value_table_t * table,uint32_t n,value_t * e)2505 value_t vtbl_find_tuple(value_table_t *table, uint32_t n, value_t *e) {
2506 tuple_hobj_t tuple_hobj;
2507
2508 tuple_hobj.m.hash = (hobj_hash_t) hash_tuple_value;
2509 tuple_hobj.m.eq = (hobj_eq_t) equal_tuple_value;
2510 tuple_hobj.m.build = (hobj_build_t) build_tuple_value;
2511 tuple_hobj.table = table;
2512 tuple_hobj.nelems = n;
2513 tuple_hobj.elem = e;
2514
2515 return int_htbl_find_obj(&table->htbl, (int_hobj_t *) &tuple_hobj);
2516 }
2517
2518 /*
2519 * Mapping object (a[0] ... a[n-1] |-> v)
2520 */
vtbl_find_map(value_table_t * table,uint32_t n,value_t * a,value_t v)2521 value_t vtbl_find_map(value_table_t *table, uint32_t n, value_t *a, value_t v) {
2522 map_hobj_t map_hobj;
2523
2524 map_hobj.m.hash = (hobj_hash_t) hash_map_value;
2525 map_hobj.m.eq = (hobj_eq_t) equal_map_value;
2526 map_hobj.m.build = (hobj_build_t) build_map_value;
2527 map_hobj.table = table;
2528 map_hobj.arity = n;
2529 map_hobj.arg = a;
2530 map_hobj.val = v;
2531
2532 return int_htbl_find_obj(&table->htbl, (int_hobj_t *) &map_hobj);
2533 }
2534
2535 /*
2536 * Function: defined by a[0 ... n-1] and the default value:
2537 * - same conventions as for vtbl_mk_function
2538 * - a is modified
2539 */
vtbl_find_function(value_table_t * table,type_t tau,uint32_t n,value_t * a,value_t def)2540 value_t vtbl_find_function(value_table_t *table, type_t tau, uint32_t n, value_t *a, value_t def) {
2541 fun_hobj_t fun_hobj;
2542
2543 assert(good_object(table, def));
2544
2545 // normalize a
2546 n = normalize_map_array(n, a);
2547 if (! object_is_unknown(table, def)) {
2548 n = remove_redundant_mappings(table, n, a, def);
2549 }
2550
2551 // if the function has finite domain and the default is something other than unknown
2552 // we may need more normalization
2553 if (type_has_finite_domain(table->type_table, tau) && !object_is_unknown(table, def)) {
2554 n = normalize_finite_domain_function(table, tau, n, a, &def);
2555 }
2556
2557 fun_hobj.m.hash = (hobj_hash_t) hash_fun_value;
2558 fun_hobj.m.eq = (hobj_eq_t) equal_fun_value;
2559 fun_hobj.m.build = (hobj_build_t) build_fun_value;
2560 fun_hobj.table = table;
2561 fun_hobj.type = tau;
2562 fun_hobj.arity = function_type_arity(table->type_table, tau);
2563 fun_hobj.def = def;
2564 fun_hobj.map_size = n;
2565 fun_hobj.map = a;
2566 fun_hobj.ambiguous = false;
2567
2568 return int_htbl_find_obj(&table->htbl, (int_hobj_t*) &fun_hobj);
2569 }
2570
2571
2572
2573 /**********************************
2574 * ENUMERATION OF FINITE TYPES *
2575 *********************************/
2576
2577 /*
2578 * Expand index i into an array of n indices a[0 ... n-1]
2579 * - where a[k] is an index for type tau[k]
2580 */
vtbl_expand_tuple_code(type_table_t * types,uint32_t n,type_t * tau,uint32_t i,uint32_t * a)2581 static void vtbl_expand_tuple_code(type_table_t *types, uint32_t n, type_t *tau, uint32_t i, uint32_t *a) {
2582 uint32_t j, q, c;
2583
2584 for (j=0; j<n; j++) {
2585 assert(is_finite_type(types, tau[j]));
2586 c = type_card(types, tau[j]);
2587 /*
2588 * i is c * q + r with 0 <= r < c
2589 * store r for a[j]
2590 */
2591 q = i / c;
2592 a[j] = i - c * q;
2593
2594 assert(a[j] < c);
2595 i = q;
2596 }
2597 }
2598
2599
2600 /*
2601 * Convert index i into a tuple of n objects of types tau[0] ... tau[n-1]
2602 * - store the result into a[0 ... n-1]
2603 */
vtbl_gen_object_tuple(value_table_t * table,uint32_t n,type_t * tau,uint32_t i,value_t * a)2604 void vtbl_gen_object_tuple(value_table_t *table, uint32_t n, type_t *tau, uint32_t i, value_t *a) {
2605 uint32_t j;
2606
2607 vtbl_expand_tuple_code(table->type_table, n, tau, i, (uint32_t *) a);
2608 for (j=0; j<n; j++) {
2609 a[j] = vtbl_gen_object(table, tau[j], (uint32_t ) a[j]);
2610 }
2611 }
2612
2613
2614 /*
2615 * Build object of a tuple type d and index i
2616 */
vtbl_gen_tuple(value_table_t * table,tuple_type_t * d,uint32_t i)2617 static value_t vtbl_gen_tuple(value_table_t *table, tuple_type_t *d, uint32_t i) {
2618 value_t buffer[10];
2619 value_t *aux;
2620 uint32_t n;
2621 value_t v;
2622
2623 n = d->nelem;
2624 aux = buffer;
2625 if (n > 10) {
2626 assert(n < UINT32_MAX/sizeof(value_t));
2627 aux = (value_t *) safe_malloc(n * sizeof(value_t));
2628 }
2629
2630 vtbl_gen_object_tuple(table, n, d->elem, i, aux);
2631 v = vtbl_mk_tuple(table, n, aux);
2632
2633 if (n > 10) {
2634 safe_free(aux);
2635 }
2636
2637 return v;
2638 }
2639
2640
2641 /*
2642 * Expand index i into an array of n indices a[0 ... n-1]
2643 * - each a[i] is an index between 0 and card(sigma) - 1
2644 */
vtbl_expand_function_code(type_table_t * types,uint32_t n,type_t sigma,uint32_t i,uint32_t * a)2645 static void vtbl_expand_function_code(type_table_t *types, uint32_t n, type_t sigma, uint32_t i, uint32_t *a) {
2646 uint32_t j, q, c;
2647
2648 assert(is_finite_type(types, sigma));
2649
2650 c = type_card(types, sigma);
2651 for (j=0; j<n; j++) {
2652 q = i / c;
2653 a[j] = i - c * q;
2654 assert(a[j] < c);
2655 i = q;
2656 }
2657 }
2658
2659
2660 /*
2661 * Construct the function of type tau defined by a[0 ... n-1]
2662 * - f = type descriptor for tau
2663 * - n = size of tau's domain
2664 * - every element of a is in tau's range
2665 */
vtbl_make_function_from_value_map(value_table_t * table,type_t tau,function_type_t * f,uint32_t n,value_t * a)2666 static value_t vtbl_make_function_from_value_map(value_table_t *table, type_t tau, function_type_t *f, uint32_t n, value_t *a) {
2667 value_t buffer[10];
2668 value_t buffer2[32];
2669 value_t *aux;
2670 value_t *map;
2671 ivector_t *v;
2672 uint32_t i, j, m, count;
2673 value_t k, def;
2674 fun_hobj_t fun_hobj;
2675
2676 assert(f == function_type_desc(table->type_table, tau));
2677
2678 // compute the default value
2679 v = &table->aux_vector;
2680 resize_ivector(v, n);
2681 for (i=0; i<n; i++) {
2682 v->data[i] = a[i];
2683 }
2684 int_array_sort(v->data, n);
2685 def = majority_element(v->data, n, &count);
2686 ivector_reset(v);
2687
2688 assert(count <= n);
2689
2690 if (count == n) {
2691 // special case: constant function
2692 k = vtbl_mk_function(table, tau, 0, NULL, def);
2693 } else {
2694
2695 // allocate array map of size (n - count) to store the map objects
2696 map = buffer2;
2697 if (n - count > 32) {
2698 assert(n - count < UINT32_MAX/sizeof(value_t));
2699 map = (value_t *) safe_malloc((n - count) * sizeof(value_t));
2700 }
2701
2702 m = f->ndom; // function arity
2703 aux = buffer;
2704 if (m > 10) {
2705 assert(m < UINT32_MAX/sizeof(value_t));
2706 aux = (value_t *) safe_malloc(m * sizeof(value_t));
2707 }
2708
2709 // build the map objects: add them to array map
2710 // we skip all map objects whose value is def
2711 j = 0;
2712 for (i=0; i<n; i++) {
2713 if (a[i] != def) {
2714 vtbl_gen_object_tuple(table, m, f->domain, i, aux);
2715 k = vtbl_mk_map(table, m, aux, a[i]);
2716 map[j] = k;
2717 j ++;
2718 }
2719 }
2720
2721 assert(j == n - count);
2722
2723 // no need to remove duplicate etc. so we just sort and
2724 // call the hash-consing constructor
2725 int_array_sort(map, j);
2726
2727 fun_hobj.m.hash = (hobj_hash_t) hash_fun_value;
2728 fun_hobj.m.eq = (hobj_eq_t) equal_fun_value;
2729 fun_hobj.m.build = (hobj_build_t) build_fun_value;
2730 fun_hobj.table = table;
2731 fun_hobj.type = tau;
2732 fun_hobj.arity = m;
2733 fun_hobj.def = def;
2734 fun_hobj.map_size = j;
2735 fun_hobj.map = map;
2736 fun_hobj.ambiguous = false;
2737
2738 k = int_htbl_get_obj(&table->htbl, (int_hobj_t*) &fun_hobj);
2739
2740 // cleanup
2741 if (m > 10) {
2742 safe_free(aux);
2743 }
2744 if (n - count > 32) {
2745 safe_free(map);
2746 }
2747 }
2748
2749 return k;
2750 }
2751
2752
2753 /*
2754 * Function of type tau and index i
2755 * - tau is finite and i < card(tau)
2756 */
vtbl_gen_function(value_table_t * table,type_t tau,uint32_t i)2757 static value_t vtbl_gen_function(value_table_t *table, type_t tau, uint32_t i) {
2758 uint32_t buffer[32];
2759 uint32_t *aux;
2760 type_table_t *types;
2761 function_type_t *f;
2762 uint32_t j, n;
2763 value_t v;
2764
2765 types = table->type_table;
2766 f = function_type_desc(types, tau);
2767
2768 if (is_unit_type(types, tau)) {
2769 // build the constant function for that type
2770 assert(i == 0 && is_unit_type(types, f->range));
2771 v = vtbl_gen_object(table, f->range, 0);
2772 v = vtbl_mk_function(table, tau, 0, NULL, v);
2773 } else {
2774 n = card_of_domain_type(types, tau);
2775 aux = buffer;
2776 if (n > 32) {
2777 assert(n < UINT32_MAX/sizeof(uint32_t));
2778 aux = (uint32_t *) safe_malloc(n * sizeof(uint32_t));
2779 }
2780
2781 vtbl_expand_function_code(types, n, f->range, i, aux);
2782 for (j=0; j<n; j++) {
2783 aux[j] = vtbl_gen_object(table, f->range, aux[j]);
2784 }
2785 v = vtbl_make_function_from_value_map(table, tau, f, n, (value_t *) aux);
2786
2787 if (n > 32) {
2788 safe_free(aux);
2789 }
2790 }
2791
2792 return v;
2793 }
2794
2795
2796 /*
2797 * Bitvector: index i, size n
2798 */
vtbl_gen_bitvector(value_table_t * table,uint32_t n,uint32_t i)2799 static value_t vtbl_gen_bitvector(value_table_t *table, uint32_t n, uint32_t i) {
2800 bvconstant_t *b;
2801
2802 b = &table->buffer;
2803 bvconstant_copy64(b, n, (uint64_t) i);
2804 return vtbl_mk_bv_from_constant(table, b);
2805 }
2806
2807
2808 /*
2809 * If tau is a finite type, then we can enumerate its elements from
2810 * 0 to card(tau) - 1. The following function constructs an element
2811 * of finite type tau given an enumeration index i.
2812 * - tau must be finite
2813 * - i must be smaller than card(tau)
2814 */
vtbl_gen_object(value_table_t * table,type_t tau,uint32_t i)2815 value_t vtbl_gen_object(value_table_t *table, type_t tau, uint32_t i) {
2816 type_table_t *types;
2817 value_t v;
2818
2819 types = table->type_table;
2820 assert(is_finite_type(types, tau) && i < type_card(types, tau));
2821
2822 switch (type_kind(types, tau)) {
2823 case BOOL_TYPE:
2824 assert(i == 0 || i == 1);
2825 v = vtbl_mk_bool(table, i);
2826 break;
2827
2828 case BITVECTOR_TYPE:
2829 v = vtbl_gen_bitvector(table, bv_type_size(types, tau), i);
2830 break;
2831
2832 case SCALAR_TYPE:
2833 v = vtbl_mk_const(table, tau, i, NULL); // anonymous constant
2834 break;
2835
2836 case TUPLE_TYPE:
2837 v = vtbl_gen_tuple(table, tuple_type_desc(types, tau), i);
2838 break;
2839
2840 case FUNCTION_TYPE:
2841 v = vtbl_gen_function(table, tau, i);
2842 break;
2843
2844 default:
2845 assert(false); // can't be a finite type
2846 v = null_value;
2847 break;
2848 }
2849
2850 return v;
2851 }
2852
2853
2854 /*
2855 * Convert function index i for type tau into an array of n objects
2856 * - n = size of tau's domain
2857 */
vtbl_gen_function_map(value_table_t * table,type_t tau,uint32_t i,value_t * a)2858 void vtbl_gen_function_map(value_table_t *table, type_t tau, uint32_t i, value_t *a) {
2859 uint32_t buffer[32];
2860 uint32_t *aux;
2861 uint32_t j, n;
2862 type_t sigma;
2863
2864 assert(type_has_finite_domain(table->type_table, tau));
2865
2866 n = card_of_domain_type(table->type_table, tau);
2867 aux = buffer;
2868 if (n > 32) {
2869 assert(n < UINT32_MAX/sizeof(uint32_t));
2870 aux = (uint32_t *) safe_malloc(n * sizeof(uint32_t));
2871 }
2872
2873 sigma = function_type_range(table->type_table, tau);
2874 vtbl_expand_function_code(table->type_table, n, sigma, i, aux);
2875 for (j=0; j<n; j++) {
2876 a[j] = vtbl_gen_object(table, sigma, aux[j]);
2877 }
2878
2879 if (n > 32) {
2880 safe_free(aux);
2881 }
2882 }
2883
2884
2885 /*
2886 * TEST EXISTENCE OF OBJECTS USING THEIR INDEX
2887 */
2888
2889 /*
2890 * Search for object tuple of index i and type tau[0] x ... x tau[n-1]
2891 * - return null_value if it's not present
2892 */
vtbl_find_object_tuple(value_table_t * table,uint32_t n,type_t * tau,uint32_t i)2893 value_t vtbl_find_object_tuple(value_table_t *table, uint32_t n, type_t *tau, uint32_t i) {
2894 uint32_t buffer[10];
2895 uint32_t *aux;
2896 uint32_t j;
2897 value_t v;
2898
2899 aux = buffer;
2900 if (n > 10) {
2901 assert(n < UINT32_MAX/sizeof(uint32_t));
2902 aux = (uint32_t *) safe_malloc(n * sizeof(uint32_t));
2903 }
2904
2905 vtbl_expand_tuple_code(table->type_table, n, tau, i, aux);
2906
2907 for (j=0; j<n; j++) {
2908 v = vtbl_find_object(table, tau[j], aux[j]);
2909 if (v == null_value) goto cleanup;
2910 aux[j] = v;
2911 }
2912
2913 // all elements aux[0 ... n-1] exist
2914 v = vtbl_find_tuple(table, n, (value_t *) aux);
2915
2916 cleanup:
2917 if (n > 10) {
2918 safe_free(aux);
2919 }
2920
2921 return v;
2922 }
2923
2924
2925 /*
2926 * Search for object of index i and tuple type d
2927 */
vtbl_find_enum_tuple(value_table_t * table,tuple_type_t * d,uint32_t i)2928 static inline value_t vtbl_find_enum_tuple(value_table_t *table, tuple_type_t *d, uint32_t i) {
2929 return vtbl_find_object_tuple(table, d->nelem, d->elem, i);
2930 }
2931
2932
2933 /*
2934 * Search for the map object defined by codes a[0 ... n-1] and value v
2935 * - a[i] is a code for type tau[i]
2936 * - v is good value
2937 * - a is modified
2938 */
vtbl_find_enum_map(value_table_t * table,uint32_t n,type_t * tau,uint32_t * a,value_t v)2939 static value_t vtbl_find_enum_map(value_table_t *table, uint32_t n, type_t *tau, uint32_t *a, value_t v) {
2940 uint32_t i;
2941 value_t k;
2942
2943 for (i=0; i<n; i++) {
2944 k = vtbl_find_object(table, tau[i], a[i]);
2945 if (k == null_value) goto done;
2946 a[i] = k;
2947 }
2948
2949 k = vtbl_find_map(table, n, (value_t *) a, v);
2950
2951 done:
2952 return k;
2953 }
2954
2955
2956 /*
2957 * Function of type tau, defined by the array a[0 ... n-1]
2958 * - f = type descriptor for tau
2959 * - n = size of tau's domain
2960 * - every a[i] is in tau's range
2961 */
vtbl_find_function_with_value_map(value_table_t * table,type_t tau,function_type_t * f,uint32_t n,value_t * a)2962 static value_t vtbl_find_function_with_value_map(value_table_t *table, type_t tau, function_type_t *f, uint32_t n, value_t *a) {
2963 uint32_t buffer[10];
2964 value_t buffer2[32];
2965 uint32_t *aux;
2966 value_t *map;
2967 ivector_t *v;
2968 uint32_t i, j, m, count;
2969 value_t k, def;
2970 fun_hobj_t fun_hobj;
2971
2972 assert(f == function_type_desc(table->type_table, tau));
2973
2974 // compute the default value
2975 v = &table->aux_vector;
2976 resize_ivector(v, n);
2977 for (i=0; i<n; i++) {
2978 v->data[i] = a[i];
2979 }
2980 int_array_sort(v->data, n);
2981 def = majority_element(v->data, n, &count);
2982 ivector_reset(v);
2983
2984 assert(count <= n);
2985
2986 if (count == 0) {
2987 // special case: constant function
2988 k = vtbl_find_function(table, tau, 0, NULL, def);
2989 } else {
2990 // allocate array map of size (n - count) to store the map objects
2991 map = buffer2;
2992 if (n - count > 32) {
2993 assert(n - count < UINT32_MAX/sizeof(value_t));
2994 map = (value_t *) safe_malloc((n - count) * sizeof(value_t));
2995 }
2996
2997 m = f->ndom; // function arity
2998 aux = buffer;
2999 if (m > 10) {
3000 assert(m < UINT32_MAX/sizeof(uint32_t));
3001 aux = (uint32_t *) safe_malloc(m * sizeof(uint32_t));
3002 }
3003
3004 // search for the map objects and add them to array map
3005 j = 0;
3006 for (i=0; i<n; i++) {
3007 if (a[i] != def) {
3008 vtbl_expand_tuple_code(table->type_table, m, f->domain, i, aux);
3009 k = vtbl_find_enum_map(table, m, f->domain, aux, a[i]);
3010 if (k == null_value) {
3011 goto cleanup;
3012 }
3013 map[j] = k;
3014 j ++;
3015 }
3016 }
3017
3018 assert(j == n - count);
3019
3020 // no need to remove duplicate etc
3021 int_array_sort(map, j);
3022
3023 fun_hobj.m.hash = (hobj_hash_t) hash_fun_value;
3024 fun_hobj.m.eq = (hobj_eq_t) equal_fun_value;
3025 fun_hobj.m.build = (hobj_build_t) build_fun_value;
3026 fun_hobj.table = table;
3027 fun_hobj.type = tau;
3028 fun_hobj.arity = m;
3029 fun_hobj.def = def;
3030 fun_hobj.map_size = j;
3031 fun_hobj.map = map;
3032 fun_hobj.ambiguous = false;
3033
3034 k = int_htbl_find_obj(&table->htbl, (int_hobj_t*) &fun_hobj);
3035
3036 cleanup:
3037 if (m > 10) {
3038 safe_free(aux);
3039 }
3040 if (n - count > 32) {
3041 safe_free(map);
3042 }
3043 }
3044
3045 return k;
3046 }
3047
3048 /*
3049 * Function of type tau and index i
3050 * - tau must be finite and i must be smaller than card(tau)
3051 */
vtbl_find_enum_function(value_table_t * table,type_t tau,uint32_t i)3052 static value_t vtbl_find_enum_function(value_table_t *table, type_t tau, uint32_t i) {
3053 uint32_t buffer[32];
3054 uint32_t *aux;
3055 type_table_t *types;
3056 function_type_t *f;
3057 uint32_t j, n;
3058 value_t v;
3059
3060 types = table->type_table;
3061 f = function_type_desc(types, tau);
3062
3063 if (is_unit_type(types, tau)) {
3064 // only element is the constant function of type tau
3065 assert(i == 0 && is_unit_type(types, f->range));
3066 v = vtbl_find_object(table, f->range, 0);
3067 if (v != null_value) {
3068 v = vtbl_find_function(table, tau, 0, NULL, v);
3069 }
3070 } else {
3071 n = card_of_domain_type(types, tau);
3072 aux = buffer;
3073 if (n > 32) {
3074 assert(n < UINT32_MAX/sizeof(uint32_t));
3075 aux = (uint32_t *) safe_malloc(n * sizeof(uint32_t));
3076 }
3077
3078 vtbl_expand_function_code(types, n, f->range, i, aux);
3079 for (j=0; j<n; j++) {
3080 v = vtbl_find_object(table, f->range, aux[j]);
3081 if (v == null_value) {
3082 goto cleanup;
3083 }
3084 aux[j] = v;
3085 }
3086
3087 // n good elements are in aux[0 ... n-1]
3088 v = vtbl_find_function_with_value_map(table, tau, f, n, (value_t *) aux);
3089
3090 cleanup:
3091 if (n > 32) {
3092 safe_free(aux);
3093 }
3094 }
3095
3096 return v;
3097 }
3098
3099 /*
3100 * Check whether object of type tau and index i is present in table.
3101 * - tau must be finite
3102 * - i must be smaller than card(tau)
3103 * - return the object of index i if present, null_value otherwise
3104 */
vtbl_find_object(value_table_t * table,type_t tau,uint32_t i)3105 value_t vtbl_find_object(value_table_t *table, type_t tau, uint32_t i) {
3106 type_table_t *types;
3107
3108 types = table->type_table;
3109 assert(is_finite_type(types, tau) && i < type_card(types, tau));
3110
3111 switch (type_kind(types, tau)) {
3112 case BOOL_TYPE:
3113 assert(i == 0 || i == 1);
3114 return vtbl_mk_bool(table, i);
3115
3116 case BITVECTOR_TYPE:
3117 return vtbl_find_bv64(table, bv_type_size(types, tau), (uint64_t) i);
3118
3119 case SCALAR_TYPE:
3120 return vtbl_find_const(table, tau, i);
3121
3122 case TUPLE_TYPE:
3123 return vtbl_find_enum_tuple(table, tuple_type_desc(types, tau), i);
3124
3125 case FUNCTION_TYPE:
3126 return vtbl_find_enum_function(table, tau, i);
3127
3128 default:
3129 // tau can't be a finite type
3130 assert(false);
3131 return null_value;
3132 }
3133 }
3134
3135
3136
3137
3138 /*****************************
3139 * FUNCTION/CONSTANT NAMES *
3140 ****************************/
3141
3142 /*
3143 * Set the name of a function f (make a copy and overwrite the current name)
3144 */
vtbl_set_function_name(value_table_t * table,value_t f,char * name)3145 void vtbl_set_function_name(value_table_t *table, value_t f, char *name) {
3146 value_fun_t *fun;
3147
3148 assert(table->kind[f] == FUNCTION_VALUE);
3149 fun = table->desc[f].ptr;
3150 if (fun->name != NULL) {
3151 safe_free(fun->name);
3152 fun->name = NULL;
3153 }
3154 if (name != NULL) {
3155 fun->name = (char *) safe_malloc(strlen(name) + 1);
3156 strcpy(fun->name, name);
3157 }
3158 }
3159
3160
3161 /*
3162 * Set the name of an uninterpreted constant c
3163 */
vtbl_set_constant_name(value_table_t * table,value_t c,char * name)3164 void vtbl_set_constant_name(value_table_t *table, value_t c, char *name) {
3165 value_unint_t *d;
3166
3167 assert(table->kind[c] == UNINTERPRETED_VALUE);
3168 d = table->desc[c].ptr;
3169 if (d->name != NULL) {
3170 safe_free(d->name);
3171 d->name = NULL;
3172 }
3173 if (name != NULL) {
3174 d->name = (char *) safe_malloc(strlen(name) + 1);
3175 strcpy(d->name, name);
3176 }
3177 }
3178
3179
3180
3181
3182
3183 /***********************
3184 * TEMPORARY OBJECTS *
3185 **********************/
3186
3187 /*
3188 * Mark all current objects as permanent.
3189 * All objects created after this function is called are temporary
3190 * and can be deleted by calling 'value_table_delete_tmp'.
3191 */
value_table_start_tmp(value_table_t * table)3192 void value_table_start_tmp(value_table_t *table) {
3193 assert(table->first_tmp == -1);
3194 // make sure unknown, true, and false are constructed
3195 (void) vtbl_mk_unknown(table);
3196 (void) vtbl_mk_true(table);
3197 (void) vtbl_mk_false(table);
3198
3199 // set the tmp mark
3200 table->first_tmp = table->nobjects;
3201 }
3202
3203
3204
3205 /*
3206 * Delete all temporary objects.
3207 * They are stored at indices [first_tmp ... nobjects-1].
3208 * Do nothing if first_tmp is -1.
3209 * Reset first_tmp to -1.
3210 */
value_table_end_tmp(value_table_t * table)3211 void value_table_end_tmp(value_table_t *table) {
3212 if (table->first_tmp >= 0) {
3213 vtbl_delete_descriptors(table, table->first_tmp);
3214 table->first_tmp = -1;
3215 }
3216 }
3217
3218
3219
3220 /********************
3221 * SPECIAL VALUES *
3222 *******************/
3223
3224 /*
3225 * Check whether v is zero:
3226 * - v must be a good object
3227 * - return true if v is a rational equal to zero
3228 */
is_zero(value_table_t * table,value_t v)3229 bool is_zero(value_table_t *table, value_t v) {
3230 assert(good_object(table, v));
3231 return object_is_rational(table, v) && q_is_zero(vtbl_rational(table, v));
3232 }
3233
3234 /*
3235 * Check whether v is one
3236 * - v must be a good object
3237 * - return true if v is a rational equal to 1
3238 */
is_one(value_table_t * table,value_t v)3239 bool is_one(value_table_t *table, value_t v) {
3240 assert(good_object(table, v));
3241 return object_is_rational(table, v) && q_is_one(vtbl_rational(table, v));
3242 }
3243
3244
3245 /*
3246 * Check whether v is +1 or -1
3247 * - v must be a good object
3248 */
is_unit(value_table_t * table,value_t v)3249 bool is_unit(value_table_t *table, value_t v) {
3250 rational_t *r;
3251
3252 assert(good_object(table, v));
3253 if (object_is_rational(table, v)) {
3254 r = vtbl_rational(table, v);
3255 return q_is_one(r) || q_is_minus_one(r);
3256 }
3257
3258 return false;
3259 }
3260
3261
3262 /*
3263 * Check whether v is 0b00000...
3264 * - v must be a good object
3265 * - return true if v is a bitvector constant of the form 0b0....0
3266 */
is_bvzero(value_table_t * table,value_t v)3267 bool is_bvzero(value_table_t *table, value_t v) {
3268 value_bv_t *b;
3269
3270 assert(good_object(table, v));
3271 if (object_is_bitvector(table, v)) {
3272 b = vtbl_bitvector(table, v);
3273 assert(bvconst_is_normalized(b->data, b->nbits));
3274 return bvconst_is_zero(b->data, b->width);
3275 }
3276
3277 return false;
3278 }
3279
3280
3281
3282
3283
3284
3285 /****************
3286 * EVALUATION *
3287 ***************/
3288
3289 /*
3290 * Check whether every element in the domain and range of f
3291 * is canonical.
3292 * - f must be a function
3293 */
semi_canonical(value_table_t * table,value_t f)3294 static bool semi_canonical(value_table_t *table, value_t f) {
3295 value_fun_t *fun;
3296
3297 fun = vtbl_function(table, f);
3298 return object_is_canonical(table, fun->def) && canonical_array(table, fun->map, fun->map_size);
3299 }
3300
3301
3302 /*
3303 * Check whether the functions f1 and f2 are equal
3304 * - the maps and default values for both must be canonical
3305 */
vtbl_eval_eq_functions(value_table_t * table,value_t f1,value_t f2)3306 static value_t vtbl_eval_eq_functions(value_table_t *table, value_t f1, value_t f2) {
3307 value_fun_t *d1, *d2;
3308 value_map_t *m;
3309 value_t v;
3310 uint32_t arity, n, i, k;
3311
3312 assert(semi_canonical(table, f1) && semi_canonical(table, f2) && f1 != f2);
3313
3314 d1 = vtbl_function(table, f1);
3315 d2 = vtbl_function(table, f2);
3316 if (d1->def == d2->def) goto not_equal; // f1 and f2 have the same default but different maps
3317
3318 arity = d1->arity;
3319 assert(d2->arity == arity);
3320
3321 n = d1->map_size;
3322 for (i=0; i<n; i++) {
3323 m = vtbl_map(table, d1->map[i]);
3324 v = hash_eval_app(table, f2, arity, m->arg);
3325 if (v == null_value) v = d2->def;
3326 /*
3327 * f1 maps m->arg[0 ... arity-1] to m->val
3328 * f2 maps m->arg[0 ... arity-1] to v
3329 * both m->value and v are canonical
3330 */
3331 assert(object_is_canonical(table, v) &&
3332 object_is_canonical(table, m->val));
3333 if (v != m->val) goto not_equal;
3334 }
3335
3336 /*
3337 * k = number of elements in the domain
3338 * where f1 and f2 agree.
3339 */
3340 k = n;
3341 n = d2->map_size;
3342 for (i=0; i<n; i++) {
3343 m = vtbl_map(table, d2->map[i]);
3344 v = hash_eval_app(table, f1, arity, m->arg);
3345 if (v == null_value) {
3346 k ++; // element in f2's map that's not in f1's map
3347 v = d1->def;
3348 }
3349 assert(object_is_canonical(table, v) &&
3350 object_is_canonical(table, m->val));
3351 if (v != m->val) goto not_equal;
3352 }
3353
3354 /*
3355 * The maps of f1 and f2 are equal, the default values are
3356 * distinct. If we can find a tuple in the domain of f1 and f2
3357 * that's not in map of f1 nor in map of f2, then f1 and f2 are
3358 * distinct.
3359 */
3360 if (type_has_finite_domain(table->type_table, d1->type) &&
3361 k == card_of_domain_type(table->type_table, d1->type)) {
3362 // f1 and f2 agree on all elements in their domain
3363 return vtbl_mk_true(table);
3364 }
3365
3366 not_equal:
3367 return vtbl_mk_false(table);
3368 }
3369
3370
3371 /*
3372 * Evaluate (eq a b)
3373 *
3374 * TODO: improve this. We could do much more when checking equality
3375 * between two functions.
3376 */
vtbl_eval_eq(value_table_t * table,value_t a,value_t b)3377 value_t vtbl_eval_eq(value_table_t *table, value_t a, value_t b) {
3378 value_t v;
3379
3380 assert(good_object(table, a) && good_object(table, b));
3381
3382 if (a == b) {
3383 v = vtbl_mk_true(table);
3384 } else if (object_is_canonical(table, a) || object_is_canonical(table, b)) {
3385 v = vtbl_mk_false(table);
3386 } else {
3387 /*
3388 * a and b are non canonical
3389 */
3390 if (object_is_function(table, a) && object_is_function(table, b) &&
3391 semi_canonical(table, a) && semi_canonical(table, b)) {
3392 v = vtbl_eval_eq_functions(table, a, b);
3393 } else {
3394 v = vtbl_mk_unknown(table);
3395 }
3396 }
3397
3398 return v;
3399 }
3400
3401
3402 /*
3403 * Check whether arrays a[0 ... n-1] and b[0 ... n-1] are equal
3404 * - return unknown if we can't tell
3405 */
vtbl_eval_array_eq(value_table_t * table,value_t * a,value_t * b,uint32_t n)3406 value_t vtbl_eval_array_eq(value_table_t *table, value_t *a, value_t *b, uint32_t n) {
3407 uint32_t i;
3408 value_t v;
3409
3410 for (i=0; i<n; i++) {
3411 assert(good_object(table, a[i]) && good_object(table, b[i]));
3412
3413 if (a[i] != b[i]) {
3414 v = vtbl_eval_eq(table, a[i], b[i]);
3415 if (v == vtbl_mk_false(table) || v == vtbl_mk_unknown(table)) {
3416 return v;
3417 }
3418 assert(v == vtbl_mk_true(table));
3419 }
3420 }
3421
3422 return vtbl_mk_true(table);
3423 }
3424
3425
3426
3427 /*
3428 * Evaluate (f a[0] ... a[n-1])
3429 * - f must be a function or update object of arity n
3430 * - a[0] ... a[n-1] must be non-null values
3431 * Return unknown if the map is not defined for a[0 ... n-1]
3432 */
vtbl_eval_application(value_table_t * table,value_t f,uint32_t n,value_t * a)3433 value_t vtbl_eval_application(value_table_t *table, value_t f, uint32_t n, value_t *a) {
3434 value_update_t *u;
3435 value_t j;
3436
3437 // unroll all updates
3438 while (object_is_update(table, f)) {
3439 u = table->desc[f].ptr;
3440 assert(u->arity == n);
3441 j = u->map;
3442 if (mapping_matches_array(table, j, n, a)) {
3443 return vtbl_map_result(table, j);
3444 }
3445 f = u->fun;
3446 }
3447
3448 assert(object_is_function(table, f) && vtbl_function(table, f)->arity == n);
3449
3450 // search for (f a[0] ... a[n-1]) in the mtbl
3451 j = hash_eval_app(table, f, n, a);
3452 if (j == null_value) {
3453 if (canonical_array(table, a, n)) {
3454 // use the default value for f
3455 j = vtbl_function(table, f)->def;
3456 } else {
3457 // can't tell for sure so we return unknown
3458 j = vtbl_mk_unknown(table);
3459 }
3460 }
3461
3462 return j;
3463 }
3464
3465
3466 /*
3467 * Evaluate (/ v 0) by a lookup in table->zero_rdiv_dun
3468 * - v should be an arithmetic object (but we don't check)
3469 * - return unknown if either zero_rdiv_fun is null or if the mapping of v is not defined.
3470 */
vtbl_eval_rdiv_by_zero(value_table_t * table,value_t v)3471 value_t vtbl_eval_rdiv_by_zero(value_table_t *table, value_t v) {
3472 value_t f, r;
3473
3474 f = table->zero_rdiv_fun;
3475 if (f != null_value) {
3476 r = vtbl_eval_application(table, f, 1, &v);
3477 } else {
3478 r = vtbl_mk_unknown(table);
3479 }
3480 return r;
3481 }
3482
3483
3484 /*
3485 * Same thing for integer division: use table->zero_idiv_fun
3486 */
vtbl_eval_idiv_by_zero(value_table_t * table,value_t v)3487 value_t vtbl_eval_idiv_by_zero(value_table_t *table, value_t v) {
3488 value_t f, r;
3489
3490 f = table->zero_idiv_fun;
3491 if (f != null_value) {
3492 r = vtbl_eval_application(table, f, 1, &v);
3493 } else {
3494 r = vtbl_mk_unknown(table);
3495 }
3496 return r;
3497 }
3498
3499 /*
3500 * Same thing for modulo: use table->zero_mod_fun
3501 */
vtbl_eval_mod_by_zero(value_table_t * table,value_t v)3502 value_t vtbl_eval_mod_by_zero(value_table_t *table, value_t v) {
3503 value_t f, r;
3504
3505 f = table->zero_mod_fun;
3506 if (f != null_value) {
3507 r = vtbl_eval_application(table, f, 1, &v);
3508 } else {
3509 r = vtbl_mk_unknown(table);
3510 }
3511 return r;
3512 }
3513
3514
3515
3516
3517
3518 /*
3519 * ACCESS TO THE QUEUE
3520 */
3521
3522 /*
3523 * Push v into the internal queue
3524 * - v must be a valid object
3525 * - do nothing if v is already in the queue
3526 */
vtbl_push_object(value_table_t * table,value_t v)3527 void vtbl_push_object(value_table_t *table, value_t v) {
3528 assert(good_object(table, v));
3529 vtbl_queue_push(&table->queue, v);
3530 }
3531
3532 /*
3533 * Empty the internal queue
3534 */
vtbl_empty_queue(value_table_t * table)3535 void vtbl_empty_queue(value_table_t *table) {
3536 reset_vtbl_queue(&table->queue);
3537 }
3538
3539 /*
3540 * Check emptiness
3541 */
vtbl_queue_is_empty(value_table_t * table)3542 bool vtbl_queue_is_empty(value_table_t *table) {
3543 return int_queue_is_empty(&table->queue.queue);
3544 }
3545