Home
last modified time | relevance | path

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

/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/
H A Dfpa2bv_converter.cpp77 expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m); in mk_eq() local
80 m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan); in mk_eq()
81 dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan); in mk_eq()
83 m_simp.mk_or(both_are_nan, both_the_same, result); in mk_eq()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/
H A Dfpa2bv_converter.cpp76 expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m);
79 m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan);
80 dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan);
82 m_simp.mk_or(both_are_nan, both_the_same, result);