Home
last modified time | relevance | path

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 Dbtornormadd.c181 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 Dbtorextract.c133 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 Dbtorrewrite.c828 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 Dbtorexp.c173 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 Dbtorexp.h97 BtorNode *btor_exp_bv_zero (Btor *btor, BtorSortId sort);
H A Dbtorcore.c1392 *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 Dbtorslvquant.c1103 e_else = btor_exp_bv_zero (btor, evar->sort_id); in mk_concrete_ite_model()
H A Dboolector.c1408 res = btor_exp_bv_zero (btor, s); in boolector_zero()
/dports/math/boolector/boolector-3.2.2/test/
H A Dtest_normquant.cpp315 zero = btor_exp_bv_zero (d_btor, sort); in TEST_F()
H A Dtest_exp.cpp262 exp1 = btor_exp_bv_zero (d_btor, sort); in TEST_F()
H A Dtest_lambda.cpp259 c = btor_exp_bv_zero (d_btor, d_elem_sort); in TEST_F()