| /dports/math/boolector/boolector-3.2.2/src/preprocess/ |
| H A D | btormerge.c | 50 delete_static_rho (Btor *btor, BtorPtrHashTable *static_rho) in delete_static_rho() argument
54 btor_iter_hashptr_init (&it, static_rho); in delete_static_rho()
60 btor_hashptr_table_delete (static_rho); in delete_static_rho()
95 BtorPtrHashTable *merge_lambdas, *static_rho; in btor_merge_lambdas() local
231 static_rho = btor_hashptr_table_new (mm, in btor_merge_lambdas()
241 btor, static_rho, btor_node_lambda_get_static_rho (cur)); in btor_merge_lambdas()
249 static_rho->count); in btor_merge_lambdas()
252 if (static_rho->count > 0) in btor_merge_lambdas()
264 delete_static_rho (btor, static_rho); in btor_merge_lambdas()
267 btor_node_lambda_set_static_rho (subst, static_rho); in btor_merge_lambdas()
[all …]
|
| H A D | btorextract.c | 1045 BtorPtrHashTable *static_rho; in create_static_rho() local
1048 static_rho = btor_hashptr_table_new (btor->mm, in create_static_rho()
1075 return static_rho; in create_static_rho()
1205 static_rho = create_static_rho ( in extract_lambdas()
1207 i_index_r += static_rho->count + 1; in extract_lambdas()
1273 static_rho = create_static_rho ( in extract_lambdas()
1275 i_index_r += static_rho->count + 1; in extract_lambdas()
1314 static_rho = create_static_rho ( in extract_lambdas()
1316 i_index_r += static_rho->count + 1; in extract_lambdas()
1362 static_rho = create_static_rho ( in extract_lambdas()
[all …]
|
| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btorsubst.c | 60 BtorPtrHashTable *static_rho, *new_static_rho; in update_node_hash_tables() local
67 static_rho = btor_node_lambda_get_static_rho (cur); in update_node_hash_tables()
69 if (!static_rho) continue; in update_node_hash_tables()
76 btor_iter_hashptr_init (&iit, static_rho); in update_node_hash_tables()
93 btor_hashptr_table_delete (static_rho); in update_node_hash_tables()
|
| H A D | btordbg.c | 29 BtorPtrHashTable *static_rho; in btor_dbg_check_lambdas_static_rho_proxy_free() local
35 static_rho = btor_node_lambda_get_static_rho (cur); in btor_dbg_check_lambdas_static_rho_proxy_free()
36 if (!static_rho) continue; in btor_dbg_check_lambdas_static_rho_proxy_free()
38 btor_iter_hashptr_init (&iit, static_rho); in btor_dbg_check_lambdas_static_rho_proxy_free()
|
| H A D | btornode.c | 812 BtorPtrHashTable *static_rho; in erase_local_data_exp() local
833 if (static_rho) in erase_local_data_exp()
841 btor_hashptr_table_delete (static_rho); in erase_local_data_exp()
1323 ((BtorLambdaNode *) lambda)->static_rho = static_rho; in btor_node_lambda_set_static_rho()
1335 BtorPtrHashTable *static_rho; in btor_node_lambda_copy_static_rho() local
1338 static_rho = btor_hashptr_table_new (btor->mm, in btor_node_lambda_copy_static_rho()
1347 return static_rho; in btor_node_lambda_copy_static_rho()
1353 BtorPtrHashTable *static_rho; in btor_node_lambda_delete_static_rho() local
1357 if (!static_rho) return; in btor_node_lambda_delete_static_rho()
1359 btor_iter_hashptr_init (&it, static_rho); in btor_node_lambda_delete_static_rho()
[all …]
|
| H A D | btornode.h | 208 BtorPtrHashTable *static_rho; member
717 BtorPtrHashTable *static_rho);
|
| H A D | btorslvfun.c | 1912 BtorPtrHashTable *table, *rho, *static_rho; in generate_table() local
1944 static_rho = 0; in generate_table()
1950 static_rho = btor_node_lambda_get_static_rho (cur); in generate_table()
1951 assert (!btor_node_real_addr (cur->e[1])->parameterized || static_rho); in generate_table()
1972 if (static_rho) btor_iter_hashptr_queue (&it, static_rho); in generate_table()
1974 else if (static_rho) in generate_table()
1975 btor_iter_hashptr_init (&it, static_rho); in generate_table()
1977 if (rho || static_rho) in generate_table()
|
| H A D | btormodel.c | 278 BtorPtrHashTable *static_rho; in recursively_compute_function_model() local
294 && (static_rho = btor_node_lambda_get_static_rho (cur_fun))) in recursively_compute_function_model()
295 add_rho_to_model (btor, fun, static_rho, bv_model, fun_model); in recursively_compute_function_model()
|
| H A D | btorcore.c | 2483 BtorPtrHashTable *static_rho; in btor_synthesize_exp() local
2585 static_rho = btor_node_lambda_get_static_rho (cur); in btor_synthesize_exp()
2586 if (static_rho) in btor_synthesize_exp()
2588 btor_iter_hashptr_init (&it, static_rho); in btor_synthesize_exp()
|
| H A D | btorexp.c | 1839 if (!lambda->static_rho) in btor_exp_lambda_write()
1841 lambda->static_rho = in btor_exp_lambda_write()
1846 b = btor_hashptr_table_add (lambda->static_rho, args); in btor_exp_lambda_write()
|
| /dports/math/boolector/boolector-3.2.2/src/dumper/ |
| H A D | btordumpsmt.c | 574 BtorPtrHashTable *static_rho; in expand_lambda() local
598 static_rho = btor_node_lambda_get_static_rho (cur); in expand_lambda()
599 assert (static_rho); in expand_lambda()
601 btor_iter_hashptr_init (&it, static_rho); in expand_lambda()
1529 BtorPtrHashTable *static_rho; in dump_smt() local
1580 static_rho = btor_node_lambda_get_static_rho (cur); in dump_smt()
1581 assert (static_rho); in dump_smt()
1583 btor_iter_hashptr_init (&it, static_rho); in dump_smt()
|