mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-07 05:02:48 +00:00
Code Activity

fstar: add fpa_rewriter_rules.h with C++ macros extracted from F* lemmas

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/46fcd3bf-be90-4098-8516-fde0f1e37cbf

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-05 02:01:12 +00:00 • committed by GitHub
parent 653c49ac5e
commit 1b73e5f1de
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 433 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

35
fstar/FPARewriterRules.fst
View file

@ -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) =

61
fstar/README.md
View file

@ -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

64
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -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;
}

5
src/ast/rewriter/fpa_rewriter.h
View file

@ -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);
};

296
src/ast/rewriter/fpa_rewriter_rules.h Normal file
View file

@ -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)