1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 /*------------------------------------------------------------------------*/
10 #ifndef NDEBUG
11 /*------------------------------------------------------------------------*/
12
13 #include "btordbg.h"
14
15 #include <limits.h>
16 #include "btorlog.h"
17 #include "utils/btorhashptr.h"
18 #include "utils/btorutil.h"
19
20 /*------------------------------------------------------------------------*/
21 /* core */
22 /*------------------------------------------------------------------------*/
23
24 bool
btor_dbg_check_lambdas_static_rho_proxy_free(const Btor * btor)25 btor_dbg_check_lambdas_static_rho_proxy_free (const Btor *btor)
26 {
27 BtorNode *cur, *data, *key;
28 BtorPtrHashTableIterator it, iit;
29 BtorPtrHashTable *static_rho;
30
31 btor_iter_hashptr_init (&it, btor->lambdas);
32 while (btor_iter_hashptr_has_next (&it))
33 {
34 cur = btor_iter_hashptr_next (&it);
35 static_rho = btor_node_lambda_get_static_rho (cur);
36 if (!static_rho) continue;
37
38 btor_iter_hashptr_init (&iit, static_rho);
39 while (btor_iter_hashptr_has_next (&iit))
40 {
41 data = iit.bucket->data.as_ptr;
42 key = btor_iter_hashptr_next (&iit);
43 assert (data);
44 if (btor_node_is_proxy (data)) return false;
45 if (btor_node_is_proxy (key)) return false;
46 }
47 }
48 return true;
49 }
50
51 bool
btor_dbg_check_unique_table_children_proxy_free(const Btor * btor)52 btor_dbg_check_unique_table_children_proxy_free (const Btor *btor)
53 {
54 uint32_t i, j;
55 BtorNode *cur;
56
57 for (i = 0; i < btor->nodes_unique_table.size; i++)
58 for (cur = btor->nodes_unique_table.chains[i]; cur; cur = cur->next)
59 for (j = 0; j < cur->arity; j++)
60 if (btor_node_is_proxy (cur->e[j]))
61 {
62 BTORLOG (1,
63 "found proxy node in unique table: %s (parent: %s)",
64 btor_util_node2string (cur->e[j]),
65 btor_util_node2string (cur));
66 return false;
67 }
68 return true;
69 }
70
71 bool
btor_dbg_check_hash_table_proxy_free(BtorPtrHashTable * table)72 btor_dbg_check_hash_table_proxy_free (BtorPtrHashTable *table)
73 {
74 BtorPtrHashTableIterator it;
75 BtorNode *cur;
76
77 btor_iter_hashptr_init (&it, table);
78 while (btor_iter_hashptr_has_next (&it))
79 {
80 cur = btor_iter_hashptr_next (&it);
81 if (btor_node_is_proxy (cur)) return false;
82 }
83 return true;
84 }
85
86 bool
btor_dbg_check_all_hash_tables_proxy_free(const Btor * btor)87 btor_dbg_check_all_hash_tables_proxy_free (const Btor *btor)
88 {
89 if (!btor_dbg_check_hash_table_proxy_free (btor->embedded_constraints))
90 return false;
91 if (!btor_dbg_check_hash_table_proxy_free (btor->unsynthesized_constraints))
92 return false;
93 if (!btor_dbg_check_hash_table_proxy_free (btor->synthesized_constraints))
94 return false;
95 return true;
96 }
97
98 bool
btor_dbg_check_hash_table_simp_free(BtorPtrHashTable * table)99 btor_dbg_check_hash_table_simp_free (BtorPtrHashTable *table)
100 {
101 BtorPtrHashTableIterator it;
102 btor_iter_hashptr_init (&it, table);
103 while (btor_iter_hashptr_has_next (&it))
104 if (btor_node_is_simplified (btor_iter_hashptr_next (&it)))
105 return false;
106 return true;
107 }
108
109 bool
btor_dbg_check_unique_table_rebuild(const Btor * btor)110 btor_dbg_check_unique_table_rebuild (const Btor *btor)
111 {
112 uint32_t i;
113 BtorNode *cur;
114
115 for (i = 0; i < btor->nodes_unique_table.size; i++)
116 for (cur = btor->nodes_unique_table.chains[i]; cur; cur = cur->next)
117 {
118 if (cur->rebuild)
119 {
120 BTORLOG (1,
121 "found node with rebuild flag enabled: %s",
122 btor_util_node2string (cur));
123 return false;
124 }
125 }
126 return true;
127 }
128
129 bool
btor_dbg_check_all_hash_tables_simp_free(const Btor * btor)130 btor_dbg_check_all_hash_tables_simp_free (const Btor *btor)
131 {
132 if (!btor_dbg_check_hash_table_simp_free (btor->embedded_constraints))
133 return false;
134 if (!btor_dbg_check_hash_table_simp_free (btor->unsynthesized_constraints))
135 return false;
136 if (!btor_dbg_check_hash_table_simp_free (btor->synthesized_constraints))
137 return false;
138 return true;
139 }
140
141 bool
btor_dbg_check_constraints_not_const(const Btor * btor)142 btor_dbg_check_constraints_not_const (const Btor *btor)
143 {
144 BtorNode *cur;
145 BtorPtrHashTableIterator it;
146
147 btor_iter_hashptr_init (&it, btor->unsynthesized_constraints);
148 while (btor_iter_hashptr_has_next (&it))
149 {
150 cur = btor_iter_hashptr_next (&it);
151 assert (cur);
152 if (btor_node_is_bv_const (cur)) return false;
153 }
154
155 btor_iter_hashptr_init (&it, btor->synthesized_constraints);
156 while (btor_iter_hashptr_has_next (&it))
157 {
158 cur = btor_iter_hashptr_next (&it);
159 assert (cur);
160 if (btor_node_is_bv_const (cur)) return false;
161 }
162 return true;
163 }
164
165 bool
btor_dbg_check_assumptions_simp_free(const Btor * btor)166 btor_dbg_check_assumptions_simp_free (const Btor *btor)
167 {
168 BtorPtrHashTableIterator it;
169 btor_iter_hashptr_init (&it, btor->assumptions);
170 while (btor_iter_hashptr_has_next (&it))
171 if (btor_node_is_simplified (btor_iter_hashptr_next (&it)))
172 return false;
173 return true;
174 }
175
176 bool
btor_dbg_check_nodes_simp_free(Btor * btor,BtorNode * nodes[],size_t nnodes)177 btor_dbg_check_nodes_simp_free (Btor *btor, BtorNode *nodes[], size_t nnodes)
178 {
179 size_t i;
180 int32_t id;
181 BtorNode *cur;
182 BtorPtrHashTableIterator it;
183 BtorIntHashTable *cache;
184 BtorPtrHashTable *rho;
185 BtorNodePtrStack visit;
186 bool opt_nondestr_subst;
187
188 BTOR_INIT_STACK (btor->mm, visit);
189 cache = btor_hashint_table_new (btor->mm);
190 opt_nondestr_subst = btor_opt_get (btor, BTOR_OPT_NONDESTR_SUBST) == 1;
191
192 for (i = 0; i < nnodes; i++)
193 {
194 BTOR_PUSH_STACK (visit, nodes[i]);
195 BTORLOG (3, " root: %s", btor_util_node2string (nodes[i]));
196 }
197
198 while (!BTOR_EMPTY_STACK (visit))
199 {
200 cur = btor_node_real_addr (BTOR_POP_STACK (visit));
201 id = btor_node_get_id (cur);
202 BTORLOG (3, "check simp free: %s", btor_util_node2string (cur));
203 if (opt_nondestr_subst && btor_node_is_synth (cur))
204 {
205 continue;
206 }
207 if (btor_node_is_simplified (cur))
208 {
209 BTORLOG (3,
210 " simplified: %s",
211 btor_util_node2string (btor_node_get_simplified (btor, cur)));
212 }
213 assert (!btor_node_is_simplified (cur));
214
215 if (btor_hashint_table_contains (cache, id)) continue;
216
217 if (btor_node_is_lambda (cur)
218 && (rho = btor_node_lambda_get_static_rho (cur)))
219 {
220 btor_iter_hashptr_init (&it, rho);
221 while (btor_iter_hashptr_has_next (&it))
222 {
223 BTOR_PUSH_STACK (visit, it.bucket->data.as_ptr);
224 BTOR_PUSH_STACK (visit, btor_iter_hashptr_next (&it));
225 }
226 }
227
228 btor_hashint_table_add (cache, id);
229 for (i = 0; i < cur->arity; i++)
230 {
231 BTOR_PUSH_STACK (visit, cur->e[i]);
232 }
233 }
234
235 BTOR_RELEASE_STACK (visit);
236 btor_hashint_table_delete (cache);
237 return true;
238 }
239
240 bool
btor_dbg_check_constraints_simp_free(Btor * btor)241 btor_dbg_check_constraints_simp_free (Btor *btor)
242 {
243 BtorNode *cur;
244 BtorNodePtrStack nodes;
245 BtorPtrHashTableIterator it;
246
247 BTOR_INIT_STACK (btor->mm, nodes);
248
249 btor_iter_hashptr_init (&it, btor->unsynthesized_constraints);
250 btor_iter_hashptr_queue (&it, btor->synthesized_constraints);
251 btor_iter_hashptr_queue (&it, btor->assumptions);
252 while (btor_iter_hashptr_has_next (&it))
253 {
254 cur = btor_iter_hashptr_next (&it);
255 BTOR_PUSH_STACK (nodes, cur);
256 }
257
258 btor_dbg_check_nodes_simp_free (btor, nodes.start, BTOR_COUNT_STACK (nodes));
259 BTOR_RELEASE_STACK (nodes);
260 return true;
261 }
262
263 /*------------------------------------------------------------------------*/
264 /* exp */
265 /*------------------------------------------------------------------------*/
266
267 bool
btor_dbg_precond_slice_exp(Btor * btor,const BtorNode * exp,uint32_t upper,uint32_t lower)268 btor_dbg_precond_slice_exp (Btor *btor,
269 const BtorNode *exp,
270 uint32_t upper,
271 uint32_t lower)
272 {
273 assert (btor);
274 assert (exp);
275 assert (!btor_node_is_simplified (exp));
276 assert (!btor_node_is_fun (exp));
277 assert (upper >= lower);
278 assert (upper < btor_node_bv_get_width (btor, exp));
279 assert (btor_node_real_addr (exp)->btor == btor);
280 return true;
281 }
282
283 bool
btor_dbg_precond_ext_exp(Btor * btor,const BtorNode * exp)284 btor_dbg_precond_ext_exp (Btor *btor, const BtorNode *exp)
285 {
286 assert (btor_dbg_precond_regular_unary_bv_exp (btor, exp));
287 return true;
288 }
289
290 bool
btor_dbg_precond_regular_unary_bv_exp(Btor * btor,const BtorNode * exp)291 btor_dbg_precond_regular_unary_bv_exp (Btor *btor, const BtorNode *exp)
292 {
293 assert (btor);
294 assert (exp);
295 assert (!btor_node_is_simplified (exp));
296 assert (!btor_node_is_fun (exp));
297 assert (btor_node_real_addr (exp)->btor == btor);
298 return true;
299 }
300
301 bool
btor_dbg_precond_eq_exp(Btor * btor,const BtorNode * e0,const BtorNode * e1)302 btor_dbg_precond_eq_exp (Btor *btor, const BtorNode *e0, const BtorNode *e1)
303 {
304 BtorNode *real_e0, *real_e1;
305
306 assert (btor);
307 assert (e0);
308 assert (e1);
309
310 real_e0 = btor_node_real_addr (e0);
311 real_e1 = btor_node_real_addr (e1);
312
313 assert (real_e0);
314 assert (real_e1);
315 assert (real_e0->btor == btor);
316 assert (real_e1->btor == btor);
317 assert (!btor_node_is_simplified (real_e0));
318 assert (!btor_node_is_simplified (real_e1));
319 assert (btor_node_get_sort_id (real_e0) == btor_node_get_sort_id (real_e1));
320 assert (real_e0->is_array == real_e1->is_array);
321 assert (!btor_node_is_fun (real_e0)
322 || (btor_node_is_regular (e0) && btor_node_is_regular (e1)));
323 return true;
324 }
325
326 bool
btor_dbg_precond_concat_exp(Btor * btor,const BtorNode * e0,const BtorNode * e1)327 btor_dbg_precond_concat_exp (Btor *btor, const BtorNode *e0, const BtorNode *e1)
328 {
329 assert (btor);
330 assert (e0);
331 assert (e1);
332 assert (!btor_node_is_simplified (e0));
333 assert (!btor_node_is_simplified (e1));
334 assert (!btor_node_is_fun (e0));
335 assert (!btor_node_is_fun (e1));
336 assert (btor_node_bv_get_width (btor, e0)
337 <= INT32_MAX - btor_node_bv_get_width (btor, e1));
338 assert (btor_node_real_addr (e0)->btor == btor);
339 assert (btor_node_real_addr (e1)->btor == btor);
340 return true;
341 }
342
343 bool
btor_dbg_precond_shift_exp(Btor * btor,const BtorNode * e0,const BtorNode * e1)344 btor_dbg_precond_shift_exp (Btor *btor, const BtorNode *e0, const BtorNode *e1)
345 {
346 assert (btor);
347 assert (e0);
348 assert (e1);
349 assert (!btor_node_is_simplified (e0));
350 assert (!btor_node_is_simplified (e1));
351 assert (!btor_node_is_fun (e0));
352 assert (!btor_node_is_fun (e1));
353 assert (btor_node_bv_get_width (btor, e0)
354 == btor_node_bv_get_width (btor, e1));
355 assert (btor_node_real_addr (e0)->btor == btor);
356 assert (btor_node_real_addr (e1)->btor == btor);
357 return true;
358 }
359
360 bool
btor_dbg_precond_regular_binary_bv_exp(Btor * btor,const BtorNode * e0,const BtorNode * e1)361 btor_dbg_precond_regular_binary_bv_exp (Btor *btor,
362 const BtorNode *e0,
363 const BtorNode *e1)
364 {
365 assert (btor);
366 assert (e0);
367 assert (e1);
368 assert (!btor_node_is_simplified (e0));
369 assert (!btor_node_is_simplified (e1));
370 assert (!btor_node_is_fun (e0));
371 assert (!btor_node_is_fun (e1));
372 assert (btor_node_get_sort_id (e0) == btor_node_get_sort_id (e1));
373 assert (btor_node_real_addr (e0)->btor == btor);
374 assert (btor_node_real_addr (e1)->btor == btor);
375 return true;
376 }
377
378 bool
btor_dbg_precond_read_exp(Btor * btor,const BtorNode * e_array,const BtorNode * e_index)379 btor_dbg_precond_read_exp (Btor *btor,
380 const BtorNode *e_array,
381 const BtorNode *e_index)
382 {
383 assert (btor);
384 assert (e_array);
385 assert (e_index);
386 assert (btor_node_is_regular (e_array));
387 assert (btor_node_is_fun (e_array));
388 assert (!btor_node_is_simplified (e_array));
389 assert (!btor_node_is_simplified (e_index));
390 assert (!btor_node_is_fun (e_index));
391 assert (btor_sort_array_get_index (btor, btor_node_get_sort_id (e_array))
392 == btor_node_get_sort_id (e_index));
393 assert (btor_node_real_addr (e_array)->btor == btor);
394 assert (btor_node_real_addr (e_index)->btor == btor);
395 assert (e_array->is_array);
396 return true;
397 }
398
399 bool
btor_dbg_precond_write_exp(Btor * btor,const BtorNode * e_array,const BtorNode * e_index,const BtorNode * e_value)400 btor_dbg_precond_write_exp (Btor *btor,
401 const BtorNode *e_array,
402 const BtorNode *e_index,
403 const BtorNode *e_value)
404 {
405 assert (btor);
406 assert (e_array);
407 assert (e_index);
408 assert (e_value);
409 assert (btor_node_is_regular (e_array));
410 assert (btor_node_is_fun (e_array));
411 assert (!btor_node_is_simplified (e_array));
412 assert (!btor_node_is_simplified (e_index));
413 assert (!btor_node_is_simplified (e_value));
414 assert (!btor_node_is_fun (e_index));
415 assert (!btor_node_is_fun (e_value));
416 assert (btor_sort_array_get_index (btor, btor_node_get_sort_id (e_array))
417 == btor_node_get_sort_id (e_index));
418 assert (btor_sort_array_get_element (btor, btor_node_get_sort_id (e_array))
419 == btor_node_get_sort_id (e_value));
420 assert (btor_node_real_addr (e_array)->btor == btor);
421 assert (btor_node_real_addr (e_index)->btor == btor);
422 assert (btor_node_real_addr (e_value)->btor == btor);
423 assert (e_array->is_array);
424 return true;
425 }
426
427 bool
btor_dbg_precond_cond_exp(Btor * btor,const BtorNode * e_cond,const BtorNode * e_if,const BtorNode * e_else)428 btor_dbg_precond_cond_exp (Btor *btor,
429 const BtorNode *e_cond,
430 const BtorNode *e_if,
431 const BtorNode *e_else)
432 {
433 assert (btor);
434 assert (e_cond);
435 assert (e_if);
436 assert (e_else);
437 assert (!btor_node_is_simplified (e_cond));
438 assert (btor_node_bv_get_width (btor, e_cond) == 1);
439
440 BtorNode *real_e_if, *real_e_else;
441
442 real_e_if = btor_node_real_addr (e_if);
443 real_e_else = btor_node_real_addr (e_else);
444
445 assert (!btor_node_is_simplified (real_e_if));
446 assert (!btor_node_is_simplified (real_e_else));
447 assert (btor_node_get_sort_id (real_e_if)
448 == btor_node_get_sort_id (real_e_else));
449 assert (btor_node_real_addr (e_cond)->btor == btor);
450 assert (real_e_if->btor == btor);
451 assert (real_e_else->btor == btor);
452 assert (real_e_if->is_array == real_e_else->is_array);
453 return true;
454 }
455
456 bool
btor_dbg_precond_apply_exp(Btor * btor,const BtorNode * fun,const BtorNode * args)457 btor_dbg_precond_apply_exp (Btor *btor,
458 const BtorNode *fun,
459 const BtorNode *args)
460 {
461 assert (btor);
462 assert (fun);
463 assert (args);
464 assert (btor_node_is_regular (fun));
465 assert (btor_node_is_regular (args));
466 assert (btor_node_is_fun (fun));
467 assert (btor_node_is_args (args));
468 assert (btor_sort_fun_get_domain (btor, btor_node_get_sort_id (fun))
469 == btor_node_get_sort_id (args));
470 return true;
471 }
472
473 /*------------------------------------------------------------------------*/
474 #endif
475 /*------------------------------------------------------------------------*/
476