Searched refs:zero_e2 (Results 1 – 2 of 2) sorted by relevance
/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/ |
H A D | fpa2bv_converter.cpp | 1708 expr_ref zero_e2(m), min_exp(m), sig_lz(m), max_exp_delta(m), sig_lz_capped(m), renorm_delta(m); in mk_fma() local 1709 zero_e2 = m_bv_util.mk_numeral(0, ebits + 2); in mk_fma() 1716 renorm_delta = m.mk_ite(m_bv_util.mk_sle(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2); in mk_fma() 2157 expr_ref zero_e2(m), min_exp(m), sig_lz(m), max_exp_delta(m), sig_lz_capped(m), renorm_delta(m); in mk_round_to_integral() local 2158 zero_e2 = m_bv_util.mk_numeral(0, ebits+2); in mk_round_to_integral() 2164 renorm_delta = m.mk_ite(m_bv_util.mk_ule(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2); in mk_round_to_integral()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/ |
H A D | fpa2bv_converter.cpp | 1697 expr_ref zero_e2(m), min_exp(m), sig_lz(m), max_exp_delta(m), sig_lz_capped(m), renorm_delta(m); 1698 zero_e2 = m_bv_util.mk_numeral(0, ebits + 2); 1705 renorm_delta = m.mk_ite(m_bv_util.mk_sle(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2); 2146 expr_ref zero_e2(m), min_exp(m), sig_lz(m), max_exp_delta(m), sig_lz_capped(m), renorm_delta(m); 2147 zero_e2 = m_bv_util.mk_numeral(0, ebits+2); 2153 renorm_delta = m.mk_ite(m_bv_util.mk_ule(zero_e2, sig_lz_capped), sig_lz_capped, zero_e2);
|