mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-07 09:30:54 +00:00
Code Activity

fstar: address review comments - improve comments and table header clarity

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7899b653-a7f0-443c-894a-32376baea5c0

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

4
fstar/FPARewriterRules.fst
View file

@ -50,7 +50,7 @@ open IEEE754
(* ================================================================== *) (* ================================================================== *)
(* 1a. fma(rm, ±0, y, NaN) = NaN (* 1a. fma(rm, ±0, y, NaN) = NaN
Source: C++ line "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). *)
let lemma_fma_zero_nan_addend let lemma_fma_zero_nan_addend
(#eb #sb: pos) (#eb #sb: pos)
@ -381,7 +381,7 @@ let lemma_fma_zero_ite_nan_arm
else begin else begin
(* is_finite y = false && is_nan y = false. (* is_finite y = false && is_nan y = false.
By the transparent definition is_finite y = not (is_nan y) && not (is_inf y), By the transparent definition is_finite y = not (is_nan y) && not (is_inf y),
Z3 can derive is_inf y = true directly. *) the type-checker can derive is_inf y = true directly. *)
assert (is_inf y = true); assert (is_inf y = true);
ax_zero_mul_inf rm zero_val y; ax_zero_mul_inf rm zero_val y;
ax_fma_nan_mul rm zero_val y z ax_fma_nan_mul rm zero_val y z

4
fstar/README.md
View file

@ -9,7 +9,7 @@ in the [F\*](https://www.fstar-lang.org/) proof assistant.
PR #9038 adds three families of optimizations to `src/ast/rewriter/fpa_rewriter.cpp` PR #9038 adds three families of optimizations to `src/ast/rewriter/fpa_rewriter.cpp`
that avoid expensive FP bit-blasting: that avoid expensive FP bit-blasting:
| Optimization | C++ function | Formalized in | | Optimization | C++ function | F\* module and section |
|---|---|---| |---|---|---|
| `fma(rm, ±0, y, z)` zero-multiplicand decomposition | `mk_fma` | `FPARewriterRules.fst` §1 | | `fma(rm, ±0, y, z)` zero-multiplicand decomposition | `mk_fma` | `FPARewriterRules.fst` §1 |
| `isNaN/isInf/isNormal` applied to `to_fp(rm, to_real(int))` | `mk_is_nan`, `mk_is_inf`, `mk_is_normal`, `mk_is_inf_of_int` | `FPARewriterRules.fst` §2 | | `isNaN/isInf/isNormal` applied to `to_fp(rm, to_real(int))` | `mk_is_nan`, `mk_is_inf`, `mk_is_normal`, `mk_is_inf_of_int` | `FPARewriterRules.fst` §2 |
@ -54,7 +54,7 @@ Derived rewrite rules proved from `IEEE754.fst` axioms.
| `lemma_fma_zero_const_nan_inf_arm` | NaN/inf arm of the same `ite` | | `lemma_fma_zero_const_nan_inf_arm` | NaN/inf arm of the same `ite` |
| `lemma_fma_zero_general_finite_arm` | finite arm for fully symbolic `y` and `z` | | `lemma_fma_zero_general_finite_arm` | finite arm for fully symbolic `y` and `z` |
| `lemma_fma_zero_general_nan_inf_arm` | NaN/inf arm for fully symbolic `y` and `z` | | `lemma_fma_zero_general_nan_inf_arm` | NaN/inf arm for fully symbolic `y` and `z` |
| `lemma_fma_zero_product_sign` | sign of `fp_mul(rm, ±0, y)` = sign(±0) XOR sign(y) | | `lemma_fma_zero_product_sign` | sign of `fp_mul(rm, zero_val, y)` = sign(zero_val) XOR sign(y) |
| `lemma_fma_zero_ite_correct` | full composite: `fma(rm, ±0, y, z) = ite(is_finite(y), fp_add(rm, fp_mul(rm, ±0, y), z), NaN)` | | `lemma_fma_zero_ite_correct` | full composite: `fma(rm, ±0, y, z) = ite(is_finite(y), fp_add(rm, fp_mul(rm, ±0, y), z), NaN)` |
#### Section 2 — Classification of Integer-to-Float Conversions #### Section 2 — Classification of Integer-to-Float Conversions