mirror of
https://github.com/Z3Prover/z3
synced 2026-04-02 09:58:59 +00:00
fix #8185: add FPA rewriter simplifications for fma with zero multiplicand and classification of int-to-float conversions
Three optimizations that eliminate expensive FP bit-blasting: 1. fma(rm, ±0, y, z): decompose into simpler operations instead of building the full FMA bit-blast circuit. When z is a concrete non-zero value, simplifies to ite(isFinite(y), z, NaN). 2. isNaN/isInf/isNormal applied to to_fp(rm, to_real(int_expr)): convert to pure integer constraints. For integers, to_fp never produces NaN or subnormals, so classification reduces to overflow threshold checks based on the rounding mode. 3. Push classification functions (isNaN, isInf, isNormal) through ite when both branches are concrete FP numerals. Together these transform the original formula from requiring full FP bit-blasting (timeout) to pure integer/real reasoning (instant). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson
parent
b5bf4be87e
commit
a37003fa2d
2 changed files with 244 additions and 0 deletions
|
|
@ -428,6 +428,86 @@ br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg
|
|||
result = m_util.mk_value(t);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// fma(rm, ±0, y, z) or fma(rm, x, ±0, z): when one multiplicand is
|
||||
// a concrete zero the full FMA bit-blast circuit is unnecessary.
|
||||
// IEEE 754: 0 * finite = ±0, so fma reduces to fp.add(rm, ±0, z).
|
||||
// 0 * NaN = NaN, 0 * inf = NaN.
|
||||
expr *other_mul = nullptr;
|
||||
bool zero_is_neg = false;
|
||||
scoped_mpf vzero(m_fm);
|
||||
if (m_util.is_numeral(arg2, vzero) && m_fm.is_zero(vzero)) {
|
||||
other_mul = arg3;
|
||||
zero_is_neg = m_fm.is_neg(vzero);
|
||||
}
|
||||
else {
|
||||
scoped_mpf v3tmp(m_fm);
|
||||
if (m_util.is_numeral(arg3, v3tmp) && m_fm.is_zero(v3tmp)) {
|
||||
other_mul = arg2;
|
||||
zero_is_neg = m_fm.is_neg(v3tmp);
|
||||
m_fm.set(vzero, v3tmp);
|
||||
}
|
||||
}
|
||||
|
||||
if (other_mul) {
|
||||
TRACE(fp_rewriter, tout << "fma zero-multiplicand simplification\n";);
|
||||
sort *s = arg4->get_sort();
|
||||
expr_ref nan(m_util.mk_nan(s), m());
|
||||
|
||||
// fma(rm, ±0, y, NaN) = NaN
|
||||
if (m_util.is_nan(arg4)) {
|
||||
result = nan;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// If the other multiplicand is a concrete NaN or infinity, result is NaN
|
||||
scoped_mpf vo(m_fm);
|
||||
if (m_util.is_numeral(other_mul, vo) && (m_fm.is_nan(vo) || m_fm.is_inf(vo))) {
|
||||
result = nan;
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
// If the other multiplicand is concrete and finite, compute the product
|
||||
// ±0, which is exact, then rewrite to fp.add(rm, product, z)
|
||||
if (m_util.is_numeral(other_mul, vo)) {
|
||||
scoped_mpf product(m_fm);
|
||||
m_fm.mul(rm, vzero, vo, product);
|
||||
SASSERT(m_fm.is_zero(product));
|
||||
result = m_util.mk_add(arg1, m_util.mk_value(product), arg4);
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
|
||||
// other_mul is symbolic.
|
||||
// When z is a concrete non-zero non-NaN value, ±0 + z = z exactly,
|
||||
// so fma(rm, ±0, y, z_const) = ite(not isNaN(y) and not isInf(y), z_const, NaN)
|
||||
scoped_mpf vz(m_fm);
|
||||
if (m_util.is_numeral(arg4, vz) && !m_fm.is_zero(vz) && !m_fm.is_nan(vz)) {
|
||||
expr_ref finite_cond(m());
|
||||
finite_cond = m().mk_not(m().mk_or(m_util.mk_is_nan(other_mul),
|
||||
m_util.mk_is_inf(other_mul)));
|
||||
result = m().mk_ite(finite_cond, arg4, nan);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
|
||||
// General case: decompose fma into ite + fp.add, avoiding
|
||||
// the expensive FMA bit-blast.
|
||||
// product sign = sign(zero) XOR sign(other_mul)
|
||||
expr_ref pzero(m_util.mk_pzero(s), m());
|
||||
expr_ref nzero(m_util.mk_nzero(s), m());
|
||||
expr_ref product_zero(m());
|
||||
if (zero_is_neg)
|
||||
product_zero = m().mk_ite(m_util.mk_is_negative(other_mul), pzero, nzero);
|
||||
else
|
||||
product_zero = m().mk_ite(m_util.mk_is_negative(other_mul), nzero, pzero);
|
||||
|
||||
expr_ref finite_cond(m());
|
||||
finite_cond = m().mk_not(m().mk_or(m_util.mk_is_nan(other_mul),
|
||||
m_util.mk_is_inf(other_mul)));
|
||||
result = m().mk_ite(finite_cond,
|
||||
m_util.mk_add(arg1, product_zero, arg4),
|
||||
nan);
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
|
|
@ -588,6 +668,30 @@ br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) {
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
// isNaN(to_fp(rm, real_or_int)) is always false:
|
||||
// converting a real/int value never produces NaN.
|
||||
if (m_util.is_to_fp(arg1)) {
|
||||
app * a = to_app(arg1);
|
||||
if (a->get_num_args() == 2 &&
|
||||
(m_util.au().is_real(a->get_arg(1)) ||
|
||||
m_util.au().is_int(a->get_arg(1)))) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
|
||||
// Push through ite when both branches are concrete FP numerals.
|
||||
expr *c = nullptr, *t = nullptr, *e = nullptr;
|
||||
if (m().is_ite(arg1, c, t, e)) {
|
||||
scoped_mpf vt(m_fm), ve(m_fm);
|
||||
if (m_util.is_numeral(t, vt) && m_util.is_numeral(e, ve)) {
|
||||
result = m().mk_ite(c,
|
||||
m_fm.is_nan(vt) ? m().mk_true() : m().mk_false(),
|
||||
m_fm.is_nan(ve) ? m().mk_true() : m().mk_false());
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
@ -599,6 +703,50 @@ br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) {
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
// isInf(to_fp(rm, to_real(int))) → integer overflow condition.
|
||||
// Converting a real never produces NaN, and for an integer source,
|
||||
// overflow to ±infinity depends only on the magnitude and rounding mode.
|
||||
mpf_rounding_mode rm;
|
||||
if (m_util.is_to_fp(arg1)) {
|
||||
app * a = to_app(arg1);
|
||||
if (a->get_num_args() == 2 && m_util.is_rm_numeral(a->get_arg(0), rm)) {
|
||||
expr * inner = a->get_arg(1);
|
||||
expr * int_expr = nullptr;
|
||||
// Detect to_real(int_expr)
|
||||
if (m_util.au().is_to_real(inner)) {
|
||||
expr * unwrapped = to_app(inner)->get_arg(0);
|
||||
if (m_util.au().is_int(unwrapped))
|
||||
int_expr = unwrapped;
|
||||
}
|
||||
else if (m_util.au().is_int(inner))
|
||||
int_expr = inner;
|
||||
|
||||
if (int_expr) {
|
||||
func_decl * fd = a->get_decl();
|
||||
unsigned ebits = fd->get_parameter(0).get_int();
|
||||
unsigned sbits = fd->get_parameter(1).get_int();
|
||||
result = mk_is_inf_of_int(rm, ebits, sbits, int_expr);
|
||||
if (result)
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// isInf(to_fp(rm, real_or_int)) where input is a real: never NaN,
|
||||
// but we can't determine finiteness without knowing the real value.
|
||||
|
||||
// Push through ite when both branches are concrete FP numerals.
|
||||
expr *c = nullptr, *t = nullptr, *e = nullptr;
|
||||
if (m().is_ite(arg1, c, t, e)) {
|
||||
scoped_mpf vt(m_fm), ve(m_fm);
|
||||
if (m_util.is_numeral(t, vt) && m_util.is_numeral(e, ve)) {
|
||||
result = m().mk_ite(c,
|
||||
m_fm.is_inf(vt) ? m().mk_true() : m().mk_false(),
|
||||
m_fm.is_inf(ve) ? m().mk_true() : m().mk_false());
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
@ -610,6 +758,48 @@ br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) {
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
// isNormal(to_fp(rm, to_real(int_expr))) → int_expr ≠ 0 ∧ ¬isInf(to_fp(...))
|
||||
// For integer x: to_fp is never NaN or subnormal, so
|
||||
// isNormal ↔ x ≠ 0 ∧ ¬overflow(x)
|
||||
mpf_rounding_mode rm;
|
||||
if (m_util.is_to_fp(arg1)) {
|
||||
app * a = to_app(arg1);
|
||||
if (a->get_num_args() == 2 && m_util.is_rm_numeral(a->get_arg(0), rm)) {
|
||||
expr * inner = a->get_arg(1);
|
||||
expr * int_expr = nullptr;
|
||||
if (m_util.au().is_to_real(inner)) {
|
||||
expr * unwrapped = to_app(inner)->get_arg(0);
|
||||
if (m_util.au().is_int(unwrapped))
|
||||
int_expr = unwrapped;
|
||||
}
|
||||
else if (m_util.au().is_int(inner))
|
||||
int_expr = inner;
|
||||
|
||||
if (int_expr) {
|
||||
func_decl * fd = a->get_decl();
|
||||
unsigned ebits = fd->get_parameter(0).get_int();
|
||||
unsigned sbits = fd->get_parameter(1).get_int();
|
||||
arith_util & au = m_util.au();
|
||||
expr_ref not_zero(m().mk_not(m().mk_eq(int_expr, au.mk_int(0))), m());
|
||||
expr_ref inf_cond = mk_is_inf_of_int(rm, ebits, sbits, int_expr);
|
||||
result = m().mk_and(not_zero, m().mk_not(inf_cond));
|
||||
return BR_REWRITE_FULL;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Push through ite when both branches are concrete FP numerals.
|
||||
expr *c = nullptr, *t = nullptr, *e = nullptr;
|
||||
if (m().is_ite(arg1, c, t, e)) {
|
||||
scoped_mpf vt(m_fm), ve(m_fm);
|
||||
if (m_util.is_numeral(t, vt) && m_util.is_numeral(e, ve)) {
|
||||
result = m().mk_ite(c,
|
||||
m_fm.is_normal(vt) ? m().mk_true() : m().mk_false(),
|
||||
m_fm.is_normal(ve) ? m().mk_true() : m().mk_false());
|
||||
return BR_REWRITE2;
|
||||
}
|
||||
}
|
||||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
@ -844,3 +1034,54 @@ br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) {
|
|||
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
// Compute isInf(to_fp(rm, to_real(x))) as an integer constraint on x.
|
||||
// For integer x, to_fp(rm, x) can only be ±0, normal, or ±infinity, never NaN or subnormal.
|
||||
// The overflow boundary depends on the rounding mode and float format.
|
||||
expr_ref fpa_rewriter::mk_is_inf_of_int(mpf_rounding_mode rm, unsigned ebits, unsigned sbits, expr * int_expr) {
|
||||
arith_util & au = m_util.au();
|
||||
|
||||
// Compute MAX_FINITE as a rational
|
||||
scoped_mpf max_val(m_fm);
|
||||
m_fm.mk_max_value(ebits, sbits, false, max_val);
|
||||
scoped_mpq max_q(m_fm.mpq_manager());
|
||||
m_fm.to_rational(max_val, max_q);
|
||||
rational max_finite(max_q);
|
||||
|
||||
// ULP at MAX_FINITE = 2^(max_exp - sbits + 1)
|
||||
mpf_exp_t max_exp = m_fm.mk_max_exp(ebits);
|
||||
int ulp_exp = (int)max_exp - (int)sbits + 1;
|
||||
rational half_ulp = rational::power_of_two(ulp_exp) / rational(2);
|
||||
|
||||
expr_ref r(m());
|
||||
|
||||
switch (rm) {
|
||||
case MPF_ROUND_NEAREST_TEVEN:
|
||||
case MPF_ROUND_NEAREST_TAWAY: {
|
||||
// Overflow when |x| >= MAX_FINITE + ULP/2.
|
||||
// At the midpoint, RNE rounds to even, which is infinity since
|
||||
// MAX_FINITE has an odd significand. RNA also rounds to infinity.
|
||||
rational threshold = max_finite + half_ulp;
|
||||
expr_ref thr(au.mk_int(threshold), m());
|
||||
expr_ref neg_thr(au.mk_int(-threshold), m());
|
||||
// |x| >= threshold ↔ x >= threshold || x <= -threshold
|
||||
r = m().mk_or(au.mk_ge(int_expr, thr), au.mk_le(int_expr, neg_thr));
|
||||
break;
|
||||
}
|
||||
case MPF_ROUND_TOWARD_POSITIVE:
|
||||
// RTP: positive overflow when x > MAX_FINITE, negative overflow never.
|
||||
r = au.mk_gt(int_expr, au.mk_int(max_finite));
|
||||
break;
|
||||
case MPF_ROUND_TOWARD_NEGATIVE:
|
||||
// RTN: negative overflow when x < -MAX_FINITE, positive overflow never.
|
||||
r = au.mk_lt(int_expr, au.mk_int(-max_finite));
|
||||
break;
|
||||
case MPF_ROUND_TOWARD_ZERO:
|
||||
// RTZ: never overflows to infinity from finite input.
|
||||
r = m().mk_false();
|
||||
break;
|
||||
}
|
||||
|
||||
TRACE(fp_rewriter, tout << "isInf(to_fp(rm, int)) -> " << mk_ismt2_pp(r, m()) << "\n";);
|
||||
return r;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -88,5 +88,8 @@ public:
|
|||
br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
|
||||
|
||||
br_status mk_bvwrap(expr * arg, expr_ref & result);
|
||||
|
||||
// Helper: compute isInf(to_fp(rm, to_real(int_expr))) as integer constraint
|
||||
expr_ref mk_is_inf_of_int(mpf_rounding_mode rm, unsigned ebits, unsigned sbits, expr * int_expr);
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue