Searched refs:btor_sort_is_bv (Results 1 – 8 of 8) sorted by relevance
| /dports/math/boolector/boolector-3.2.2/src/ |
| H A D | btorabort.h | 73 BTOR_ABORT (!btor_sort_is_bv (btor, btor_node_get_sort_id (arg)), \
|
| H A D | btorsort.h | 153 bool btor_sort_is_bv (Btor *btor, BtorSortId id);
|
| H A D | boolector.c | 1244 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_constd()
1278 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_consth()
1406 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_zero()
1427 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_ones()
1448 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_one()
1509 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_unsigned_int()
1530 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_int()
1601 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_var()
3148 BTOR_ABORT (!btor_sort_is_bv (btor, s), in boolector_param()
4502 BTOR_ABORT (!btor_sort_is_bv (btor, is), in boolector_array_sort()
[all …]
|
| H A D | btorexp.c | 127 assert (btor_sort_is_bv (btor, btor_node_get_sort_id (value))); in btor_exp_const_array()
289 assert (btor_sort_is_bv (btor, sort)); in btor_exp_bv_zero()
307 assert (btor_sort_is_bv (btor, sort)); in btor_exp_bv_ones()
325 assert (btor_sort_is_bv (btor, sort)); in btor_exp_bv_one()
343 assert (btor_sort_is_bv (btor, sort)); in btor_exp_bv_min_signed()
361 assert (btor_sort_is_bv (btor, sort)); in btor_exp_bv_max_signed()
379 assert (btor_sort_is_bv (btor, sort)); in btor_exp_bv_int()
397 assert (btor_sort_is_bv (btor, sort)); in btor_exp_bv_unsigned()
|
| H A D | btornode.h | 345 return btor_sort_is_bv (exp->btor, exp->sort_id) in btor_node_is_bv_const()
354 return btor_sort_is_bv (exp->btor, exp->sort_id) in btor_node_is_bv_var()
|
| H A D | btorsort.c | 734 return btor_sort_is_bv (btor, id) && btor_sort_bv_get_width (btor, id) == 1; in btor_sort_is_bool()
738 btor_sort_is_bv (Btor *btor, BtorSortId id) in btor_sort_is_bv() function
|
| H A D | btornode.c | 71 && btor_sort_is_bv (btor_node_real_addr (exp)->btor, in btor_node_is_bv_cond()
2307 assert (btor_sort_is_bv (btor, sort)); in btor_node_create_var()
2332 assert (btor_sort_is_bv (btor, btor_sort_fun_get_codomain (btor, sort)) in btor_node_create_uf()
2350 assert (btor_sort_is_bv (btor, sort)); in btor_node_create_param()
|
| H A D | btorslvfun.c | 472 assert (btor_sort_is_bv (btor, sort)); in create_function_inequality()
|