Searched refs:btor_exp_bv_zero (Results 1 – 11 of 11) sorted by relevance
/dports/math/boolector/boolector-3.2.2/src/preprocess/ |
H A D | btornormadd.c | 181 BtorNode *zero = btor_exp_bv_zero (btor, sort_id); in prep_leafs() 239 BtorNode *zero = btor_exp_bv_zero (btor, sort_id); in normalize_coeffs() 405 BtorNode *zero = btor_exp_bv_zero (btor, sort_id); in normalize_eq_adds()
|
H A D | btorextract.c | 133 zero = btor_exp_bv_zero (btor, btor_node_get_sort_id (slice)); in create_range() 145 zero = btor_exp_bv_zero (btor, btor_node_get_sort_id (lower)); in create_range()
|
/dports/math/boolector/boolector-3.2.2/src/ |
H A D | btorrewrite.c | 828 tmp3 = btor_exp_bv_zero (btor, sort); in apply_special_const_lhs_binary_exp() 874 tmp4 = btor_exp_bv_zero (btor, sort); in apply_special_const_lhs_binary_exp() 1107 tmp3 = btor_exp_bv_zero (btor, sort); in apply_special_const_rhs_binary_exp() 1153 tmp4 = btor_exp_bv_zero (btor, sort); in apply_special_const_rhs_binary_exp() 1785 tmp = btor_exp_bv_zero (btor, btor_node_get_sort_id (e0)); in apply_add_left_eq() 2471 zero = btor_exp_bv_zero (btor, sort); 4134 pad = btor_exp_bv_zero (btor, sort); in apply_power2_udiv() 4531 result = btor_exp_bv_zero (btor, sort); in apply_const_sll() 4538 pad = btor_exp_bv_zero (btor, sort); in apply_const_sll() 4591 result = btor_exp_bv_zero (btor, sort); in apply_const_srl() [all …]
|
H A D | btorexp.c | 173 result = btor_exp_bv_zero (btor, sort); in btor_exp_false() 285 btor_exp_bv_zero (Btor *btor, BtorSortId sort) in btor_exp_bv_zero() function 450 zero = btor_exp_bv_zero (btor, btor_node_get_sort_id (exp)); in btor_exp_bv_redor() 533 zero = btor_exp_bv_zero (btor, sort); in btor_exp_bv_uext() 559 zero = btor_exp_bv_zero (btor, sort); in btor_exp_bv_sext() 823 result = btor_exp_bv_zero (btor, sort); in btor_exp_bv_umulo() 1219 zero = btor_exp_bv_zero (btor, sort); in exp_rotate() 1545 zero = btor_exp_bv_zero (btor, btor_node_get_sort_id (e0)); in btor_exp_bv_smod()
|
H A D | btorexp.h | 97 BtorNode *btor_exp_bv_zero (Btor *btor, BtorSortId sort);
|
H A D | btorcore.c | 1392 *right_result = btor_exp_bv_zero (btor, sort); in normalize_substitution() 1457 const_exp = btor_exp_bv_zero (btor, sort); in normalize_substitution()
|
H A D | btorslvquant.c | 1103 e_else = btor_exp_bv_zero (btor, evar->sort_id); in mk_concrete_ite_model()
|
H A D | boolector.c | 1408 res = btor_exp_bv_zero (btor, s); in boolector_zero()
|
/dports/math/boolector/boolector-3.2.2/test/ |
H A D | test_normquant.cpp | 315 zero = btor_exp_bv_zero (d_btor, sort); in TEST_F()
|
H A D | test_exp.cpp | 262 exp1 = btor_exp_bv_zero (d_btor, sort); in TEST_F()
|
H A D | test_lambda.cpp | 259 c = btor_exp_bv_zero (d_btor, d_elem_sort); in TEST_F()
|