Home
last modified time | relevance | path

Searched refs:SIGovf (Results 1 – 4 of 4) sorted by relevance

/dports/math/py-z3-solver/z3-z3-4.8.10/src/util/
H A Dmpf.cpp2071 bool SIGovf = o.exponent > e_max; in round() local
2073 TRACE("mpf_dbg", tout << "SIGovf = " << SIGovf << std::endl;); in round()
2078 bool OVF2 = SIGovf && o_has_max_exp; in round()
/dports/math/z3/z3-z3-4.8.13/src/util/
H A Dmpf.cpp2071 bool SIGovf = o.exponent > e_max; in round() local
2073 TRACE("mpf_dbg", tout << "SIGovf = " << SIGovf << std::endl;); in round()
2078 bool OVF2 = SIGovf && o_has_max_exp; in round()
/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/
H A Dfpa2bv_converter.cpp4104 expr_ref SIGovf(m); in round() local
4106 m_simp.mk_eq(t_sig, one_1, SIGovf); in round()
4107 SASSERT(is_well_sorted(m, SIGovf)); in round()
4108 dbg_decouple("fpa2bv_rnd_SIGovf", SIGovf); in round()
4113 m_simp.mk_ite(SIGovf, hallbut1_sig, lallbut1_sig, sig); in round()
4119 m_simp.mk_ite(SIGovf, exp_p1, exp, exp); in round()
4143 m_simp.mk_and(SIGovf, preOVF2, OVF2); in round()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/
H A Dfpa2bv_converter.cpp4088 expr_ref SIGovf(m);
4090 m_simp.mk_eq(t_sig, one_1, SIGovf);
4091 SASSERT(is_well_sorted(m, SIGovf));
4092 dbg_decouple("fpa2bv_rnd_SIGovf", SIGovf);
4097 m_simp.mk_ite(SIGovf, hallbut1_sig, lallbut1_sig, sig);
4103 m_simp.mk_ite(SIGovf, exp_p1, exp, exp);
4127 m_simp.mk_and(SIGovf, preOVF2, OVF2);