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 #include <stdio.h>
20 #include <stdint.h>
21 #include <inttypes.h>
22 #include <assert.h>
23
24 #include "io/type_printer.h"
25 #include "io/yices_pp.h"
26 #include "terms/types.h"
27 #include "utils/refcount_strings.h"
28
29 /*
30 * Short cuts
31 */
binary_function_type(type_table_t * tbl,type_t dom1,type_t dom2,type_t range)32 static type_t binary_function_type(type_table_t *tbl, type_t dom1, type_t dom2, type_t range) {
33 type_t a[2];
34
35 a[0] = dom1;
36 a[1] = dom2;
37 return function_type(tbl, range, 2, a);
38 }
39
tuple_type_pair(type_table_t * tbl,type_t t1,type_t t2)40 static type_t tuple_type_pair(type_table_t *tbl, type_t t1, type_t t2) {
41 type_t a[2];
42
43 a[0] = t1;
44 a[1] = t2;
45 return tuple_type(tbl, 2, a);
46 }
47
tuple_type_triple(type_table_t * tbl,type_t t1,type_t t2,type_t t3)48 static type_t tuple_type_triple(type_table_t *tbl, type_t t1, type_t t2, type_t t3) {
49 type_t a[3];
50
51 a[0] = t1;
52 a[1] = t2;
53 a[2] = t3;
54 return tuple_type(tbl, 3, a);
55 }
56
57 static type_table_t table;
58
59
60 /*
61 * Print a hash table
62 */
print_int_hash_table(FILE * f,int_htbl_t * tbl,uint32_t level)63 static void print_int_hash_table(FILE *f, int_htbl_t *tbl, uint32_t level) {
64 uint32_t i;
65 int_hrec_t *r;
66
67 fprintf(f, "hash table %p\n", tbl);
68 fprintf(f, " size = %"PRIu32"\n", tbl->size);
69 fprintf(f, " nelems = %"PRIu32"\n", tbl->nelems);
70 fprintf(f, " ndeleted = %"PRIu32"\n", tbl->ndeleted);
71 fprintf(f, " resize threshold = %"PRIu32"\n", tbl->resize_threshold);
72 fprintf(f, " cleanup threshold = %"PRIu32"\n", tbl->cleanup_threshold);
73 if (level >= 1) {
74 fprintf(f, " records:\n");
75 for (i=0; i<tbl->size; i++) {
76 r = tbl->records + i;
77 if (r->value >= 0) {
78 fprintf(f, " %"PRIu32": [key = %8x, val = %"PRId32"]\n", i, (unsigned) r->key, r->value);
79 }
80 }
81 }
82 if (level >= 2) {
83 fprintf(f, " deleted:\n");
84 for (i=0; i<tbl->size; i++) {
85 r = tbl->records + i;
86 if (r->value == DELETED_VALUE) {
87 fprintf(f, " %"PRIu32": [key = %8x, val = %"PRId32"]\n", i, (unsigned) r->key, r->value);
88 }
89 }
90 }
91 if (level >= 100) {
92 fprintf(f, " free:\n");
93 for (i=0; i<tbl->size; i++) {
94 r = tbl->records + i;
95 if (r->value == NULL_VALUE) {
96 fprintf(f, " %"PRIu32": [key = %8x, val = %"PRId32"]\n", i, (unsigned) r->key, r->value);
97 }
98 }
99 }
100 }
101
102
103
104 /*
105 * Print a symbol table
106 */
print_symbol_table(FILE * f,stbl_t * table,uint32_t level)107 static void print_symbol_table(FILE *f, stbl_t *table, uint32_t level) {
108 uint32_t i, k;
109 stbl_rec_t *r;
110 stbl_bank_t *b;
111
112 fprintf(f, "symbol table %p\n", table);
113 fprintf(f, " size = %"PRIu32"\n", table->size);
114 fprintf(f, " nelems = %"PRIu32"\n", table->nelems);
115 fprintf(f, " ndeleted = %"PRIu32"\n", table->ndeleted);
116 fprintf(f, " free idx = %"PRIu32"\n", table->free_idx);
117 if (level >= 1) {
118 for (i=0; i<table->size; i++) {
119 r = table->data[i];
120 if (r != NULL) {
121 fprintf(f, " bucket %"PRIu32"\n", i);
122 do {
123 fprintf(f, " [hash = %8x, value = %"PRId32", string = %s]\n", (unsigned) r->hash, r->value, r->string);
124 r = r->next;
125 } while (r != NULL);
126 }
127 }
128 }
129
130 if (level >= 3) {
131 if (table->bnk == NULL) {
132 fprintf(f, " no allocated banks\n");
133 }
134 k = table->free_idx;
135 for (b = table->bnk; b != NULL; b = b->next) {
136 fprintf(f, " bank %p\n", b);
137 for (r = b->block + k; r < b->block + STBL_BANK_SIZE; r ++) {
138 if (r->string == NULL) {
139 fprintf(f, " %p: [hash = %8x, value = %"PRId32", string = %p, next = %p]\n",
140 r, (unsigned) r->hash, r->value, r->string, r->next);
141 } else {
142 fprintf(f, " %p: [hash = %8x, value = %"PRId32", string = %s, next = %p]\n",
143 r, (unsigned) r->hash, r->value, r->string, r->next);
144 }
145 }
146 k = 0;
147 }
148 }
149
150 if (level >= 3) {
151 r = table->free_rec;
152 if (r == NULL) {
153 fprintf(f, " free list: empty\n");
154 } else {
155 fprintf(f, " free list:\n");
156 do {
157 fprintf(f, " %p: [hash = %8x, value = %"PRId32", string = %p, next = %p]\n",
158 r, (unsigned) r->hash, r->value, r->string, r->next);
159 r = r->next;
160 } while (r != NULL);
161 }
162 }
163 }
164
165
main(void)166 int main(void) {
167 type_t bv10, bv32, i, any, enumtype, ft, unit, tt;
168 type_t unit2, finite_fun;
169 type_t var1, var2, fvar1, tvar;
170
171 init_yices_pp_tables();
172
173 printf("*** Initial table ***\n");
174 init_type_table(&table, 0);
175 print_type_table(stdout, &table);
176 printf("\n");
177
178 printf("*** Naming real ***\n");
179 set_type_name(&table, real_type(&table), clone_string("R"));
180 print_type_table(stdout, &table);
181 printf("\n");
182
183 printf("*** Creating bv10 ***\n");
184 bv10 = bv_type(&table, 10);
185 print_type_table(stdout, &table);
186 printf("\n");
187
188 i = bv_type(&table, 10);
189 printf("---> bv10: %"PRId32", i: %"PRId32", depth = %"PRIu32"\n\n",
190 bv10, i, type_depth(&table, i));
191 assert(i == bv10);
192
193 printf("*** Creating bv32 ***\n");
194 bv32 = bv_type(&table, 32);
195 set_type_name(&table, bv32, clone_string("bv32"));
196 set_type_name(&table, bv32, clone_string("int32"));
197 print_type_table(stdout, &table);
198 printf("\n");
199 i = bv_type(&table, 32);
200 printf("---> bv32: %"PRId32", i: %"PRId32", depth = %"PRIu32"\n\n",
201 bv32, i, type_depth(&table, i));
202 assert(i == bv32);
203
204 printf("*** Creating any (uninterpreted) ***\n");
205 any = new_uninterpreted_type(&table);
206 set_type_name(&table, any, clone_string("any"));
207 print_type_table(stdout, &table);
208 printf("\n");
209 printf("---> any: %"PRId32", depth = %"PRIu32"\n\n", any, type_depth(&table, any));
210
211 printf("*** Creating enum (scalar 5) ***\n");
212 enumtype = new_scalar_type(&table, 5);
213 set_type_name(&table, enumtype, clone_string("enum"));
214 print_type_table(stdout, &table);
215 printf("\n");
216 printf("---> enum: %"PRId32", depth = %"PRIu32"\n\n", enumtype, type_depth(&table, enumtype));
217
218 printf("*** Creating ftype ***\n");
219 ft = binary_function_type(&table, enumtype, any, real_type(&table));
220 set_type_name(&table, ft, clone_string("ftype"));
221 i = binary_function_type(&table, enumtype, any, real_type(&table));
222 print_type_table(stdout, &table);
223 printf("\n");
224 printf("---> ft: %"PRId32", i: %"PRId32", depth = %"PRIu32"\n\n",
225 ft, i, type_depth(&table, i));
226 assert(i == ft);
227
228 printf("*** Creating unit (scalar 1) ***\n");
229 unit = new_scalar_type(&table, 1);
230 set_type_name(&table, unit, clone_string("unit"));
231 print_type_table(stdout, &table);
232 printf("\n");
233
234 printf("*** Creating unit2 (scalar 1) ***\n");
235 unit2 = new_scalar_type(&table, 1);
236 print_type_table(stdout, &table);
237 printf("\n");
238
239 printf("*** Creating unit pair ***\n");
240 (void) tuple_type_pair(&table, unit, unit2);
241 print_type_table(stdout, &table);
242 printf("\n");
243
244 printf("*** Creating finite pair ***\n");
245 (void) tuple_type_pair(&table, bool_type(&table), enumtype);
246 print_type_table(stdout, &table);
247 printf("\n");
248
249 printf("*** Creating finite function ***\n");
250 finite_fun = binary_function_type(&table, bool_type(&table), enumtype, bool_type(&table));
251 print_type_table(stdout, &table);
252 printf("\n");
253
254 printf("*** Creating unit function ***\n");
255 (void) binary_function_type(&table, int_type(&table), int_type(&table), unit);
256 print_type_table(stdout, &table);
257 printf("\n");
258
259 printf("*** Creating large finite function ***\n");
260 (void) binary_function_type(&table, finite_fun, bool_type(&table), enumtype);
261 print_type_table(stdout, &table);
262 printf("\n");
263
264 printf("*** Creating type variable (id = 0) ***\n");
265 var1 = type_variable(&table, 0);
266 set_type_name(&table, var1, clone_string("X0"));
267 print_type_table(stdout, &table);
268 printf("\n");
269 i = type_variable(&table, 0);
270 printf("---> var1 = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
271 var1, i, type_depth(&table, i));
272 assert(i == var1);
273
274 printf("*** Creating type variable (id = 100) ***\n");
275 var2 = type_variable(&table, 100);
276 print_type_table(stdout, &table);
277 printf("\n");
278 i = type_variable(&table, 100);
279 printf("---> var2 = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
280 var2, i, type_depth(&table, i));
281 assert(i == var2);
282
283 printf("*** Creating function type: (-> int int var1) ***\n");
284 fvar1 = binary_function_type(&table, int_type(&table), int_type(&table), var1);
285 i = binary_function_type(&table, int_type(&table), int_type(&table), var1);
286 print_type_table(stdout, &table);
287 printf("\n");
288 printf("----> fvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
289 fvar1, i, type_depth(&table, i));
290 assert(i == fvar1);
291
292 printf("*** Creating function type: (-> var1 var1 unit) ***\n");
293 fvar1 = binary_function_type(&table, var1, var1, unit);
294 i = binary_function_type(&table, var1, var1, unit);
295 print_type_table(stdout, &table);
296 printf("\n");
297 printf("----> fvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
298 fvar1, i, type_depth(&table, i));
299 assert(i == fvar1);
300
301 printf("*** Creating function type: (-> int var1 unit) ***\n");
302 fvar1 = binary_function_type(&table, int_type(&table), var1, unit);
303 i = binary_function_type(&table, int_type(&table), var1, unit);
304 print_type_table(stdout, &table);
305 printf("\n");
306 printf("----> fvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
307 fvar1, i, type_depth(&table, i));
308 assert(i == fvar1);
309
310 printf("*** Creating function type: (-> int var1 enum) ***\n");
311 fvar1 = binary_function_type(&table, int_type(&table), var1, enumtype);
312 i = binary_function_type(&table, int_type(&table), var1, enumtype);
313 print_type_table(stdout, &table);
314 printf("\n");
315 printf("----> fvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
316 fvar1, i, type_depth(&table, i));
317 assert(i == fvar1);
318
319 printf("*** Creating tuple type: (tuple var1 var2) ****\n");
320 tvar = tuple_type_pair(&table, var1, var2);
321 i = tuple_type_pair(&table, var1, var2);
322 print_type_table(stdout, &table);
323 printf("\n");
324 printf("----> tvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
325 tvar, i, type_depth(&table, i));
326 assert(i == tvar);
327
328 printf("*** Creating tuple type: (tuple var2 real) ****\n");
329 tvar = tuple_type_pair(&table, var2, real_type(&table));
330 i = tuple_type_pair(&table, var2, real_type(&table));
331 print_type_table(stdout, &table);
332 printf("\n");
333 printf("----> tvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
334 tvar, i, type_depth(&table, i));
335 assert(i == tvar);
336
337 printf("*** Creating tuple type: (tuple real var2) ****\n");
338 tvar = tuple_type_pair(&table, real_type(&table), var2);
339 i = tuple_type_pair(&table, real_type(&table), var2);
340 print_type_table(stdout, &table);
341 printf("\n");
342 printf("----> tvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
343 tvar, i, type_depth(&table, i));
344 assert(i == tvar);
345
346 printf("*** Creating function type: (-> real real (tuple real var2)) ****\n");
347 fvar1 = binary_function_type(&table, real_type(&table), real_type(&table), tvar);
348 set_type_name(&table, fvar1, clone_string("F0"));
349 i = binary_function_type(&table, real_type(&table), real_type(&table), tvar);
350 print_type_table(stdout, &table);
351 printf("\n");
352 printf("---> fvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
353 fvar1, i, type_depth(&table, i));
354 assert(i == fvar1);
355
356 printf("*** Creating function type: (-> real (tuple real var2) enum) ****\n");
357 fvar1 = binary_function_type(&table, real_type(&table), tvar, enumtype);
358 i = binary_function_type(&table, real_type(&table), tvar, enumtype);
359 print_type_table(stdout, &table);
360 printf("\n");
361 printf("---> fvar = %"PRId32", i = %"PRId32", depth = %"PRIu32"\n\n",
362 fvar1, i, type_depth(&table, i));
363 assert(i == fvar1);
364
365 printf("\n\n*** ALL TYPES ***\n");
366 pp_type_table(stdout, &table);
367 printf("\n\n");
368
369 printf("*** Testing get_by_name ***\n");
370 i = get_type_by_name(&table, "real");
371 printf("---> type-by-name real: %"PRId32"\n", i);
372 assert(i == NULL_TERM);
373 i = get_type_by_name(&table, "R");
374 printf("---> type-by-name R: %"PRId32"\n", i);
375 assert(i == real_id);
376 i = get_type_by_name(&table, "enum");
377 printf("---> type-by-name enum: %"PRId32"\n", i);
378 assert(i == enumtype);
379 i = get_type_by_name(&table, "any");
380 printf("---> type-by-name any: %"PRId32"\n", i);
381 assert(i == any);
382 i = get_type_by_name(&table, "bv32");
383 printf("---> type-by-name bv32: %"PRId32"\n", i);
384 assert(i == bv32);
385 i = get_type_by_name(&table, "int32");
386 printf("---> type-by-name int32: %"PRId32"\n", i);
387 assert(i == bv32);
388 i = get_type_by_name(&table, "ftype");
389 printf("---> type-by-name ftype: %"PRId32"\n", i);
390 assert(i == ft);
391 i = get_type_by_name(&table, "bvxxx2");
392 printf("---> type-by-name bvxxx2: %"PRId32"\n", i);
393 assert(i == NULL_TYPE);
394 printf("\n\n");
395
396 printf("*** Garbage Collection ***\n");
397 type_table_gc(&table, true);
398 print_type_table(stdout, &table);
399 printf("\n");
400
401 printf("*** removing bv32 and int32 ***\n");
402 remove_type_name(&table, "bv32");
403 i = get_type_by_name(&table, "bv32");
404 printf("---> type-by-name bv32: %"PRId32"\n", i);
405 assert(i == NULL_TYPE);
406 remove_type_name(&table, "int32");
407 i = get_type_by_name(&table, "int32");
408 printf("---> type-by-name int32: %"PRId32"\n", i);
409 remove_type_name(&table, "int32");
410 i = get_type_by_name(&table, "int32");
411 printf("---> type-by-name int32: %"PRId32"\n\n", i);
412 assert(i == NULL_TYPE);
413 print_type_table(stdout, &table);
414 printf("\n");
415
416 printf("*** Garbage Collection ***\n");
417 type_table_gc(&table, true);
418 print_type_table(stdout, &table);
419 printf("\n");
420
421 printf("*** Creating pair type ***\n");
422 tt = tuple_type_pair(&table, any, enumtype);
423 i = tuple_type_pair(&table, any, enumtype);
424 printf("---> tt: %"PRId32", i: %"PRId32", depth = %"PRIu32"\n\n",
425 tt, i, type_depth(&table, i));
426 assert(i == tt);
427 print_type_table(stdout, &table);
428 printf("\n");
429
430 printf("*** Creating triplets ***\n");
431 tt = tuple_type_triple(&table, any, int_type(&table), tt);
432 i = tuple_type_triple(&table, bv_type(&table, 24), int_type(&table), tt);
433 printf("---> tt: %"PRId32", i: %"PRId32"\n", tt, i);
434 printf("---> depth(tt) = %"PRIu32"\n", type_depth(&table, tt));
435 printf("---> depth(i) = %"PRIu32"\n\n", type_depth(&table, i));
436 print_type_table(stdout, &table);
437 printf("\n");
438
439 // Check hash consing
440 i = tuple_type_triple(&table, bv_type(&table, 24), int_type(&table),
441 tuple_type_triple(&table, any, int_type(&table),
442 tuple_type_pair(&table, any, enumtype)));
443 printf("\n---> (tuple (bv 24) int (tuple any int (tuple any enum))): %"PRId32"\n", i);
444 printf("---> depth = %"PRIu32"\n\n", type_depth(&table, i));
445 print_type_table(stdout, &table);
446 printf("\n");
447
448 // mark last type i:
449 type_table_set_gc_mark(&table, i);
450 printf("*** Garbage Collection (marked tau!%"PRId32") ***\n", i);
451 type_table_gc(&table, true);
452 print_type_table(stdout, &table);
453 printf("\n");
454
455 // mark tt
456 type_table_set_gc_mark(&table, tt);
457 printf("*** Garbage Collection (marked tau!%"PRId32") ***\n", tt);
458 type_table_gc(&table, true);
459 print_type_table(stdout, &table);
460 printf("\n");
461
462 delete_type_table(&table);
463
464
465 printf("\n*** New Table ***\n");
466 init_type_table(&table, 20);
467 print_type_table(stdout, &table);
468 printf("\n");
469
470 printf("*** Creating bv10 and bv32 ***\n");
471 bv10 = bv_type(&table, 10);
472 i = bv_type(&table, 10);
473 printf("---> bv10: %"PRId32", i: %"PRId32"\n", bv10, i);
474 assert(i == bv10);
475 bv32 = bv_type(&table, 32);
476 set_type_name(&table, bv32, clone_string("bv32"));
477 set_type_name(&table, bv32, clone_string("int32"));
478 i = bv_type(&table, 32);
479 printf("---> bv32: %"PRId32", i: %"PRId32"\n\n", bv32, i);
480 print_type_table(stdout, &table);
481 printf("\n");
482
483 printf("*** Creating any (uninterpreted) ***\n");
484 any = new_uninterpreted_type(&table);
485 set_type_name(&table, any, clone_string("any"));
486 printf("---> any: %"PRId32"\n\n", any);
487 print_type_table(stdout, &table);
488 printf("\n");
489
490 printf("\n*** END ***\n");
491 print_type_table(stdout, &table);
492 printf("\n");
493 print_symbol_table(stdout, &table.stbl, 10);
494 printf("\n");
495 print_int_hash_table(stdout, &table.htbl, 10);
496 printf("\n\n");
497
498 delete_type_table(&table);
499
500
501 return 0;
502 }
503