Searched refs:exp_bv (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 | 3236 expr_ref exp_bv(m), exp_all_ones(m); in mk_to_ieee_bv_unspecified() local
3237 exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); in mk_to_ieee_bv_unspecified()
3238 exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits))); in mk_to_ieee_bv_unspecified()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/ |
| H A D | fpa2bv_converter.cpp | 3230 expr_ref exp_bv(m), exp_all_ones(m);
3231 exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result);
3232 exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, ebits)));
|