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 * PRINT FUNCTION/ARRAY SOLVER STRUCTURES
21 */
22
23 #include <inttypes.h>
24
25 #include "io/type_printer.h"
26 #include "solvers/egraph/egraph_printer.h"
27 #include "solvers/funs/fun_solver_printer.h"
28 #include "utils/pointer_vectors.h"
29
30
31
32 /*
33 * Print edge i
34 */
print_fsolver_edge(FILE * f,fun_solver_t * solver,uint32_t edge_id)35 void print_fsolver_edge(FILE *f, fun_solver_t *solver, uint32_t edge_id) {
36 fun_edgetable_t *etbl;
37 fun_edge_t *e;
38 uint32_t i, n;
39
40 etbl = &solver->etbl;
41 assert(0 <= edge_id && edge_id < etbl->nedges);
42 e = etbl->data[edge_id];
43
44 fprintf(f, "edge[%"PRIu32"] : f!%"PRIu32" ---> f!%"PRIu32" [", edge_id, e->source, e->target);
45 n = solver->vtbl.arity[e->source];
46 assert(solver->vtbl.arity[e->target] == n);
47 for (i=0; i<n; i++) {
48 if (i>0) {
49 fputc(' ', f);
50 }
51 print_occurrence(f, e->index[i]);
52 }
53 fprintf(f, "]");
54 }
55
56
57 /*
58 * Print the edges
59 */
print_fsolver_edges(FILE * f,fun_solver_t * solver)60 void print_fsolver_edges(FILE *f, fun_solver_t *solver) {
61 uint32_t i, n;
62
63 n = solver->etbl.nedges;
64 for (i=0; i<n; i++) {
65 print_fsolver_edge(f, solver, i);
66 fputc('\n', f);
67 }
68 fflush(f);
69 }
70
71
72 /*
73 * Print the variables
74 */
print_fsolver_vars(FILE * f,fun_solver_t * solver)75 void print_fsolver_vars(FILE *f, fun_solver_t *solver) {
76 fun_vartable_t *vtbl;
77 uint32_t i, n;
78
79 vtbl = &solver->vtbl;
80 n = vtbl->nvars;
81 for (i=0; i<n; i++) {
82 fprintf(f, "var f!%"PRId32": eterm = ", i);
83 print_eterm_id(f, vtbl->eterm[i]);
84 if (tst_bit(vtbl->fdom, i)) {
85 fprintf(f, ", finite domain");
86 }
87 fprintf(f, ", type: ");
88 print_type_def(f, solver->types, vtbl->type[i]);
89 fprintf(f, "\n");
90 }
91 fflush(f);
92 }
93
94
95 /*
96 * Print the root variables
97 */
print_fsolver_roots(FILE * f,fun_solver_t * solver)98 void print_fsolver_roots(FILE *f, fun_solver_t *solver) {
99 fun_vartable_t *vtbl;
100 uint32_t i, n;
101
102 vtbl = &solver->vtbl;
103 n = vtbl->nvars;
104 for (i=0; i<n; i++) {
105 fprintf(f, "root[f!%"PRIu32"] = f!%"PRIu32", eterm[f!%"PRIu32"] = ", i, vtbl->root[i], i);
106 print_eterm_id(f, vtbl->eterm[i]);
107 fputc('\n', f);
108 }
109 fflush(f);
110 }
111
112
113 /*
114 * Print the equivalence classes
115 */
print_fsolver_classes(FILE * f,fun_solver_t * solver)116 void print_fsolver_classes(FILE *f, fun_solver_t *solver) {
117 fun_vartable_t *vtbl;
118 uint32_t i, n;
119 thvar_t x;
120
121 vtbl = &solver->vtbl;
122 n = vtbl->nvars;
123 for (i=0; i<n; i++) {
124 if (vtbl->root[i] == i) {
125 // i is a root:
126 fprintf(f, "class of f!%"PRIu32" = {", i);
127 x = i;
128 do {
129 fprintf(f, " f!%"PRId32, x);
130 x = vtbl->next[x];
131 } while (x != null_thvar);
132 fprintf(f, " }\n");
133 }
134 }
135 }
136
137
138 /*
139 * Print the application vectors
140 */
print_fsolver_apps(FILE * f,fun_solver_t * solver)141 void print_fsolver_apps(FILE *f, fun_solver_t *solver) {
142 fun_vartable_t *vtbl;
143 composite_t **p;
144 uint32_t i, n, j, m;
145
146 vtbl = &solver->vtbl;
147 n = vtbl->nvars;
148 for (i=0; i<n; i++) {
149 if (vtbl->root[i] == i) {
150 p = (composite_t **) vtbl->app[i];
151 if (p != NULL) {
152 fprintf(f, "--- Apps for f!%"PRIu32" ---\n", i);
153 m = pv_size((void **) p);
154 for (j=0; j<m; j++) {
155 print_composite(f, p[j]);
156 fputs(" == ", f);
157 print_label(f, egraph_term_label(solver->egraph, p[j]->id));
158 fputc('\n', f);
159 }
160 } else {
161 fprintf(f, "--- No apps for f!%"PRIu32" ---\n", i);
162 }
163 }
164 }
165 fflush(f);
166 }
167
168
169
170 /*
171 * Print (f i_1 ... i_n) as a map element
172 */
print_map(FILE * f,egraph_t * egraph,composite_t * c)173 static void print_map(FILE *f, egraph_t *egraph, composite_t *c) {
174 uint32_t i, n;
175
176 assert(composite_kind(c) == COMPOSITE_APPLY);
177
178 n = composite_arity(c);
179 fputc('[', f);
180 for (i=1; i<n; i++) {
181 print_label(f, egraph_label(egraph, composite_child(c, i)));
182 fputc(' ', f);
183 }
184 fputs("|-> ", f);
185 print_label(f, egraph_term_label(egraph, c->id));
186 fputs("]\n", f);
187 }
188
189
190 /*
191 * Print the application vectors + base labels
192 * - formatted as a mapping form egraph labels to egraph labels
193 */
print_fsolver_maps(FILE * f,fun_solver_t * solver)194 void print_fsolver_maps(FILE *f, fun_solver_t *solver) {
195 fun_vartable_t *vtbl;
196 egraph_t *egraph;
197 composite_t **p;
198 uint32_t i, n, j, m;
199
200 egraph = solver->egraph;
201 vtbl = &solver->vtbl;
202 n = vtbl->nvars;
203 for (i=0; i<n; i++) {
204 if (vtbl->root[i] == i) {
205 fprintf(f, "--- Map for f!%"PRIu32" ---\n", i);
206 fprintf(f, "base = %"PRId32"\n", vtbl->base[i]);
207 p = (composite_t **) vtbl->app[i];
208 if (p != NULL) {
209 m = pv_size((void **) p);
210 for (j=0; j<m; j++) {
211 print_map(f, egraph, p[j]);
212 }
213 }
214 }
215 }
216
217 }
218
219
220 /*
221 * Print the base values for every root variable
222 */
print_fsolver_base_values(FILE * f,fun_solver_t * solver)223 void print_fsolver_base_values(FILE *f, fun_solver_t *solver) {
224 fun_vartable_t *vtbl;
225 uint32_t i, n;
226 int32_t c, k;
227
228 if (solver->base_value == NULL) {
229 fputs("no base values\n", f);
230 return;
231 }
232
233 vtbl = &solver->vtbl;
234 n = vtbl->nvars;
235 for (i=0; i<n; i++) {
236 if (vtbl->root[i] == i) {
237 c = vtbl->base[i];
238 k = solver->base_value[c];
239 fprintf(f, "base value for f!%"PRIu32": ", i);
240 if (k < 0) {
241 fprintf(f, "fresh(%"PRId32")\n", - (k + 1));
242 } else if (k == INT32_MAX) {
243 fputs("unknown\n", f);
244 } else {
245 print_label(f, k);
246 fputc('\n', f);
247 }
248 }
249 }
250 }
251
252
253
254 /*
255 * Print particle x as an index
256 */
print_particle_index(FILE * f,egraph_t * egraph,particle_t x)257 static void print_particle_index(FILE *f, egraph_t *egraph, particle_t x) {
258 pstore_t *store;
259 particle_tuple_t *tup;
260 uint32_t i, n;
261
262 store = egraph->mdl.pstore;
263 switch (particle_kind(store, x)) {
264 case LABEL_PARTICLE:
265 print_label(f, particle_label(store, x));
266 break;
267 case FRESH_PARTICLE:
268 fprintf(f, "fresh!%"PRId32, x);
269 break;
270 case TUPLE_PARTICLE:
271 tup = tuple_particle_desc(store, x);
272 n = tup->nelems;
273 for (i=0; i<n; i++) {
274 if (i>0) fputc(' ', f);
275 print_particle_index(f, egraph, tup->elem[i]);
276 }
277 break;
278 }
279 }
280
281 /*
282 * Print particle x as a value
283 */
print_particle_value(FILE * f,egraph_t * egraph,particle_t x)284 static void print_particle_value(FILE *f, egraph_t *egraph, particle_t x) {
285 pstore_t *store;
286 particle_tuple_t *tup;
287 uint32_t i, n;
288
289 store = egraph->mdl.pstore;
290 switch (particle_kind(store, x)) {
291 case LABEL_PARTICLE:
292 print_label(f, particle_label(store, x));
293 break;
294 case FRESH_PARTICLE:
295 fprintf(f, "fresh!%"PRId32, x);
296 break;
297 case TUPLE_PARTICLE:
298 tup = tuple_particle_desc(store, x);
299 n = tup->nelems;
300 fputs("(tuple", f);
301 for (i=0; i<n; i++) {
302 fputc(' ', f);
303 print_particle_value(f, egraph, tup->elem[i]);
304 }
305 fputc(')', f);
306 break;
307 }
308 }
309
310 /*
311 * Print the mapping [idx -> value]
312 */
print_map_elem(FILE * f,egraph_t * egraph,particle_t idx,particle_t val)313 static void print_map_elem(FILE *f, egraph_t *egraph, particle_t idx, particle_t val) {
314 fputc('[', f);
315 print_particle_index(f, egraph, idx);
316 fputs(" -> ", f);
317 print_particle_value(f, egraph, val);
318 fputs("]\n", f);
319 }
320
321
322 /*
323 * Print the values
324 */
print_fsolver_values(FILE * f,fun_solver_t * solver)325 void print_fsolver_values(FILE *f, fun_solver_t *solver) {
326 fun_vartable_t *vtbl;
327 egraph_t *egraph;
328 map_t *map;
329 uint32_t i, n, j;
330
331 egraph = solver->egraph;
332 vtbl = &solver->vtbl;
333 n = vtbl->nvars;
334 for (i=0; i<n; i++) {
335 if (vtbl->root[i] == i) {
336 fprintf(f, "--- Value for f!%"PRIu32" ---\n", i);
337 map = solver->value[i];
338 if (map != NULL) {
339 for (j=0; j<map->nelems; j++) {
340 print_map_elem(f, egraph, map->data[j].index, map->data[j].value);
341 }
342 if (map->def != null_particle) {
343 fputs("[else -> ", f);
344 print_particle_value(f, egraph, map->def);
345 fputs("]\n", f);
346 }
347 }
348 }
349 }
350
351 }
352
353
354 /*
355 * Print the asserted disequalities
356 */
print_fsolver_diseqs(FILE * f,fun_solver_t * solver)357 void print_fsolver_diseqs(FILE *f, fun_solver_t *solver) {
358 diseq_stack_t *dstack;
359 uint32_t i, n;
360
361 dstack = &solver->dstack;
362 n = dstack->top;
363 for (i=0; i<n; i++) {
364 fprintf(f, "diseq[%"PRIu32"]: f!%"PRIu32" != f%"PRIu32"\n", i, dstack->data[i].left, dstack->data[i].right);
365 }
366
367 }
368
369
370