Home
last modified time | relevance | path

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

/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/
H A Dfpa2bv_converter.cpp533 expr_ref res_sig_eq(m), sig_abs(m), one_1(m); in add_core() local
535 m_simp.mk_eq(sign_bv, one_1, res_sig_eq); in add_core()
536 m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs); in add_core()
1675 expr_ref res_sig_eq(m), sig_abs(m); in mk_fma() local
1676 m_simp.mk_eq(sign_bv, one_1, res_sig_eq); in mk_fma()
1677 m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs); in mk_fma()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/
H A Dfpa2bv_converter.cpp532 expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
534 m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
535 m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
1664 expr_ref res_sig_eq(m), sig_abs(m);
1665 m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
1666 m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);