big_sig_shifted (reference) in projects: dports

Searched refs:big_sig_shifted (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	3348 expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m); in mk_to_bv() local 3349 big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift), in mk_to_bv() 3351 int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted); in mk_to_bv() 3353 last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted); in mk_to_bv() 3354 round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted); in mk_to_bv() 3355 stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted); in mk_to_bv() 3357 dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted); in mk_to_bv()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/
H A D	fpa2bv_converter.cpp	3342 expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m); 3343 big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift), 3345 int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted); 3347 last = m_bv_util.mk_extract(big_sig_sz-(bv_sz+3), big_sig_sz-(bv_sz+3), big_sig_shifted); 3348 round = m_bv_util.mk_extract(big_sig_sz-(bv_sz+4), big_sig_sz-(bv_sz+4), big_sig_shifted); 3349 stickies = m_bv_util.mk_extract(big_sig_sz-(bv_sz+5), 0, big_sig_shifted); 3351 dbg_decouple("fpa2bv_to_bv_big_sig_shifted", big_sig_shifted);