Home
last modified time | relevance | path

Searched refs:big_sig (Results 1 – 2 of 2) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/
H A Dfpa2bv_converter.cpp3316 expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), is_neg_shift(m), big_sig(m); in mk_to_bv() local
3321 big_sig = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(bv_sz + 2, sig), bv0); in mk_to_bv()
3323 SASSERT(m_bv_util.get_bv_size(big_sig) == big_sig_sz); in mk_to_bv()
3338 SASSERT(m_bv_util.get_bv_size(shift) == m_bv_util.get_bv_size(big_sig)); in mk_to_bv()
3339 dbg_decouple("fpa2bv_to_bv_big_sig", big_sig); in mk_to_bv()
3349 big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift), in mk_to_bv()
3350 m_bv_util.mk_bv_shl(big_sig, shift)); in mk_to_bv()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/
H A Dfpa2bv_converter.cpp3310 expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), is_neg_shift(m), big_sig(m);
3315 big_sig = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(bv_sz + 2, sig), bv0);
3317 SASSERT(m_bv_util.get_bv_size(big_sig) == big_sig_sz);
3332 SASSERT(m_bv_util.get_bv_size(shift) == m_bv_util.get_bv_size(big_sig));
3333 dbg_decouple("fpa2bv_to_bv_big_sig", big_sig);
3343 big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift),
3344 m_bv_util.mk_bv_shl(big_sig, shift));