From 1b73e5f1de00029880a29e714b7de7f4eba54ce3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 5 Apr 2026 02:01:12 +0000 Subject: [PATCH] fstar: add fpa_rewriter_rules.h with C++ macros extracted from F* lemmas Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/46fcd3bf-be90-4098-8516-fde0f1e37cbf Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- fstar/FPARewriterRules.fst | 35 ++- fstar/README.md | 61 ++++-- src/ast/rewriter/fpa_rewriter.cpp | 64 ++++++ src/ast/rewriter/fpa_rewriter.h | 5 + src/ast/rewriter/fpa_rewriter_rules.h | 296 ++++++++++++++++++++++++++ 5 files changed, 433 insertions(+), 28 deletions(-) create mode 100644 src/ast/rewriter/fpa_rewriter_rules.h diff --git a/fstar/FPARewriterRules.fst b/fstar/FPARewriterRules.fst index 46fb2b92e..8594ab182 100644 --- a/fstar/FPARewriterRules.fst +++ b/fstar/FPARewriterRules.fst @@ -51,7 +51,8 @@ open IEEE754 (* 1a. fma(rm, ±0, y, NaN) = NaN Source: C++ fpa_rewriter.cpp, mk_fma, branch "if (m_util.is_nan(arg4))". - The addend NaN propagates (IEEE 754-2019 §6.2, NaN payload rules). *) + The addend NaN propagates (IEEE 754-2019 §6.2, NaN payload rules). + [extract: FPA_REWRITE_FMA_ZERO_MUL, case (a)] *) let lemma_fma_zero_nan_addend (#eb #sb: pos) (rm: rounding_mode) (zero_val y: float eb sb) @@ -62,7 +63,8 @@ let lemma_fma_zero_nan_addend (* 1b. fma(rm, ±0, NaN, z) = NaN Source: C++ check "m_fm.is_nan(vo)" for other_mul. - NaN in the second multiplicand propagates regardless of the addend. *) + NaN in the second multiplicand propagates regardless of the addend. + [extract: FPA_REWRITE_FMA_ZERO_MUL, case (b)] *) let lemma_fma_zero_nan_mul (#eb #sb: pos) (rm: rounding_mode) (zero_val z: float eb sb) @@ -74,7 +76,8 @@ let lemma_fma_zero_nan_mul (* 1c. fma(rm, ±0, ±∞, z) = NaN Source: C++ check "m_fm.is_inf(vo)" for other_mul. 0 * ∞ is the "invalid operation" NaN (IEEE 754-2019 §7.2), - which then propagates through the addition. *) + which then propagates through the addition. + [extract: FPA_REWRITE_FMA_ZERO_MUL, case (b)] *) let lemma_fma_zero_inf_mul (#eb #sb: pos) (rm: rounding_mode) (zero_val inf_val z: float eb sb) @@ -90,7 +93,8 @@ let lemma_fma_zero_inf_mul an addition whose first operand is the computed ±0 product. This is the key decomposition that replaces the expensive FMA - circuit with a cheaper addition. *) + circuit with a cheaper addition. + [extract: FPA_REWRITE_FMA_ZERO_MUL, case (c)] *) let lemma_fma_zero_finite_decomposes (#eb #sb: pos) (rm: rounding_mode) (zero_val y z: float eb sb) @@ -105,7 +109,8 @@ let lemma_fma_zero_finite_decomposes Source: C++ branch with "m_util.is_numeral(arg4, vz) && !m_fm.is_zero(vz)" and a concrete finite other_mul. When z is nonzero and finite, ±0 + z = z exactly under any rounding - mode (IEEE 754-2019 §6.3), so the entire fma collapses to z. *) + mode (IEEE 754-2019 §6.3), so the entire fma collapses to z. + [extract: FPA_REWRITE_FMA_ZERO_MUL, case (c) folded with ax_add_zero_nonzero] *) let lemma_fma_zero_const_addend (#eb #sb: pos) (rm: rounding_mode) (zero_val y z: float eb sb) @@ -123,6 +128,7 @@ let lemma_fma_zero_const_addend ite(¬isNaN(y) ∧ ¬isInf(y), z_const, NaN) Source: C++ branch producing "m().mk_ite(finite_cond, arg4, nan)". We prove each arm of the ite separately. + [extract: FPA_REWRITE_FMA_ZERO_MUL, case (d)] Finite arm: y is finite → fma = z_const (by 1e). *) let lemma_fma_zero_const_finite_arm @@ -155,7 +161,8 @@ let lemma_fma_zero_const_nan_inf_arm ite(is_finite(y), fp_add(rm, product_zero, z), NaN) Source: C++ block producing the final ite with product_zero. product_zero is ±0 with sign = sign(±0) XOR sign(y). - We prove each arm. *) + We prove each arm. + [extract: FPA_REWRITE_FMA_ZERO_MUL, case (e)] *) (* Finite arm: fma = fp_add(rm, fp_mul(rm, ±0, y), z). *) let lemma_fma_zero_general_finite_arm @@ -217,7 +224,8 @@ let lemma_fma_zero_product_sign (* isNaN(to_fp(rm, x)) = false for any integer x. Source: C++ block in mk_is_nan checking "a->get_num_args() == 2 && - (m_util.au().is_real(a->get_arg(1)) || m_util.au().is_int(a->get_arg(1)))". *) + (m_util.au().is_real(a->get_arg(1)) || m_util.au().is_int(a->get_arg(1)))". + [extract: FPA_REWRITE_IS_NAN_TO_FP_INT] *) let lemma_is_nan_to_fp_int (#eb #sb: pos) (rm: rounding_mode) (x: int) : Lemma (is_nan (to_fp_of_int #eb #sb rm x) = false) = @@ -227,7 +235,8 @@ let lemma_is_nan_to_fp_int (* --- 2b: isInf --- *) (* Source: C++ function mk_is_inf_of_int, called from mk_is_inf. - Each lemma corresponds to one case in the switch(rm) statement. *) + Each lemma corresponds to one case in the switch(rm) statement. + [extract: FPA_REWRITE_IS_INF_TO_FP_INT, helper mk_is_inf_of_int] *) (* RNE: overflow iff |x| >= overflow_threshold(eb, sb). At the boundary the significand of MAX_FINITE is odd, so RNE rounds @@ -270,6 +279,7 @@ let lemma_is_inf_to_fp_int_rtz Source: C++ block in mk_is_normal: "expr_ref not_zero(...); expr_ref inf_cond = mk_is_inf_of_int(...); result = m().mk_and(not_zero, m().mk_not(inf_cond));" + [extract: FPA_REWRITE_IS_NORMAL_TO_FP_INT] Proof sketch: For integer x, to_fp is never NaN (by ax_to_fp_int_not_nan) and @@ -322,7 +332,8 @@ let lemma_is_normal_to_fp_int (* 3a. isNaN(ite(c, t, e)) = ite(c, isNaN(t), isNaN(e)) Source: C++ block producing "m().mk_ite(c, is_nan(t) ? true : false, - is_nan(e) ? true : false)". *) + is_nan(e) ? true : false)". + [extract: FPA_REWRITE_IS_NAN_ITE] *) let lemma_is_nan_ite (#eb #sb: pos) (c: bool) (t e: float eb sb) : Lemma (is_nan (if c then t else e) = @@ -330,7 +341,8 @@ let lemma_is_nan_ite (* 3b. isInf(ite(c, t, e)) = ite(c, isInf(t), isInf(e)) - Source: same pattern in mk_is_inf. *) + Source: same pattern in mk_is_inf. + [extract: FPA_REWRITE_IS_INF_ITE] *) let lemma_is_inf_ite (#eb #sb: pos) (c: bool) (t e: float eb sb) : Lemma (is_inf (if c then t else e) = @@ -338,7 +350,8 @@ let lemma_is_inf_ite (* 3c. isNormal(ite(c, t, e)) = ite(c, isNormal(t), isNormal(e)) - Source: same pattern in mk_is_normal. *) + Source: same pattern in mk_is_normal. + [extract: FPA_REWRITE_IS_NORMAL_ITE] *) let lemma_is_normal_ite (#eb #sb: pos) (c: bool) (t e: float eb sb) : Lemma (is_normal (if c then t else e) = diff --git a/fstar/README.md b/fstar/README.md index 971bb81c7..1bc56151b 100644 --- a/fstar/README.md +++ b/fstar/README.md @@ -20,7 +20,6 @@ that avoid expensive FP bit-blasting: ### `IEEE754.fst` Abstract axiomatic theory of IEEE 754 floating-point arithmetic. - - **Type** `float eb sb` — abstract float parameterized by exponent bits `eb` and significand bits `sb`, matching Z3's `mpf` representation. - **Type** `rounding_mode` — the five IEEE 754 rounding modes (RNE, RNA, RTP, @@ -83,25 +82,53 @@ The Section 3 lemmas are trivially true in F\* by computation (applying a function to `if c then t else e` reduces to `if c then f t else f e`), which is why their proofs are the single term `()`. +### `../src/ast/rewriter/fpa_rewriter_rules.h` + +C++ header containing one `#define` macro per rewrite rule, extracted from +the F\* lemmas. Each macro is annotated with a `[extract: MACRO_NAME]` +comment in the corresponding F\* lemma. + +| Macro | F\* lemma(s) | Used in C++ function | +|---|---|---| +| `FPA_REWRITE_IS_NAN_TO_FP_INT` | `lemma_is_nan_to_fp_int` | `mk_is_nan` | +| `FPA_REWRITE_IS_NAN_ITE` | `lemma_is_nan_ite` | `mk_is_nan` | +| `FPA_REWRITE_IS_INF_TO_FP_INT` | `lemma_is_inf_to_fp_int_*` | `mk_is_inf` | +| `FPA_REWRITE_IS_INF_ITE` | `lemma_is_inf_ite` | `mk_is_inf` | +| `FPA_REWRITE_IS_NORMAL_TO_FP_INT` | `lemma_is_normal_to_fp_int` | `mk_is_normal` | +| `FPA_REWRITE_IS_NORMAL_ITE` | `lemma_is_normal_ite` | `mk_is_normal` | +| `FPA_REWRITE_FMA_ZERO_MUL` | `lemma_fma_zero_*` (all §1 lemmas) | `mk_fma` | + +Each macro is self-contained and uses `_fpa_`-prefixed local variables to +avoid name collisions. All macros are designed for use inside member +functions of `fpa_rewriter` where `m()`, `m_util`, `m_fm`, and +`mk_is_inf_of_int` are in scope. + +The helper function `mk_is_inf_of_int` (declared in `fpa_rewriter.h`, +implemented in `fpa_rewriter.cpp`) computes the integer-arithmetic overflow +condition for `isInf(to_fp(rm, x))` by switching on the rounding mode, +corresponding to the five `lemma_is_inf_to_fp_int_*` lemmas. + ## Relationship to the C++ Code -The following table maps each lemma to the corresponding C++ code in -`src/ast/rewriter/fpa_rewriter.cpp` after the PR is applied. +The following table maps each lemma to the corresponding C++ macro in +`src/ast/rewriter/fpa_rewriter_rules.h` and where it is used. -| Lemma | C++ code | -|---|---| -| `lemma_fma_zero_nan_addend` | `if (m_util.is_nan(arg4)) { result = nan; return BR_DONE; }` | -| `lemma_fma_zero_nan_mul` | `if (m_util.is_numeral(other_mul, vo) && m_fm.is_nan(vo))` | -| `lemma_fma_zero_inf_mul` | `if (m_util.is_numeral(other_mul, vo) && m_fm.is_inf(vo))` | -| `lemma_fma_zero_finite_decomposes` | `m_util.mk_add(arg1, m_util.mk_value(product), arg4)` with `m_fm.mul(rm, vzero, vo, product)` | -| `lemma_fma_zero_const_addend` | `m().mk_ite(finite_cond, arg4, nan)` (z_const branch) | -| `lemma_fma_zero_general_*` | general `m().mk_ite(finite_cond, m_util.mk_add(...), nan)` | -| `lemma_is_nan_to_fp_int` | `mk_is_nan`: `result = m().mk_false(); return BR_DONE;` | -| `lemma_is_inf_to_fp_int_*` | `mk_is_inf_of_int` switch statement | -| `lemma_is_normal_to_fp_int` | `mk_is_normal`: `result = m().mk_and(not_zero, m().mk_not(inf_cond))` | -| `lemma_is_nan_ite` | `mk_is_nan`: ite-pushthrough block | -| `lemma_is_inf_ite` | `mk_is_inf`: ite-pushthrough block | -| `lemma_is_normal_ite` | `mk_is_normal`: ite-pushthrough block | +| Lemma | C++ macro | Used in | +|---|---|---| +| `lemma_fma_zero_nan_addend` | `FPA_REWRITE_FMA_ZERO_MUL` case (a) | `mk_fma` | +| `lemma_fma_zero_nan_mul` | `FPA_REWRITE_FMA_ZERO_MUL` case (b) | `mk_fma` | +| `lemma_fma_zero_inf_mul` | `FPA_REWRITE_FMA_ZERO_MUL` case (b) | `mk_fma` | +| `lemma_fma_zero_finite_decomposes` | `FPA_REWRITE_FMA_ZERO_MUL` case (c) | `mk_fma` | +| `lemma_fma_zero_const_addend` | `FPA_REWRITE_FMA_ZERO_MUL` case (c) | `mk_fma` | +| `lemma_fma_zero_const_*_arm` | `FPA_REWRITE_FMA_ZERO_MUL` case (d) | `mk_fma` | +| `lemma_fma_zero_general_*_arm` | `FPA_REWRITE_FMA_ZERO_MUL` case (e) | `mk_fma` | +| `lemma_fma_zero_product_sign` | `FPA_REWRITE_FMA_ZERO_MUL` sign computation | `mk_fma` | +| `lemma_is_nan_to_fp_int` | `FPA_REWRITE_IS_NAN_TO_FP_INT` | `mk_is_nan` | +| `lemma_is_inf_to_fp_int_*` | `FPA_REWRITE_IS_INF_TO_FP_INT` + `mk_is_inf_of_int` | `mk_is_inf` | +| `lemma_is_normal_to_fp_int` | `FPA_REWRITE_IS_NORMAL_TO_FP_INT` | `mk_is_normal` | +| `lemma_is_nan_ite` | `FPA_REWRITE_IS_NAN_ITE` | `mk_is_nan` | +| `lemma_is_inf_ite` | `FPA_REWRITE_IS_INF_ITE` | `mk_is_inf` | +| `lemma_is_normal_ite` | `FPA_REWRITE_IS_NORMAL_ITE` | `mk_is_normal` | ## IEEE 754 References diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index c2c888885..358a1c1f0 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "ast/rewriter/fpa_rewriter.h" +#include "ast/rewriter/fpa_rewriter_rules.h" #include "params/fpa_rewriter_params.hpp" #include "ast/ast_smt2_pp.h" @@ -430,6 +431,8 @@ br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg } } + FPA_REWRITE_FMA_ZERO_MUL(arg1, arg2, arg3, arg4, result); + return BR_FAILED; } @@ -588,6 +591,9 @@ br_status fpa_rewriter::mk_is_nan(expr * arg1, expr_ref & result) { return BR_DONE; } + FPA_REWRITE_IS_NAN_TO_FP_INT(arg1, result); + FPA_REWRITE_IS_NAN_ITE(arg1, result); + return BR_FAILED; } @@ -599,6 +605,9 @@ br_status fpa_rewriter::mk_is_inf(expr * arg1, expr_ref & result) { return BR_DONE; } + FPA_REWRITE_IS_INF_TO_FP_INT(arg1, result); + FPA_REWRITE_IS_INF_ITE(arg1, result); + return BR_FAILED; } @@ -610,6 +619,9 @@ br_status fpa_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { return BR_DONE; } + FPA_REWRITE_IS_NORMAL_TO_FP_INT(arg1, result); + FPA_REWRITE_IS_NORMAL_ITE(arg1, result); + return BR_FAILED; } @@ -844,3 +856,55 @@ br_status fpa_rewriter::mk_bvwrap(expr * arg, expr_ref & result) { return BR_FAILED; } + +// mk_is_inf_of_int: compute isInf(to_fp(rm, to_real(x))) as an integer constraint. +// For integer x, to_fp is never NaN or subnormal (IEEE 754-2019 §5.4.1), so +// the result is one of: ±zero, normal, or ±infinity. +// Overflow to ±infinity depends only on |x| relative to the format's +// representable range and the rounding mode. +// Corresponds to lemma_is_inf_to_fp_int_{rne,rna,rtp,rtn,rtz} in +// fstar/FPARewriterRules.fst. +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(); + + 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); + + 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((unsigned)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 boundary, MAX_FINITE has an odd significand so both RNE + // and RNA round away from MAX_FINITE, i.e. 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()); + 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 only; negative values round toward zero. + r = au.mk_gt(int_expr, au.mk_int(max_finite)); + break; + case MPF_ROUND_TOWARD_NEGATIVE: + // RTN: negative overflow only; positive values round toward zero. + r = au.mk_lt(int_expr, au.mk_int(-max_finite)); + break; + case MPF_ROUND_TOWARD_ZERO: + // RTZ: truncation toward zero never overflows to infinity. + r = m().mk_false(); + break; + } + + TRACE(fp_rewriter, tout << "isInf(to_fp(rm, int)) -> " << mk_ismt2_pp(r, m()) << "\n";); + return r; +} diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 333302eec..17d72ebc6 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -88,5 +88,10 @@ 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 used by FPA_REWRITE_IS_INF_TO_FP_INT and FPA_REWRITE_IS_NORMAL_TO_FP_INT: + // compute isInf(to_fp(rm, to_real(int_expr))) as a pure integer constraint. + // Corresponds to lemma_is_inf_to_fp_int_* in fstar/FPARewriterRules.fst. + expr_ref mk_is_inf_of_int(mpf_rounding_mode rm, unsigned ebits, unsigned sbits, expr * int_expr); }; diff --git a/src/ast/rewriter/fpa_rewriter_rules.h b/src/ast/rewriter/fpa_rewriter_rules.h new file mode 100644 index 000000000..e33c2898e --- /dev/null +++ b/src/ast/rewriter/fpa_rewriter_rules.h @@ -0,0 +1,296 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + fpa_rewriter_rules.h + +Abstract: + + Rewrite rule macros for floating-point arithmetic, extracted from + F* lemmas in fstar/FPARewriterRules.fst. + + Each macro is proved correct by one or more lemmas in that file; + the correspondence is documented at each macro definition. + + Macros are designed for use inside member functions of fpa_rewriter, + where m(), m_util, m_fm, and mk_is_inf_of_int are available. + Internal variables use the _fpa_ prefix to minimize name collisions. + +Author: + + (extracted from F* in fstar/FPARewriterRules.fst) + +Notes: + +--*/ +#pragma once + +// ----------------------------------------------------------------------- +// FPA_REWRITE_IS_NAN_TO_FP_INT +// +// F* lemma: lemma_is_nan_to_fp_int +// isNaN(to_fp(rm, real_or_int)) = false +// IEEE 754-2019 §5.4.1: converting a real or integer value never produces NaN. +// +// Applies to: mk_is_nan(arg1, result) +// ----------------------------------------------------------------------- +#define FPA_REWRITE_IS_NAN_TO_FP_INT(arg1, result) \ + do { \ + if (m_util.is_to_fp(arg1)) { \ + app * _fpa_a = to_app(arg1); \ + if (_fpa_a->get_num_args() == 2 && \ + (m_util.au().is_real(_fpa_a->get_arg(1)) || \ + m_util.au().is_int(_fpa_a->get_arg(1)))) { \ + result = m().mk_false(); \ + return BR_DONE; \ + } \ + } \ + } while (0) + + +// ----------------------------------------------------------------------- +// FPA_REWRITE_IS_NAN_ITE +// +// F* lemma: lemma_is_nan_ite +// isNaN(ite(c, t, e)) = ite(c, isNaN(t), isNaN(e)) +// When both branches are concrete FP numerals the rewriter evaluates +// the predicate statically and folds the result into the condition. +// +// Applies to: mk_is_nan(arg1, result) +// ----------------------------------------------------------------------- +#define FPA_REWRITE_IS_NAN_ITE(arg1, result) \ + do { \ + expr *_fpa_c = nullptr, *_fpa_t = nullptr, *_fpa_e = nullptr; \ + if (m().is_ite(arg1, _fpa_c, _fpa_t, _fpa_e)) { \ + scoped_mpf _fpa_vt(m_fm), _fpa_ve(m_fm); \ + if (m_util.is_numeral(_fpa_t, _fpa_vt) && m_util.is_numeral(_fpa_e, _fpa_ve)) { \ + result = m().mk_ite(_fpa_c, \ + m_fm.is_nan(_fpa_vt) ? m().mk_true() : m().mk_false(), \ + m_fm.is_nan(_fpa_ve) ? m().mk_true() : m().mk_false()); \ + return BR_REWRITE2; \ + } \ + } \ + } while (0) + + +// ----------------------------------------------------------------------- +// FPA_REWRITE_IS_INF_TO_FP_INT +// +// F* lemmas: lemma_is_inf_to_fp_int_rne, _rna, _rtp, _rtn, _rtz +// isInf(to_fp(rm, to_real(int))) = integer overflow condition +// Each rounding mode maps to a different threshold; computed by +// mk_is_inf_of_int (see fpa_rewriter.cpp). +// +// Applies to: mk_is_inf(arg1, result) +// ----------------------------------------------------------------------- +#define FPA_REWRITE_IS_INF_TO_FP_INT(arg1, result) \ + do { \ + mpf_rounding_mode _fpa_rm; \ + if (m_util.is_to_fp(arg1)) { \ + app * _fpa_a = to_app(arg1); \ + if (_fpa_a->get_num_args() == 2 && m_util.is_rm_numeral(_fpa_a->get_arg(0), _fpa_rm)) { \ + expr * _fpa_inner = _fpa_a->get_arg(1); \ + expr * _fpa_int_expr = nullptr; \ + if (m_util.au().is_to_real(_fpa_inner)) { \ + expr * _fpa_unwrapped = to_app(_fpa_inner)->get_arg(0); \ + if (m_util.au().is_int(_fpa_unwrapped)) \ + _fpa_int_expr = _fpa_unwrapped; \ + } \ + else if (m_util.au().is_int(_fpa_inner)) \ + _fpa_int_expr = _fpa_inner; \ + if (_fpa_int_expr) { \ + func_decl * _fpa_fd = _fpa_a->get_decl(); \ + unsigned _fpa_eb = _fpa_fd->get_parameter(0).get_int(); \ + unsigned _fpa_sb = _fpa_fd->get_parameter(1).get_int(); \ + result = mk_is_inf_of_int(_fpa_rm, _fpa_eb, _fpa_sb, _fpa_int_expr); \ + if (result) \ + return BR_REWRITE_FULL; \ + } \ + } \ + } \ + } while (0) + + +// ----------------------------------------------------------------------- +// FPA_REWRITE_IS_INF_ITE +// +// F* lemma: lemma_is_inf_ite +// isInf(ite(c, t, e)) = ite(c, isInf(t), isInf(e)) +// When both branches are concrete FP numerals the predicate is evaluated +// statically and folded into the condition. +// +// Applies to: mk_is_inf(arg1, result) +// ----------------------------------------------------------------------- +#define FPA_REWRITE_IS_INF_ITE(arg1, result) \ + do { \ + expr *_fpa_c = nullptr, *_fpa_t = nullptr, *_fpa_e = nullptr; \ + if (m().is_ite(arg1, _fpa_c, _fpa_t, _fpa_e)) { \ + scoped_mpf _fpa_vt(m_fm), _fpa_ve(m_fm); \ + if (m_util.is_numeral(_fpa_t, _fpa_vt) && m_util.is_numeral(_fpa_e, _fpa_ve)) { \ + result = m().mk_ite(_fpa_c, \ + m_fm.is_inf(_fpa_vt) ? m().mk_true() : m().mk_false(), \ + m_fm.is_inf(_fpa_ve) ? m().mk_true() : m().mk_false()); \ + return BR_REWRITE2; \ + } \ + } \ + } while (0) + + +// ----------------------------------------------------------------------- +// FPA_REWRITE_IS_NORMAL_TO_FP_INT +// +// F* lemma: lemma_is_normal_to_fp_int +// isNormal(to_fp(rm, to_real(int))) = int != 0 AND NOT isInf(to_fp(rm, int)) +// For integer inputs: never NaN, never subnormal, so the float is normal +// iff it is nonzero (int != 0) and does not overflow (NOT isInf). +// +// Applies to: mk_is_normal(arg1, result) +// ----------------------------------------------------------------------- +#define FPA_REWRITE_IS_NORMAL_TO_FP_INT(arg1, result) \ + do { \ + mpf_rounding_mode _fpa_rm; \ + if (m_util.is_to_fp(arg1)) { \ + app * _fpa_a = to_app(arg1); \ + if (_fpa_a->get_num_args() == 2 && m_util.is_rm_numeral(_fpa_a->get_arg(0), _fpa_rm)) { \ + expr * _fpa_inner = _fpa_a->get_arg(1); \ + expr * _fpa_int_expr = nullptr; \ + if (m_util.au().is_to_real(_fpa_inner)) { \ + expr * _fpa_unwrapped = to_app(_fpa_inner)->get_arg(0); \ + if (m_util.au().is_int(_fpa_unwrapped)) \ + _fpa_int_expr = _fpa_unwrapped; \ + } \ + else if (m_util.au().is_int(_fpa_inner)) \ + _fpa_int_expr = _fpa_inner; \ + if (_fpa_int_expr) { \ + func_decl * _fpa_fd = _fpa_a->get_decl(); \ + unsigned _fpa_eb = _fpa_fd->get_parameter(0).get_int(); \ + unsigned _fpa_sb = _fpa_fd->get_parameter(1).get_int(); \ + arith_util & _fpa_au = m_util.au(); \ + expr_ref _fpa_nz(m().mk_not(m().mk_eq(_fpa_int_expr, _fpa_au.mk_int(0))), m()); \ + expr_ref _fpa_ic = mk_is_inf_of_int(_fpa_rm, _fpa_eb, _fpa_sb, _fpa_int_expr); \ + result = m().mk_and(_fpa_nz, m().mk_not(_fpa_ic)); \ + return BR_REWRITE_FULL; \ + } \ + } \ + } \ + } while (0) + + +// ----------------------------------------------------------------------- +// FPA_REWRITE_IS_NORMAL_ITE +// +// F* lemma: lemma_is_normal_ite +// isNormal(ite(c, t, e)) = ite(c, isNormal(t), isNormal(e)) +// When both branches are concrete FP numerals the predicate is evaluated +// statically and folded into the condition. +// +// Applies to: mk_is_normal(arg1, result) +// ----------------------------------------------------------------------- +#define FPA_REWRITE_IS_NORMAL_ITE(arg1, result) \ + do { \ + expr *_fpa_c = nullptr, *_fpa_t = nullptr, *_fpa_e = nullptr; \ + if (m().is_ite(arg1, _fpa_c, _fpa_t, _fpa_e)) { \ + scoped_mpf _fpa_vt(m_fm), _fpa_ve(m_fm); \ + if (m_util.is_numeral(_fpa_t, _fpa_vt) && m_util.is_numeral(_fpa_e, _fpa_ve)) { \ + result = m().mk_ite(_fpa_c, \ + m_fm.is_normal(_fpa_vt) ? m().mk_true() : m().mk_false(), \ + m_fm.is_normal(_fpa_ve) ? m().mk_true() : m().mk_false()); \ + return BR_REWRITE2; \ + } \ + } \ + } while (0) + + +// ----------------------------------------------------------------------- +// FPA_REWRITE_FMA_ZERO_MUL +// +// F* lemmas: lemma_fma_zero_nan_addend, lemma_fma_zero_nan_mul, +// lemma_fma_zero_inf_mul, lemma_fma_zero_finite_decomposes, +// lemma_fma_zero_const_addend, lemma_fma_zero_const_{finite,nan_inf}_arm, +// lemma_fma_zero_general_{finite,nan_inf}_arm, lemma_fma_zero_product_sign +// +// 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-2019 §6.3: 0 * finite = ±0 (exact); 0 * inf = NaN. +// +// Case breakdown (mirroring the F* section-1 lemmas): +// (a) addend is NaN → NaN (lemma_fma_zero_nan_addend) +// (b) other_mul is concrete NaN or inf → NaN (lemma_fma_zero_nan_mul/inf_mul) +// (c) other_mul is concrete finite → fp.add(rm, product, addend) +// (lemma_fma_zero_finite_decomposes) +// (d) other_mul symbolic, addend concrete nonzero finite +// → ite(isFinite(other_mul), addend, NaN) +// (lemma_fma_zero_const_finite/nan_inf_arm) +// (e) fully symbolic → ite(isFinite(other_mul), +// fp.add(rm, product_zero, addend), NaN) +// (lemma_fma_zero_general_finite/nan_inf_arm) +// +// Applies to: mk_fma(arg1, arg2, arg3, arg4, result) +// arg1 = rounding mode, arg2 = x, arg3 = y, arg4 = addend +// ----------------------------------------------------------------------- +#define FPA_REWRITE_FMA_ZERO_MUL(arg1, arg2, arg3, arg4, result) \ + do { \ + mpf_rounding_mode _fpa_rm; \ + if (m_util.is_rm_numeral(arg1, _fpa_rm)) { \ + expr *_fpa_other = nullptr; \ + bool _fpa_zero_neg = false; \ + scoped_mpf _fpa_vzero(m_fm), _fpa_v3(m_fm); \ + if (m_util.is_numeral(arg2, _fpa_vzero) && m_fm.is_zero(_fpa_vzero)) { \ + _fpa_other = arg3; \ + _fpa_zero_neg = m_fm.is_neg(_fpa_vzero); \ + } \ + else if (m_util.is_numeral(arg3, _fpa_v3) && m_fm.is_zero(_fpa_v3)) { \ + _fpa_other = arg2; \ + _fpa_zero_neg = m_fm.is_neg(_fpa_v3); \ + m_fm.set(_fpa_vzero, _fpa_v3); \ + } \ + if (_fpa_other) { \ + TRACE(fp_rewriter, tout << "fma zero-multiplicand simplification\n";); \ + sort *_fpa_s = arg4->get_sort(); \ + expr_ref _fpa_nan(m_util.mk_nan(_fpa_s), m()); \ + if (m_util.is_nan(arg4)) { \ + result = _fpa_nan; \ + return BR_DONE; \ + } \ + scoped_mpf _fpa_vo(m_fm); \ + if (m_util.is_numeral(_fpa_other, _fpa_vo) && \ + (m_fm.is_nan(_fpa_vo) || m_fm.is_inf(_fpa_vo))) { \ + result = _fpa_nan; \ + return BR_DONE; \ + } \ + if (m_util.is_numeral(_fpa_other, _fpa_vo)) { \ + scoped_mpf _fpa_prod(m_fm); \ + m_fm.mul(_fpa_rm, _fpa_vzero, _fpa_vo, _fpa_prod); \ + SASSERT(m_fm.is_zero(_fpa_prod)); \ + result = m_util.mk_add(arg1, m_util.mk_value(_fpa_prod), arg4); \ + return BR_REWRITE2; \ + } \ + scoped_mpf _fpa_vz(m_fm); \ + if (m_util.is_numeral(arg4, _fpa_vz) && \ + !m_fm.is_zero(_fpa_vz) && !m_fm.is_nan(_fpa_vz)) { \ + expr_ref _fpa_fin_c(m()); \ + _fpa_fin_c = m().mk_not(m().mk_or(m_util.mk_is_nan(_fpa_other), \ + m_util.mk_is_inf(_fpa_other))); \ + result = m().mk_ite(_fpa_fin_c, arg4, _fpa_nan); \ + return BR_REWRITE_FULL; \ + } \ + expr_ref _fpa_pzero(m_util.mk_pzero(_fpa_s), m()); \ + expr_ref _fpa_nzero(m_util.mk_nzero(_fpa_s), m()); \ + expr_ref _fpa_prod_zero(m()); \ + if (_fpa_zero_neg) \ + _fpa_prod_zero = m().mk_ite(m_util.mk_is_negative(_fpa_other), \ + _fpa_pzero, _fpa_nzero); \ + else \ + _fpa_prod_zero = m().mk_ite(m_util.mk_is_negative(_fpa_other), \ + _fpa_nzero, _fpa_pzero); \ + expr_ref _fpa_fin_g(m()); \ + _fpa_fin_g = m().mk_not(m().mk_or(m_util.mk_is_nan(_fpa_other), \ + m_util.mk_is_inf(_fpa_other))); \ + result = m().mk_ite(_fpa_fin_g, \ + m_util.mk_add(arg1, _fpa_prod_zero, arg4), \ + _fpa_nan); \ + return BR_REWRITE_FULL; \ + } \ + } \ + } while (0)