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 * UTILITIES: ACCESS TO INTERNAL EGRAPH STRUCTURES
21 */
22
23 #include "solvers/egraph/egraph_utils.h"
24 #include "utils/int_hash_map.h"
25
26 /*
27 * Allocate and initialize the internal imap
28 */
egraph_alloc_imap(egraph_t * egraph)29 void egraph_alloc_imap(egraph_t *egraph) {
30 assert(egraph->imap == NULL);
31 egraph->imap = (int_hmap_t *) safe_malloc(sizeof(int_hmap_t));
32 init_int_hmap(egraph->imap, 0);
33 }
34
35
36
37
38 /*
39 * SUPPORT FOR GARBAGE COLLECTOR
40 */
41
42 /*
43 * Mark all types present in eterm table
44 * - types = the relevant type table
45 */
eterm_table_gc_mark(eterm_table_t * tbl,type_table_t * types)46 static void eterm_table_gc_mark(eterm_table_t *tbl, type_table_t *types) {
47 uint32_t i, n;
48 type_t tau;
49
50 n = tbl->nterms;
51 for (i=0; i<n; i++) {
52 tau = tbl->real_type[i];
53 if (tau != NULL_TYPE) { // not sure this test is necessary
54 type_table_set_gc_mark(types, tau);
55 }
56 }
57 }
58
59 /*
60 * Mark all types present in lambda tag table
61 * - types = relevant type table
62 */
ltag_table_gc_mark(ltag_table_t * tbl,type_table_t * types)63 static void ltag_table_gc_mark(ltag_table_t *tbl, type_table_t *types) {
64 ltag_desc_t *d;
65 uint32_t i, ntags;
66 uint32_t j ,n;
67
68 ntags = tbl->ntags;
69 for (i=0; i<ntags; i++) {
70 d = tbl->data[i];
71 n = d->arity;
72 for (j=0; j<n; j++) {
73 type_table_set_gc_mark(types, d->dom[j]);
74 }
75 }
76 }
77
78 /*
79 * Mark all types used by egraph to preserve them from deletion on
80 * the next call to type_table_gc.
81 *
82 * Marked types include:
83 * - any type tau that occurs in egraph->terms.real_type[i]
84 * - all types that occur in egraph->tag_table.
85 */
egraph_gc_mark(egraph_t * egraph)86 void egraph_gc_mark(egraph_t *egraph) {
87 eterm_table_gc_mark(&egraph->terms, egraph->types);
88 ltag_table_gc_mark(&egraph->tag_table, egraph->types);
89 }
90
91