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 * Operations on composite objects
21 */
22 #include <stddef.h>
23
24 #include "solvers/egraph/composites.h"
25 #include "utils/int_array_sort.h"
26 #include "utils/memalloc.h"
27
28
29
30 /******************
31 * CONSTRUCTORS *
32 *****************/
33
34 /*
35 * Allocate a new composite: n = arity
36 * - this allocates a child array of size 2n
37 */
alloc_composite(uint32_t n)38 static inline composite_t *alloc_composite(uint32_t n) {
39 assert(n <= MAX_COMPOSITE_ARITY);
40 n += n;
41 return (composite_t *) safe_malloc(sizeof(composite_t) + n * sizeof(int32_t));
42 }
43
arena_alloc_composite(arena_t * m,uint32_t n)44 static inline composite_t *arena_alloc_composite(arena_t *m, uint32_t n) {
45 assert(n <= MAX_COMPOSITE_ARITY);
46 n += n;
47 return (composite_t *) arena_alloc(m, sizeof(composite_t) + n * sizeof(int32_t));
48 }
49
alloc_lambda_composite(void)50 static inline composite_t *alloc_lambda_composite(void) {
51 return (composite_t *) safe_malloc(sizeof(composite_t) + 3 * sizeof(int32_t));
52 }
53
arena_alloc_lambda_composite(arena_t * m)54 static inline composite_t *arena_alloc_lambda_composite(arena_t *m) {
55 return (composite_t *) arena_alloc(m, sizeof(composite_t) + 3 * sizeof(int32_t));
56 }
57
58
59 /*
60 * Initialization
61 */
init_header(composite_t * c,uint32_t tg)62 static inline void init_header(composite_t *c, uint32_t tg) {
63 c->tag = tg;
64 c->hash = 0;
65 c->id = null_eterm;
66 }
67
init_hooks(composite_t * c)68 static void init_hooks(composite_t *c) {
69 uint32_t i, n;
70 int32_t *h;
71
72 n = composite_arity(c);
73 h = c->child + n;
74 for (i=0; i<n; i++) {
75 h[i] = no_ptr;
76 }
77 }
78
init_apply(composite_t * c,occ_t f,uint32_t n,occ_t * a)79 static void init_apply(composite_t *c, occ_t f, uint32_t n, occ_t *a) {
80 uint32_t i;
81
82 assert(n >= 1);
83
84 init_header(c, mk_apply_tag(n + 1));
85 c->child[0] = f;
86 for (i=0; i<n; i++) {
87 c->child[i+1] = a[i];
88 }
89 init_hooks(c);
90 }
91
init_update(composite_t * c,occ_t f,uint32_t n,occ_t * a,occ_t v)92 static void init_update(composite_t *c, occ_t f, uint32_t n, occ_t *a, occ_t v) {
93 uint32_t i;
94
95 assert(n >= 1);
96 init_header(c, mk_update_tag(n + 2));
97 c->child[0] = f;
98 for (i=0; i<n; i++) {
99 c->child[i+1] = a[i];
100 }
101 c->child[n+1] = v;
102 init_hooks(c);
103 }
104
init_tuple(composite_t * c,uint32_t n,occ_t * a)105 static void init_tuple(composite_t *c, uint32_t n, occ_t *a) {
106 uint32_t i;
107
108 assert(n >= 1);
109
110 init_header(c, mk_tuple_tag(n));
111 for (i=0; i<n; i++) {
112 c->child[i] = a[i];
113 }
114 init_hooks(c);
115 }
116
init_eq(composite_t * c,occ_t t1,occ_t t2)117 static void init_eq(composite_t *c, occ_t t1, occ_t t2) {
118 init_header(c, mk_eq_tag());
119 c->child[0] = t1;
120 c->child[1] = t2;
121 init_hooks(c);
122 }
123
init_distinct(composite_t * c,uint32_t n,occ_t * a)124 static void init_distinct(composite_t *c, uint32_t n, occ_t *a) {
125 uint32_t i;
126
127 assert(n >= 2); // ? 3 is a better limit
128
129 init_header(c, mk_distinct_tag(n));
130 for (i=0; i<n; i++) {
131 c->child[i] = a[i];
132 }
133 init_hooks(c);
134 }
135
init_ite(composite_t * c,occ_t t1,occ_t t2,occ_t t3)136 static void init_ite(composite_t *c, occ_t t1, occ_t t2, occ_t t3) {
137 init_header(c, mk_ite_tag());
138 c->child[0] = t1;
139 c->child[1] = t2;
140 c->child[2] = t3;
141 init_hooks(c);
142 }
143
init_or(composite_t * c,uint32_t n,occ_t * a)144 static void init_or(composite_t *c, uint32_t n, occ_t *a) {
145 uint32_t i;
146
147 assert(n >= 2);
148
149 init_header(c, mk_or_tag(n));
150 for (i=0; i<n; i++) {
151 c->child[i] = a[i];
152 }
153 init_hooks(c);
154 }
155
init_lambda(composite_t * c,occ_t t,int32_t tag)156 static void init_lambda(composite_t *c, occ_t t, int32_t tag) {
157 init_header(c, mk_lambda_tag());
158 c->child[0] = t;
159 c->child[1] = no_ptr; // hook
160 c->child[2] = tag;
161 }
162
163
164 /*
165 * Long-term composites
166 */
new_apply_composite(occ_t f,uint32_t n,occ_t * a)167 composite_t *new_apply_composite(occ_t f, uint32_t n, occ_t *a) {
168 composite_t *tmp;
169
170 tmp = alloc_composite(n + 1);
171 init_apply(tmp, f, n, a);
172 return tmp;
173 }
174
new_update_composite(occ_t f,uint32_t n,occ_t * a,occ_t v)175 composite_t *new_update_composite(occ_t f, uint32_t n, occ_t *a, occ_t v) {
176 composite_t *tmp;
177
178 tmp = alloc_composite(n + 2);
179 init_update(tmp, f, n, a, v);
180 return tmp;
181 }
182
new_tuple_composite(uint32_t n,occ_t * a)183 composite_t *new_tuple_composite(uint32_t n, occ_t *a) {
184 composite_t *tmp;
185
186 tmp = alloc_composite(n);
187 init_tuple(tmp, n, a);
188 return tmp;
189 }
190
new_eq_composite(occ_t t1,occ_t t2)191 composite_t *new_eq_composite(occ_t t1, occ_t t2) {
192 composite_t *tmp;
193
194 tmp = alloc_composite(2);
195 init_eq(tmp, t1, t2);
196 return tmp;
197 }
198
new_distinct_composite(uint32_t n,occ_t * a)199 composite_t *new_distinct_composite(uint32_t n, occ_t *a) {
200 composite_t *tmp;
201
202 tmp = alloc_composite(n);
203 init_distinct(tmp, n, a);
204 return tmp;
205 }
206
new_ite_composite(occ_t t1,occ_t t2,occ_t t3)207 composite_t *new_ite_composite(occ_t t1, occ_t t2, occ_t t3) {
208 composite_t *tmp;
209
210 tmp = alloc_composite(3);
211 init_ite(tmp, t1, t2, t3);
212 return tmp;
213 }
214
new_or_composite(uint32_t n,occ_t * a)215 composite_t *new_or_composite(uint32_t n, occ_t *a) {
216 composite_t *tmp;
217
218 tmp = alloc_composite(n);
219 init_or(tmp, n, a);
220 return tmp;
221 }
222
new_lambda_composite(occ_t t,int32_t tag)223 composite_t *new_lambda_composite(occ_t t, int32_t tag) {
224 composite_t *tmp;
225
226 tmp = alloc_lambda_composite();
227 init_lambda(tmp, t, tag);
228 return tmp;
229 }
230
231
232 /*
233 * Composites allocated in arena m
234 */
arena_apply_composite(arena_t * m,occ_t f,uint32_t n,occ_t * a)235 composite_t *arena_apply_composite(arena_t *m, occ_t f, uint32_t n, occ_t *a) {
236 composite_t *tmp;
237
238 tmp = arena_alloc_composite(m, n + 1);
239 init_apply(tmp, f, n, a);
240 return tmp;
241 }
242
arena_update_composite(arena_t * m,occ_t f,uint32_t n,occ_t * a,occ_t v)243 composite_t *arena_update_composite(arena_t *m, occ_t f, uint32_t n, occ_t *a, occ_t v) {
244 composite_t *tmp;
245
246 tmp = arena_alloc_composite(m, n + 2);
247 init_update(tmp, f, n, a, v);
248 return tmp;
249 }
250
arena_tuple_composite(arena_t * m,uint32_t n,occ_t * a)251 composite_t *arena_tuple_composite(arena_t *m, uint32_t n, occ_t *a) {
252 composite_t *tmp;
253
254 tmp = arena_alloc_composite(m, n);
255 init_tuple(tmp, n, a);
256 return tmp;
257 }
258
arena_eq_composite(arena_t * m,occ_t t1,occ_t t2)259 composite_t *arena_eq_composite(arena_t *m, occ_t t1, occ_t t2) {
260 composite_t *tmp;
261
262 tmp = arena_alloc_composite(m, 2);
263 init_eq(tmp, t1, t2);
264 return tmp;
265 }
266
arena_distinct_composite(arena_t * m,uint32_t n,occ_t * a)267 composite_t *arena_distinct_composite(arena_t *m, uint32_t n, occ_t *a) {
268 composite_t *tmp;
269
270 tmp = arena_alloc_composite(m, n);
271 init_distinct(tmp, n, a);
272 return tmp;
273 }
274
arena_ite_composite(arena_t * m,occ_t t1,occ_t t2,occ_t t3)275 composite_t *arena_ite_composite(arena_t *m, occ_t t1, occ_t t2, occ_t t3) {
276 composite_t *tmp;
277
278 tmp = arena_alloc_composite(m, 3);
279 init_ite(tmp, t1, t2, t3);
280 return tmp;
281 }
282
arena_or_composite(arena_t * m,uint32_t n,occ_t * a)283 composite_t *arena_or_composite(arena_t *m, uint32_t n, occ_t *a) {
284 composite_t *tmp;
285
286 tmp = arena_alloc_composite(m, n);
287 init_or(tmp, n, a);
288 return tmp;
289 }
290
arena_lambda_composite(arena_t * m,occ_t t,int32_t tag)291 composite_t *arena_lambda_composite(arena_t *m, occ_t t, int32_t tag) {
292 composite_t *tmp;
293
294 tmp = arena_alloc_lambda_composite(m);
295 init_lambda(tmp, t, tag);
296 return tmp;
297 }
298
299
300 /*
301 * Variants for or and distinct: do not allocate the hook parts
302 * - these composites cannot be attached to the parents vectors
303 */
new_distinct_composite_var(uint32_t n,occ_t * a)304 composite_t *new_distinct_composite_var(uint32_t n, occ_t *a) {
305 composite_t *tmp;
306 uint32_t i;
307
308 assert(n <= MAX_COMPOSITE_ARITY);
309
310 tmp = (composite_t *) safe_malloc(sizeof(composite_t) + n * sizeof(int32_t));
311 init_header(tmp, mk_distinct_tag(n));
312 for (i=0; i<n; i++) {
313 tmp->child[i] = a[i];
314 }
315
316 return tmp;
317 }
318
new_or_composite_var(uint32_t n,occ_t * a)319 composite_t *new_or_composite_var(uint32_t n, occ_t *a) {
320 composite_t *tmp;
321 uint32_t i;
322
323 assert(n <= MAX_COMPOSITE_ARITY);
324
325 tmp = (composite_t *) safe_malloc(sizeof(composite_t) + n * sizeof(int32_t));
326 init_header(tmp, mk_or_tag(n));
327 for (i=0; i<n; i++) {
328 tmp->child[i] = a[i];
329 }
330
331 return tmp;
332 }
333
334
335
336
337 /**************************
338 * HASH-CONSING SUPPORT *
339 *************************/
340
341 /*
342 * Syntactic equality:
343 * check whether c == (apply f a[0] ... a[n-1]) etc.
344 */
equal_children(int32_t * ch,uint32_t n,occ_t * a)345 static inline bool equal_children(int32_t *ch, uint32_t n, occ_t *a) {
346 uint32_t i;
347
348 for (i=0; i<n; i++) {
349 if (ch[i] != a[i]) return false;
350 }
351 return true;
352 }
353
354
equal_apply(composite_t * c,occ_t f,uint32_t n,occ_t * a)355 bool equal_apply(composite_t *c, occ_t f, uint32_t n, occ_t *a) {
356 return c->tag == mk_apply_tag(n + 1) && c->child[0] == f &&
357 equal_children(c->child + 1, n, a);
358 }
359
equal_update(composite_t * c,occ_t f,uint32_t n,occ_t * a,occ_t v)360 bool equal_update(composite_t *c, occ_t f, uint32_t n, occ_t *a, occ_t v) {
361 return c->tag == mk_update_tag(n + 2) && c->child[0] == f &&
362 equal_children(c->child + 1, n, a) && c->child[n+1] == v;
363 }
364
equal_tuple(composite_t * c,uint32_t n,occ_t * a)365 bool equal_tuple(composite_t *c, uint32_t n, occ_t *a) {
366 return c->tag == mk_tuple_tag(n) && equal_children(c->child, n, a);
367 }
368
equal_eq(composite_t * c,occ_t t1,occ_t t2)369 bool equal_eq(composite_t *c, occ_t t1, occ_t t2) {
370 return c->tag == mk_eq_tag() && c->child[0] == t1 && c->child[1] == t2;
371 }
372
equal_ite(composite_t * c,occ_t t1,occ_t t2,occ_t t3)373 bool equal_ite(composite_t *c, occ_t t1, occ_t t2, occ_t t3) {
374 return c->tag == mk_ite_tag() && c->child[0] == t1 &&
375 c->child[1] == t2 && c->child[2] == t3;
376 }
377
equal_distinct(composite_t * c,uint32_t n,occ_t * a)378 bool equal_distinct(composite_t *c, uint32_t n, occ_t *a) {
379 return c->tag == mk_distinct_tag(n) && equal_children(c->child, n, a);
380 }
381
equal_or(composite_t * c,uint32_t n,occ_t * a)382 bool equal_or(composite_t *c, uint32_t n, occ_t *a) {
383 return c->tag == mk_or_tag(n) && equal_children(c->child, n, a);
384 }
385
equal_lambda(composite_t * c,occ_t t,int32_t tag)386 bool equal_lambda(composite_t *c, occ_t t, int32_t tag) {
387 return c->tag == mk_lambda_tag() && c->child[0] == t && c->child[2] == tag;
388 }
389
390
391 /*
392 * The hash functions are based on Jenkins's lookup3.c code
393 * (public domain code, see http://www.burtleburtle.net)
394 */
395 #define rot(x,k) (((x)<<(k)) | ((x)>>(32-(k))))
396
397 #define mix(x,y,z) \
398 { \
399 x -= z; x ^= rot(z, 4); z += y; \
400 y -= x; y ^= rot(x, 6); x += z; \
401 z -= y; z ^= rot(y, 8); y += x; \
402 x -= z; x ^= rot(z,16); z += y; \
403 y -= x; y ^= rot(x,19); x += z; \
404 z -= y; z ^= rot(y, 4); y += x; \
405 }
406
407 #define final(x,y,z) \
408 { \
409 z ^= y; z -= rot(y,14); \
410 x ^= z; x -= rot(z,11); \
411 y ^= x; y -= rot(x,25); \
412 z ^= y; z -= rot(y,16); \
413 x ^= z; x -= rot(z,4); \
414 y ^= x; y -= rot(x,14); \
415 z ^= y; z -= rot(y,24); \
416 }
417
418 #define hash_uint32(x) \
419 { \
420 x = (x + 0x7ed55d16) + (x<<12); \
421 x = (x ^ 0xc761c23c) ^ (x>>19); \
422 x = (x + 0x165667b1) + (x<<5); \
423 x = (x + 0xd3a2646c) ^ (x<<9); \
424 x = (x + 0xfd7046c5) + (x<<3); \
425 x = (x ^ 0xb55a4f09) ^ (x>>16); \
426 }
427
428
429
430 /*
431 * Combine x, y, z with a[0] .. a[n-1]
432 */
hash_aux(uint32_t n,int32_t * a,uint32_t x,uint32_t y,uint32_t z)433 static uint32_t hash_aux(uint32_t n, int32_t *a, uint32_t x, uint32_t y, uint32_t z) {
434 while (n > 3) {
435 x += a[0];
436 y += a[1];
437 z += a[2];
438 mix(x, y, z);
439 n -= 3;
440 a += 3;
441 }
442
443 switch (n) {
444 case 3: z += a[2];
445 case 2: y += a[1];
446 case 1: x += a[0];
447 final(x, y, z);
448 default:
449 break;
450 }
451
452 return z;
453 }
454
455
456 /*
457 * Hashcode for hash-consing
458 * (not the same as the internal c->hash, which is used for congruence)
459 */
hash_apply(occ_t f,uint32_t n,occ_t * a)460 uint32_t hash_apply(occ_t f, uint32_t n, occ_t *a) {
461 return hash_aux(n, a, f + mk_apply_tag(n+1), 0x1abe2834, 0x1abe2834);
462 }
463
hash_update(occ_t f,uint32_t n,occ_t * a,occ_t v)464 uint32_t hash_update(occ_t f, uint32_t n, occ_t *a, occ_t v) {
465 return hash_aux(n, a, f + mk_update_tag(n+2), v, 0x81238354);
466 }
467
hash_tuple(uint32_t n,occ_t * a)468 uint32_t hash_tuple(uint32_t n, occ_t *a) {
469 return hash_aux(n, a, mk_tuple_tag(n), 0x3ef56a27, 0x3ef56a27);
470 }
471
hash_eq(occ_t t1,occ_t t2)472 uint32_t hash_eq(occ_t t1, occ_t t2) {
473 uint32_t x;
474
475 x = (t1 << 16) + t2;
476 hash_uint32(x);
477 return x;
478 }
479
hash_ite(occ_t t1,occ_t t2,occ_t t3)480 uint32_t hash_ite(occ_t t1, occ_t t2, occ_t t3) {
481 uint32_t x, y, z;
482
483 x = t1;
484 y = t2;
485 z = t3;
486 final(x, y, z);
487
488 return z;
489 }
490
hash_distinct(uint32_t n,occ_t * a)491 uint32_t hash_distinct(uint32_t n, occ_t *a) {
492 return hash_aux(n, a, mk_distinct_tag(n), 0xdef67a81, 0xdef67a81);
493 }
494
hash_or(uint32_t n,occ_t * a)495 uint32_t hash_or(uint32_t n, occ_t *a) {
496 return hash_aux(n, a, mk_or_tag(n), 0x9279a675, 0x9279a675);
497 }
498
hash_lambda(occ_t t,int32_t tag)499 uint32_t hash_lambda(occ_t t, int32_t tag) {
500 uint32_t x, y, z;
501
502 x = t;
503 y = tag;
504 z = 0xabdaabda;
505 final(x, y, z);
506
507 return z;
508 }
509
510
hash_composite(composite_t * c)511 uint32_t hash_composite(composite_t *c) {
512 uint32_t tag, n;
513
514 tag = c->tag;
515 n = tag_arity(tag);
516
517 switch (tag_kind(tag)) {
518 case COMPOSITE_APPLY:
519 return hash_apply(c->child[0], n - 1, c->child + 1);
520 case COMPOSITE_UPDATE:
521 return hash_update(c->child[0], n - 2, c->child + 1, c->child[n - 1]);
522 case COMPOSITE_TUPLE:
523 return hash_tuple(n, c->child);
524 case COMPOSITE_EQ:
525 return hash_eq(c->child[0], c->child[1]);
526 case COMPOSITE_ITE:
527 return hash_ite(c->child[0], c->child[1], c->child[2]);
528 case COMPOSITE_DISTINCT:
529 return hash_distinct(n, c->child);
530 case COMPOSITE_OR:
531 return hash_or(n, c->child);
532 case COMPOSITE_LAMBDA:
533 return hash_lambda(c->child[0], c->child[2]);
534 }
535 // prevent GCC warning
536 assert(false);
537 return 0;
538 }
539
540
541
542 /**********************************************
543 * ADDITION AND REMOVAL FROM PARENT VECTORS *
544 *********************************************/
545
546 /*
547 * Get class id for t (i.e., remove the polarity bits)
548 */
get_class(elabel_t * label,occ_t t)549 static inline class_t get_class(elabel_t *label, occ_t t) {
550 return class_of(label[term_of_occ(t)]);
551 }
552
553 /*
554 * Get label for t:
555 * - if t has positive polarity, that's label[term_of(t)]
556 * - if t has negative polarity, that's label[term_of(t)] ^ 1 (flipped polarity)
557 */
get_label(elabel_t * label,occ_t t)558 static inline elabel_t get_label(elabel_t *label, occ_t t) {
559 return label[term_of_occ(t)] ^ polarity_of_occ(t);
560 }
561
562 /*
563 * Check whether c0 = class of child[i] is a duplicate, i.e.,
564 * whether there's a j<i such that get_class(child[j]) == c0
565 */
duplicate_class(occ_t * child,elabel_t * label,class_t c0,uint32_t i)566 static bool duplicate_class(occ_t *child, elabel_t *label, class_t c0, uint32_t i) {
567 uint32_t j;
568
569 for (j=0; j<i; j++) {
570 if (get_class(label, child[j]) == c0) return true;
571 }
572 return false;
573 }
574
575 /*
576 * Attach c to the use vectors u, using labeling label
577 * - if c->child[i] = t, then c is added to u[k]
578 * where k = class of t = class_of(label[term_of(t)])
579 */
attach_composite(composite_t * c,elabel_t * label,use_vector_t * u)580 void attach_composite(composite_t *c, elabel_t *label, use_vector_t *u) {
581 uint32_t i, n;
582 int32_t *h, *child;
583 int32_t k;
584 class_t c0;
585
586 n = composite_arity(c);
587 h = composite_hooks(c);
588 child = c->child;
589
590 for (i=0; i<n; i++) {
591 c0 = get_class(label, child[i]);
592 if (duplicate_class(child, label, c0, i)) {
593 h[i] = duplicate_ptr;
594 } else {
595 k = use_vector_store(u + c0, c);
596 h[i] = k;
597 }
598 }
599 }
600
601 /*
602 * Converse operation: remove c from the use vectors u
603 */
detach_composite(composite_t * c,elabel_t * label,use_vector_t * u)604 void detach_composite(composite_t *c, elabel_t *label, use_vector_t *u) {
605 uint32_t i, n;
606 int32_t *h;
607 class_t c0;
608 int32_t k;
609
610 n = composite_arity(c);
611 h = composite_hooks(c);
612 for (i=0; i<n; i++) {
613 k = h[i];
614 if (k >= 0) {
615 c0 = get_class(label, c->child[i]);
616 clear_use_vector_entry(u + c0, k);
617 }
618 }
619 }
620
621 /*
622 * Remove c from the use vectors, except u[r0]
623 */
separate_composite(composite_t * c,elabel_t * label,use_vector_t * u,class_t r0)624 void separate_composite(composite_t *c, elabel_t *label, use_vector_t *u, class_t r0) {
625 uint32_t i, n;
626 int32_t *h;
627 class_t c0;
628 int32_t k;
629
630 n = composite_arity(c);
631 h = composite_hooks(c);
632 for (i=0; i<n; i++) {
633 k = h[i];
634 c0 = get_class(label, c->child[i]);
635 if (k >= 0 && c0 != r0) {
636 clear_use_vector_entry(u + c0, k);
637 }
638 }
639 }
640
641 /*
642 * Remove the hook to r0 from c;
643 * - search for the first i such that class[child[i]] = r0.
644 * - set corresponding hook[i] to no_ptr
645 */
unhook_composite(composite_t * c,elabel_t * label,class_t r0)646 void unhook_composite(composite_t *c, elabel_t *label, class_t r0) {
647 uint32_t i, n;
648 int32_t *h;
649 class_t c0;
650
651 n = composite_arity(c);
652 h = composite_hooks(c);
653 for (i=0; i<n; i++) {
654 c0 = get_class(label, c->child[i]);
655 if (c0 == r0) {
656 h[i] = no_ptr;
657 break;
658 }
659 }
660
661 assert(i < n);
662 }
663
664 /*
665 * Hook composite c to class r0
666 * - search for the first child in that class
667 * - if its hook is negative, attach cmp to class r0
668 * - if its hook is non-negative, there's nothing to do, c is already
669 * in r0's use vector.
670 */
hook_composite(composite_t * c,elabel_t * label,use_vector_t * u,class_t r0)671 void hook_composite(composite_t *c, elabel_t *label, use_vector_t *u, class_t r0) {
672 uint32_t i, n;
673 int32_t *h;
674 class_t c0;
675 int32_t k;
676
677 n = composite_arity(c);
678 h = composite_hooks(c);
679 for (i=0; i<n; i++) {
680 c0 = get_class(label, c->child[i]);
681 if (c0 == r0) {
682 k = h[i];
683 if (k < 0) {
684 k = use_vector_store(u + r0, c);
685 h[i] = k;
686 }
687 break;
688 }
689 }
690
691 assert(i < n);
692 }
693
694
695 /*
696 * Hide c from the use vectors
697 * if u[k] = c then u[k] is marked
698 */
hide_composite(composite_t * c,elabel_t * label,use_vector_t * u)699 void hide_composite(composite_t *c, elabel_t *label, use_vector_t *u) {
700 uint32_t i, n;
701 int32_t *h;
702 class_t c0;
703 int32_t k;
704
705 n = composite_arity(c);
706 h = composite_hooks(c);
707 for (i=0; i<n; i++) {
708 k = h[i];
709 if (k >= 0) {
710 c0 = get_class(label, c->child[i]);
711 mark_use_vector_entry(u + c0, k);
712 }
713 }
714 }
715
716
717 /*
718 * Converse operation: restore c
719 * if u[k] = c then u[k] is unmarked
720 */
reveal_composite(composite_t * c,elabel_t * label,use_vector_t * u)721 void reveal_composite(composite_t *c, elabel_t *label, use_vector_t *u) {
722 uint32_t i, n;
723 int32_t *h;
724 class_t c0;
725 int32_t k;
726
727 n = composite_arity(c);
728 h = composite_hooks(c);
729 for (i=0; i<n; i++) {
730 k = h[i];
731 if (k >= 0) {
732 c0 = get_class(label, c->child[i]);
733 unmark_use_vector_entry(u + c0, k);
734 }
735 }
736 }
737
738
739
740 /****************************
741 * SIGNATURE COMPUTATION *
742 ***************************/
743
744 #define INIT_SIGN_BUFFER_SIZE 8
745
746 /*
747 * Initialize buffer s
748 */
init_sign_buffer(signature_t * s)749 void init_sign_buffer(signature_t *s) {
750 s->size = INIT_SIGN_BUFFER_SIZE;
751 s->tag = 0;
752 s->sigma = (elabel_t *) safe_malloc(INIT_SIGN_BUFFER_SIZE * sizeof(elabel_t));
753 }
754
755 /*
756 * Increase size to at least n
757 */
resize_sign_buffer(signature_t * s,uint32_t n)758 static void resize_sign_buffer(signature_t *s, uint32_t n) {
759 assert(n <= MAX_COMPOSITE_ARITY);
760 if (s->size < n) {
761 s->size = n;
762 s->sigma = (elabel_t *) safe_realloc(s->sigma, n * sizeof(elabel_t));
763 }
764 }
765
766 /*
767 * Delete
768 */
delete_sign_buffer(signature_t * s)769 void delete_sign_buffer(signature_t *s) {
770 safe_free(s->sigma);
771 s->sigma = NULL;
772 }
773
774
775 /*
776 * Normalize the signature for an equality term (eq t0 t1)
777 * - s[0] and s[1] must the labels of t0 and t1
778 * - ensure lhs has positive polarity and lhs < rhs
779 */
normalize_sigma_eq(elabel_t * s)780 static void normalize_sigma_eq(elabel_t *s) {
781 elabel_t l;
782 uint32_t sgn;
783
784 if (s[1] < s[0]) {
785 l = s[0]; s[0] = s[1]; s[1] = l;
786 }
787 sgn = sign_of(s[0]);
788 s[0] ^= sgn;
789 s[1] ^= sgn;
790 }
791
792
793
794
795 /*
796 * Simple signature for apply/update/tuple terms
797 */
signature_basic(composite_t * c,elabel_t * label,signature_t * s)798 void signature_basic(composite_t *c, elabel_t *label, signature_t *s) {
799 uint32_t i, n, tag;
800
801 tag = c->tag;
802 n = tag_arity(tag);
803 resize_sign_buffer(s, n);
804 s->tag = tag;
805 for (i=0; i<n; i++) {
806 s->sigma[i] = get_label(label, c->child[i]);
807 }
808 }
809
810 /*
811 * equality term
812 */
signature_eq(composite_t * c,elabel_t * label,signature_t * s)813 void signature_eq(composite_t *c, elabel_t *label, signature_t *s) {
814 assert(c->tag == mk_eq_tag());
815 s->tag = mk_eq_tag();
816 s->sigma[0] = get_label(label, c->child[0]);
817 s->sigma[1] = get_label(label, c->child[1]);
818 normalize_sigma_eq(s->sigma);
819 }
820
821 /*
822 * Normalize: make l0 positive, swap l1 and l2 if necessary
823 * (i.e., rewrite (ite (not t) t1 t2) to (ite t t2 t1))
824 */
signature_ite(composite_t * c,elabel_t * label,signature_t * s)825 void signature_ite(composite_t *c, elabel_t *label, signature_t *s) {
826 elabel_t l0, l1, l2;
827
828 assert(c->tag == mk_ite_tag());
829 l0 = get_label(label, c->child[0]);
830 l1 = get_label(label, c->child[1]);
831 l2 = get_label(label, c->child[2]);
832
833 s->tag = mk_ite_tag();
834 if (is_pos_label(l0)) {
835 s->sigma[0] = l0;
836 s->sigma[1] = l1;
837 s->sigma[2] = l2;
838 } else {
839 s->sigma[0] = opposite_label(l0);
840 s->sigma[1] = l2;
841 s->sigma[2] = l1;
842 }
843 }
844
845 /*
846 * Sort labels in increasing order
847 */
signature_distinct(composite_t * c,elabel_t * label,signature_t * s)848 void signature_distinct(composite_t *c, elabel_t *label, signature_t *s) {
849 uint32_t i, n;
850 occ_t *t;
851
852 assert(composite_kind(c) == COMPOSITE_DISTINCT);
853 n = composite_arity(c);
854 t = c->child;
855
856 resize_sign_buffer(s, n);
857 for (i=0; i<n; i++) {
858 s->sigma[i] = get_label(label, t[i]);
859 }
860
861 int_array_sort(s->sigma, n);
862 s->tag = mk_distinct_tag(n);
863 }
864
865 /*
866 * Sort, remove false and duplicate labels
867 */
signature_or(composite_t * c,elabel_t * label,signature_t * s)868 void signature_or(composite_t *c, elabel_t *label, signature_t *s) {
869 uint32_t i, j, n;
870 elabel_t l, l_aux, *a;
871 occ_t *t;
872
873 assert(composite_kind(c) == COMPOSITE_OR);
874 n = composite_arity(c);
875 a = s->sigma;
876 t = c->child;
877
878 resize_sign_buffer(s, n);
879
880 // copy labels of t[0] ... t[n-1]
881 // remove t[i] if t[i] == false
882 j = 0;
883 for (i=0; i<n; i++) {
884 l = get_label(label, t[i]);
885 if (l != false_label) {
886 a[j] = l;
887 j ++;
888 }
889 }
890 n = j;
891
892 if (n > 1) {
893 // sort and remove duplicates
894 int_array_sort(a, n);
895
896 l = a[0];
897 j = 1;
898 for (i=1; i<n; i++) {
899 l_aux = a[i];
900 if (l_aux != l) {
901 a[j] = l_aux;
902 j ++;
903 l = l_aux;
904 }
905 }
906 }
907
908 s->tag = mk_or_tag(j);
909 }
910
911
912 /*
913 * For a lambda:
914 * - the signature depends on label[c->child[0]] and on c->child[2] (lambda tag)
915 */
signature_lambda(composite_t * c,elabel_t * label,signature_t * s)916 void signature_lambda(composite_t *c, elabel_t *label, signature_t *s) {
917 assert(composite_kind(c) == COMPOSITE_LAMBDA && composite_arity(c) == 1);
918
919 s->tag = mk_lambda_tag();
920 s->sigma[0] = get_label(label, c->child[0]);
921 s->sigma[1] = c->child[2];
922 }
923
924
925 /*
926 * Generic form
927 */
signature_composite(composite_t * c,elabel_t * label,signature_t * s)928 void signature_composite(composite_t *c, elabel_t *label, signature_t *s) {
929 switch (composite_kind(c)) {
930 case COMPOSITE_APPLY:
931 case COMPOSITE_UPDATE:
932 case COMPOSITE_TUPLE:
933 signature_basic(c, label, s);
934 break;
935
936 case COMPOSITE_EQ:
937 signature_eq(c, label, s);
938 break;
939
940 case COMPOSITE_ITE:
941 signature_ite(c, label, s);
942 break;
943
944 case COMPOSITE_DISTINCT:
945 signature_distinct(c, label, s);
946 break;
947
948 case COMPOSITE_OR:
949 signature_or(c, label, s);
950 break;
951
952 case COMPOSITE_LAMBDA:
953 signature_lambda(c, label, s);
954 break;
955 }
956 }
957
958
959
960 /*
961 * Compute a hash of signature s
962 */
hash_signature(signature_t * s)963 uint32_t hash_signature(signature_t *s) {
964 uint32_t n;
965
966 n = tag_arity(s->tag);
967 return hash_aux(n, s->sigma, s->tag, 0xdeadbeef, 0xdeadbeef);
968 }
969
970
971
972 /*
973 * Check whether s1 and s2 are equal
974 */
equal_signatures(signature_t * s1,signature_t * s2)975 bool equal_signatures(signature_t *s1, signature_t *s2) {
976 uint32_t tag, i, n;
977
978 tag = s1->tag;
979 if (tag != s2->tag) return false;
980
981 n = tag_arity(tag);
982 for (i=0; i<n; i++) {
983 if (s1->sigma[i] != s2->sigma[i]) return false;
984 }
985
986 return true;
987 }
988
989
990 /*
991 * Check whether c's signature is equal to s
992 */
signature_matches(composite_t * c,signature_t * s,signature_t * aux,elabel_t * label)993 bool signature_matches(composite_t *c, signature_t *s, signature_t *aux, elabel_t *label) {
994 uint32_t i, n, c_tag, s_tag;
995 elabel_t l[3];
996
997 c_tag = c->tag;
998 s_tag = s->tag;
999 if (tag_kind(c_tag) != tag_kind(s_tag)) return false;
1000
1001 switch (tag_kind(c_tag)) {
1002 case COMPOSITE_APPLY:
1003 case COMPOSITE_UPDATE:
1004 case COMPOSITE_TUPLE:
1005 n = tag_arity(c_tag);
1006 if (n != tag_arity(s_tag)) return false;
1007 for (i=0; i<n; i++) {
1008 if (s->sigma[i] != get_label(label, c->child[i])) {
1009 return false;
1010 }
1011 }
1012 return true;
1013
1014 case COMPOSITE_EQ:
1015 l[0] = get_label(label, c->child[0]);
1016 l[1] = get_label(label, c->child[1]);
1017 normalize_sigma_eq(l);
1018 return s->sigma[0] == l[0] && s->sigma[1] == l[1];
1019
1020 case COMPOSITE_ITE:
1021 l[0] = get_label(label, c->child[0]);
1022 l[1] = get_label(label, c->child[1]);
1023 l[2] = get_label(label, c->child[2]);
1024 return (s->sigma[0] == l[0] && s->sigma[1] == l[1] && s->sigma[2] == l[2])
1025 || (s->sigma[0] == opposite_label(l[0]) && s->sigma[1] == l[2] && s->sigma[2] == l[1]);
1026
1027 case COMPOSITE_DISTINCT:
1028 signature_distinct(c, label, aux);
1029 return equal_signatures(s, aux);
1030
1031 case COMPOSITE_OR:
1032 signature_or(c, label, aux);
1033 return equal_signatures(s, aux);
1034
1035 case COMPOSITE_LAMBDA:
1036 return s->sigma[0] == get_label(label, c->child[0]) && s->sigma[1] == c->child[2];
1037 }
1038
1039 // prevents a GCC warning
1040 assert(false);
1041 return false;
1042 }
1043
1044
1045
1046 /**********************************
1047 * SUPPORT FOR THE ARRAY SOLVER *
1048 *********************************/
1049
1050 /*
1051 * Signature of (apply g i_1 ... i_n) given c = (apply f i_1 ... i_n)
1052 */
signature_modified_apply(composite_t * c,eterm_t g,elabel_t * label,signature_t * s)1053 void signature_modified_apply(composite_t *c, eterm_t g, elabel_t *label, signature_t *s) {
1054 uint32_t i, n, tag;
1055
1056 tag = c->tag;
1057 n = tag_arity(tag);
1058 resize_sign_buffer(s, n);
1059 s->tag = tag;
1060 s->sigma[0] = label[g]; // function term = label of g
1061 for (i=1; i<n; i++) { // children
1062 s->sigma[i] = get_label(label, composite_child(c, i));
1063 }
1064 }
1065
1066
1067 /*
1068 * Variant: signature of (apply glabel i1 ... in)
1069 */
signature_modified_apply2(composite_t * c,elabel_t glabel,elabel_t * label,signature_t * s)1070 void signature_modified_apply2(composite_t *c, elabel_t glabel, elabel_t *label, signature_t *s) {
1071 uint32_t i, n, tag;
1072
1073 tag = c->tag;
1074 n = tag_arity(tag);
1075 resize_sign_buffer(s, n);
1076 s->tag = tag;
1077 s->sigma[0] = glabel; // function label
1078 for (i=1; i<n; i++) { // children
1079 s->sigma[i] = get_label(label, composite_child(c, i));
1080 }
1081 }
1082
1083
1084 /*
1085 * Check whether two apply composites have the same argument tuple (modulo the egraph)
1086 * - c must be of the form (apply f i_1 ... i_n)
1087 * d must be of the form (apply g j_i ... j_m)
1088 * - return true if n == m and label[i_1] = label[j_1], ..., label[i_n] = label[j_m]
1089 */
same_arg_signature(composite_t * c,composite_t * d,elabel_t * label)1090 bool same_arg_signature(composite_t *c, composite_t *d, elabel_t *label) {
1091 uint32_t i, n;
1092
1093 assert(composite_kind(c) == COMPOSITE_APPLY && composite_kind(d) == COMPOSITE_APPLY);
1094
1095 n = composite_arity(c);
1096 if (n != composite_arity(d)) {
1097 return false;
1098 }
1099
1100 for (i=1; i<n; i++) {
1101 if (get_label(label, composite_child(c, i)) != get_label(label, composite_child(d, i))) {
1102 return false;
1103 }
1104 }
1105
1106 return true;
1107 }
1108
1109
1110 /*
1111 * Compute a hash code of c's argument tuple
1112 * - c must be of the form (apply f i_1 ... i_n)
1113 * - return a hash computed based one n and label[i_1], ..., label[i_n]
1114 * - so if same_arg_signature(c, d, label) is true then
1115 * hash_arg_signature(c, label) = hash_arg_signature(d, label).
1116 */
hash_arg_signature(composite_t * c,elabel_t * label)1117 uint32_t hash_arg_signature(composite_t *c, elabel_t *label) {
1118 int32_t *a;
1119 uint32_t n;
1120 uint32_t x, y, z;
1121
1122 assert(composite_kind(c) == COMPOSITE_APPLY);
1123 n = composite_arity(c);
1124 assert(n > 0);
1125 n --;
1126 a = c->child + 1; // skip child[0] = f
1127
1128 x = y = z = 0xdeadbeef + (n << 2);
1129 while (n > 3) {
1130 x += (uint32_t) get_label(label, a[0]);
1131 y += (uint32_t) get_label(label, a[1]);
1132 z += (uint32_t) get_label(label, a[2]);
1133 mix(x, y, z);
1134 n -= 3;
1135 a += 3;
1136 }
1137
1138 switch (n) {
1139 case 3: z += (uint32_t) get_label(label, a[2]);
1140 case 2: y += (uint32_t) get_label(label, a[1]);
1141 case 1: x += (uint32_t) get_label(label, a[0]);
1142 final(x, y, z);
1143 default:
1144 break;
1145 }
1146
1147 return z;
1148 }
1149
1150
1151
1152
1153 /**********************
1154 * CONGRUENCE TABLE *
1155 *********************/
1156
1157 /*
1158 * For debugging: check whether n is a power of two
1159 */
1160 #ifndef NDEBUG
is_power_of_two(uint32_t n)1161 static bool is_power_of_two(uint32_t n) {
1162 return (n & (n - 1)) == 0;
1163 }
1164 #endif
1165
1166
1167 /*
1168 * Initialization.
1169 * - n = size, if n = 0, the default size is used.
1170 */
init_congruence_table(congruence_table_t * tbl,uint32_t n)1171 void init_congruence_table(congruence_table_t *tbl, uint32_t n) {
1172 uint32_t i;
1173 composite_t **tmp;
1174
1175 if (n == 0) {
1176 n = DEFAULT_CONGRUENCE_TBL_SIZE;
1177 }
1178
1179 if (n >= MAX_CONGRUENCE_TBL_SIZE) {
1180 out_of_memory();
1181 }
1182
1183 assert(is_power_of_two(n));
1184
1185 tmp = (composite_t **) safe_malloc(n * sizeof(composite_t *));
1186 for (i=0; i<n; i++) {
1187 tmp[i] = NULL_COMPOSITE;
1188 }
1189
1190 tbl->data = tmp;
1191 tbl->size = n;
1192 tbl->nelems = 0;
1193 tbl->ndeleted = 0;
1194
1195 tbl->resize_threshold = (uint32_t)(n * CONGRUENCE_TBL_RESIZE_RATIO);
1196 tbl->cleanup_threshold = (uint32_t)(n * CONGRUENCE_TBL_CLEANUP_RATIO);
1197
1198 init_sign_buffer(&tbl->buffer);
1199 }
1200
1201
1202 /*
1203 * Reset: remove all composites
1204 */
reset_congruence_table(congruence_table_t * tbl)1205 void reset_congruence_table(congruence_table_t *tbl) {
1206 uint32_t i, n;
1207
1208 n = tbl->size;
1209 for (i=0; i<n; i++) {
1210 tbl->data[i] = NULL_COMPOSITE;
1211 }
1212
1213 tbl->nelems = 0;
1214 tbl->ndeleted = 0;
1215 }
1216
1217
1218 /*
1219 * Delete
1220 */
delete_congruence_table(congruence_table_t * tbl)1221 void delete_congruence_table(congruence_table_t *tbl) {
1222 safe_free(tbl->data);
1223 tbl->data = NULL;
1224 delete_sign_buffer(&tbl->buffer);
1225 }
1226
1227
1228 /*
1229 * Store composite d in a clean data array
1230 * - mask = size of data - 1
1231 * - d->hash is the hash code of d
1232 * data must not contain any deleted eterms and must have at least one empty slot
1233 */
congruence_table_clean_copy(composite_t ** data,composite_t * d,uint32_t mask)1234 static void congruence_table_clean_copy(composite_t **data, composite_t *d, uint32_t mask) {
1235 uint32_t j;
1236
1237 j = d->hash & mask;
1238 while (data[j] != NULL_COMPOSITE) {
1239 j ++;
1240 j &= mask;
1241 }
1242 data[j] = d;
1243 }
1244
1245
1246 /*
1247 * Check whether a pointer is non-deleted and non-null
1248 */
live_ptr(composite_t * d)1249 static inline bool live_ptr(composite_t *d) {
1250 return (((uintptr_t) d) & ~((uintptr_t) 1)) != 0;
1251 }
1252
1253
1254 /*
1255 * Remove deleted elements
1256 */
congruence_table_cleanup(congruence_table_t * tbl)1257 static void congruence_table_cleanup(congruence_table_t *tbl) {
1258 composite_t **tmp, *d;
1259 uint32_t j, n, mask;
1260
1261 n = tbl->size;
1262 tmp = (composite_t **) safe_malloc(n * sizeof(composite_t *));
1263 for (j=0; j<n; j++) {
1264 tmp[j] = NULL_COMPOSITE;
1265 }
1266
1267 mask = n - 1;
1268 for (j=0; j<n; j++) {
1269 d = tbl->data[j];
1270 if (live_ptr(d)) {
1271 congruence_table_clean_copy(tmp, d, mask);
1272 }
1273 }
1274
1275 safe_free(tbl->data);
1276 tbl->data = tmp;
1277 tbl->ndeleted = 0;
1278 }
1279
1280
1281 /*
1282 * Remove deleted elements and make the table twice as large
1283 */
congruence_table_extend(congruence_table_t * tbl)1284 static void congruence_table_extend(congruence_table_t *tbl) {
1285 composite_t **tmp;
1286 uint32_t n, n2, j, mask;
1287 composite_t *d;
1288
1289 n = tbl->size;
1290 n2 = n<<1;
1291 if (n2 >= MAX_CONGRUENCE_TBL_SIZE) {
1292 out_of_memory();
1293 }
1294
1295 tmp = (composite_t **) safe_malloc(n2 * sizeof(composite_t *));
1296 for (j=0; j<n2; j++) {
1297 tmp[j] = NULL_COMPOSITE;
1298 }
1299
1300 mask = n2 - 1;
1301 for (j=0; j<n; j++) {
1302 d = tbl->data[j];
1303 if (live_ptr(d)) {
1304 congruence_table_clean_copy(tmp, d, mask);
1305 }
1306 }
1307
1308 safe_free(tbl->data);
1309 tbl->data = tmp;
1310 tbl->ndeleted = 0;
1311 tbl->size = n2;
1312
1313 tbl->resize_threshold = (uint32_t)(n2 * CONGRUENCE_TBL_RESIZE_RATIO);
1314 tbl->cleanup_threshold = (uint32_t)(n2 * CONGRUENCE_TBL_CLEANUP_RATIO);
1315 }
1316
1317
1318 /*
1319 * Remove c from the congruence table.
1320 * - c must be in the table otherwise the function loops
1321 */
congruence_table_remove(congruence_table_t * tbl,composite_t * c)1322 void congruence_table_remove(congruence_table_t *tbl, composite_t *c) {
1323 uint32_t mask, j;
1324
1325 mask = tbl->size - 1;
1326 j = c->hash & mask;
1327 while (tbl->data[j] != c) {
1328 j ++;
1329 j &= mask;
1330 }
1331
1332 assert(tbl->data[j] == c);
1333 tbl->data[j] = DELETED_COMPOSITE;
1334 tbl->nelems --;
1335 tbl->ndeleted ++;
1336 if (tbl->ndeleted > tbl->cleanup_threshold) {
1337 congruence_table_cleanup(tbl);
1338 }
1339 }
1340
1341
1342 /*
1343 * Remove c from the table if it's present. No change otherwise.
1344 * The table must not be full.
1345 * - return true if c has been removed
1346 * - return false if c was not present
1347 */
congruence_table_remove_if_present(congruence_table_t * tbl,composite_t * c)1348 bool congruence_table_remove_if_present(congruence_table_t *tbl, composite_t *c) {
1349 uint32_t mask, j;
1350 composite_t *aux;
1351
1352 assert(tbl->size > tbl->ndeleted + tbl->nelems);
1353
1354 mask = tbl->size - 1;
1355 j = c->hash & mask;
1356 for (;;) {
1357 aux = tbl->data[j];
1358 if (aux == c) break;
1359 if (aux == NULL_COMPOSITE) return false; // c not in the table
1360 j ++;
1361 j &= mask;
1362 }
1363
1364 assert(tbl->data[j] == c);
1365 tbl->data[j] = DELETED_COMPOSITE;
1366 tbl->nelems --;
1367 tbl->ndeleted ++;
1368 if (tbl->ndeleted > tbl->cleanup_threshold) {
1369 congruence_table_cleanup(tbl);
1370 }
1371
1372 return true;
1373 }
1374
1375
1376
1377
1378 /*
1379 * Add c to tbl,
1380 * - use only if it is known that no term is congruent to c
1381 */
congruence_table_add(congruence_table_t * tbl,composite_t * c)1382 void congruence_table_add(congruence_table_t *tbl, composite_t *c) {
1383 uint32_t mask, j;
1384
1385 assert(tbl->size > tbl->ndeleted + tbl->nelems);
1386
1387 mask = tbl->size - 1;
1388 j = c->hash & mask;
1389 while (live_ptr(tbl->data[j])) {
1390 j ++;
1391 j &= mask;
1392 }
1393
1394 if (tbl->data[j] == DELETED_COMPOSITE) {
1395 assert(tbl->ndeleted > 0);
1396 tbl->ndeleted --;
1397 }
1398
1399 tbl->data[j] = c;
1400 tbl->nelems ++;
1401 if (tbl->nelems + tbl->ndeleted > tbl->resize_threshold) {
1402 congruence_table_extend(tbl);
1403 }
1404 }
1405
1406
1407 /*
1408 * Search for a composite of signature s in the table.
1409 * Return NULL_COMPOSITE if there's none.
1410 * - the table must not be full
1411 */
congruence_table_find(congruence_table_t * tbl,signature_t * s,elabel_t * label)1412 composite_t *congruence_table_find(congruence_table_t *tbl, signature_t *s, elabel_t *label) {
1413 uint32_t mask, j, h;
1414 composite_t *c;
1415
1416 mask = tbl->size - 1;
1417 h = hash_signature(s);
1418 j = h & mask;
1419 for (;;) {
1420 c = tbl->data[j];
1421 if (c == NULL_COMPOSITE ||
1422 (c != DELETED_COMPOSITE && c->hash == h && signature_matches(c, s, &tbl->buffer, label))) {
1423 return c;
1424 }
1425 j ++;
1426 j &= mask;
1427 }
1428 }
1429
1430
1431
1432
1433 /*
1434 * Auxiliary functions for find_eq to avoid intermediate signature buffer
1435 */
1436 // cf. hash_signature
hash_sigma_eq(elabel_t * sigma)1437 static inline uint32_t hash_sigma_eq(elabel_t *sigma) {
1438 return hash_aux(2, sigma, mk_eq_tag(), 0xdeadbeef, 0xdeadbeef);
1439 }
1440
matches_sigma_eq(composite_t * c,elabel_t * sigma,elabel_t * label)1441 static inline bool matches_sigma_eq(composite_t *c, elabel_t *sigma, elabel_t *label) {
1442 elabel_t s[2];
1443 s[0] = get_label(label, c->child[0]);
1444 s[1] = get_label(label, c->child[1]);
1445 normalize_sigma_eq(s);
1446 return s[0] == sigma[0] && s[1] == sigma[1];
1447 }
1448
1449
1450 /*
1451 * Search for a composite congruent to (eq t1 t2)
1452 * - return NULL_COMPOSITE if there's none
1453 */
congruence_table_find_eq(congruence_table_t * tbl,occ_t t1,occ_t t2,elabel_t * label)1454 composite_t *congruence_table_find_eq(congruence_table_t *tbl, occ_t t1, occ_t t2, elabel_t *label) {
1455 uint32_t mask, j, h;
1456 composite_t *c;
1457 elabel_t s[2];
1458
1459 s[0] = get_label(label, t1);
1460 s[1] = get_label(label, t2);
1461 normalize_sigma_eq(s);
1462 h = hash_sigma_eq(s);
1463
1464 mask = tbl->size - 1;
1465 j = h & mask;
1466 for (;;) {
1467 c = tbl->data[j];
1468 if (c == NULL_COMPOSITE ||
1469 (c != DELETED_COMPOSITE &&
1470 c->tag == mk_eq_tag() && c->hash == h && matches_sigma_eq(c, s, label))) {
1471 return c;
1472 }
1473 j ++;
1474 j &= mask;
1475 }
1476
1477 }
1478
1479
1480 /*
1481 * Find a composite term congruent to c modulo root in tbl.
1482 * If there is none, insert c in tbl.
1483 */
congruence_table_get(congruence_table_t * tbl,composite_t * c,signature_t * s,elabel_t * label)1484 composite_t *congruence_table_get(congruence_table_t *tbl, composite_t *c, signature_t *s, elabel_t *label) {
1485 uint32_t mask, j, k, h;
1486 composite_t *aux;
1487
1488 assert(tbl->size > tbl->ndeleted + tbl->nelems);
1489
1490 mask = tbl->size - 1;
1491 h = hash_signature(s);
1492 c->hash = h;
1493 j = h & mask;
1494
1495 for (;;) {
1496 aux = tbl->data[j];
1497 if (aux == NULL_COMPOSITE) goto add;
1498 if (aux == DELETED_COMPOSITE) break;
1499 if (aux->hash == h && signature_matches(aux, s, &tbl->buffer, label)) goto found;
1500 j ++;
1501 j &= mask;
1502 }
1503
1504 // j is where addition will happen if necessary
1505 k = j;
1506 for (;;) {
1507 k++;
1508 k &= mask;
1509 aux = tbl->data[k];
1510 if (aux == NULL_COMPOSITE) {
1511 tbl->ndeleted --;
1512 goto add;
1513 }
1514 if (aux != DELETED_COMPOSITE &&
1515 aux->hash == h && signature_matches(aux, s, &tbl->buffer, label)) goto found;
1516 }
1517
1518 add:
1519 tbl->data[j] = c;
1520 tbl->nelems ++;
1521 if (tbl->nelems + tbl->ndeleted > tbl->resize_threshold) {
1522 congruence_table_extend(tbl);
1523 }
1524 return c;
1525
1526
1527 found:
1528 return aux;
1529 }
1530
1531
1532
1533
1534 /*
1535 * Check whether c is a congruence root
1536 * - use the internal buffer to compute c's signature and hash code
1537 * - no change to c->hash
1538 */
congruence_table_is_root(congruence_table_t * tbl,composite_t * c,elabel_t * label)1539 bool congruence_table_is_root(congruence_table_t *tbl, composite_t *c, elabel_t *label) {
1540 uint32_t mask, j;
1541 signature_t *s;
1542 composite_t *aux;
1543
1544 assert(tbl->size > tbl->ndeleted + tbl->nelems);
1545
1546 s = &tbl->buffer;
1547 signature_composite(c, label, s);
1548
1549 mask = tbl->size - 1;
1550 j = hash_signature(s) & mask;
1551 for (;;) {
1552 aux = tbl->data[j];
1553 if (aux == c) return true;
1554 if (aux == NULL_COMPOSITE) return false;
1555 j ++;
1556 j &= mask;
1557 }
1558 }
1559
1560
1561