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 * MODELS
21 */
22
23 /*
24 * A model is a (partial) map from terms to concrete values.
25 *
26 * The terms in this map's domain should be uninterpreted constant,
27 * functions, or predicates. That should be enough for computing the
28 * value of any other term.
29 *
30 * Added 06/10/2009: A model can also store a substitution table
31 * (i.e. a mapping from uninterpreted terms to terms.) This allows us
32 * to keep track of the variable substitutions performed during
33 * internalization (cf. context.h).
34 */
35
36
37 #ifndef __MODELS_H
38 #define __MODELS_H
39
40 #include <stdint.h>
41
42 #include "model/concrete_values.h"
43 #include "terms/terms.h"
44 #include "utils/int_hash_map.h"
45
46 #include "yices_types.h"
47
48
49 /*
50 * Model structure:
51 * - vtbl = table where the concrete values are constructed
52 * - map = hash map for storing the map from terms to concrete
53 * values (fixed part of the model)
54 * - alias_map = hash map for storing the substitution table
55 * (it's allocated on demand).
56 * - terms = term table where all terms are stored
57 * - has_alias: flag true if the model is intended to support
58 * the internal substitution table (alias_map). (NOTE: has_alias
59 * is set at construction time and it may be true even if alias_map is NULL).
60 */
61 struct model_s {
62 value_table_t vtbl;
63 int_hmap_t map;
64 int_hmap_t *alias_map;
65 term_table_t *terms;
66 bool has_alias;
67 };
68
69
70 /*
71 * Initialize model
72 * - terms = attached term table
73 * - keep_subst = whether to support alias_map or not
74 * - map and vtbl are given default sizes
75 * - alias_map is NULL
76 */
77 extern void init_model(model_t *model, term_table_t *terms, bool keep_subst);
78
79
80 /*
81 * Delete model
82 * - free all internal memory
83 */
84 extern void delete_model(model_t *model);
85
86
87 /*
88 * Get the internal vtbl
89 */
model_get_vtbl(model_t * model)90 static inline value_table_t *model_get_vtbl(model_t *model) {
91 return &model->vtbl;
92 }
93
94 /*
95 * Find the value of term t in model
96 * - t must be a valid term index (null_term is not allowed here)
97 * - return null_value if t is not mapped to anything
98 * - return the concrete object mapped to t otherwise
99 */
100 extern value_t model_find_term_value(model_t *model, term_t t);
101
102
103 /*
104 * Check whether t is mapped to a term v in the substitution table.
105 * - return v if it is
106 * - return NULL_TERM otherwise
107 * - model->has_alias must be true
108 */
109 extern term_t model_find_term_substitution(model_t *model, term_t t);
110
111
112 /*
113 * Store the mapping t := v in model
114 * - t must be a valid term index (not null_term)
115 * - t must not be mapped to anything
116 * - v must be a valid object created in model->vtbl.
117 *
118 * If v is a function object and it has no name, then t's name is
119 * given to v.
120 */
121 extern void model_map_term(model_t *model, term_t t, value_t v);
122
123
124 /*
125 * Store the substitution t --> u in the model
126 * - t and u must be valid term indices
127 * - t must be an uninterpreted term, not mapped to anything
128 * - model->has_alias must be true
129 */
130 extern void model_add_substitution(model_t *model, term_t t, term_t u);
131
132
133 /*
134 * Iteration: call f(aux, t) for every term t stored in the model
135 * - this includes every t in model->map (term mapped to a value)
136 * - if all is true, then the iterator is also applied to every t in
137 * the domain of model->alias (term mapped to another term)
138 * - f must not have side effects on model
139 */
140 typedef void (*model_iterator_t)(void *aux, term_t t);
141
142 extern void model_term_iterate(model_t *model, bool all, void *aux, model_iterator_t f);
143
144
145 /*
146 * Term collector: call f(aux, t) for every term t that's stored in the model
147 * - if f(aux, t) returns true, add t to vector v
148 * - if all is false, only the terms in model->map are considered
149 * - if all is true, the terms in model->map and model->alias are considered
150 * - f must not have side effects
151 *
152 * NOTE: v is not reset. All terms collected are added to v
153 */
154 typedef bool (*model_filter_t)(void *aux, term_t t);
155
156 extern void model_collect_terms(model_t *model, bool all, void *aux, model_filter_t f, ivector_t *v);
157
158
159 /*
160 * Prepare for garbage collection: mark all the terms present in model
161 * - all marked terms will be considered as roots on the next call
162 * to term_table_gc
163 */
164 extern void model_gc_mark(model_t *model);
165
166
167 #endif /* __MODELS_H */
168