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: address code review - diagnostic on bvar fallback, refactor extractions, fix include path

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/c7b6d01e-b309-4d67-93bb-f6bad4d79b75

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

9
fstar/README.md
View file

@ -137,10 +137,13 @@ The three `let _ = run_tactic ...` blocks at the bottom of the file
demonstrate extraction for the three ite-pushthrough lemmas and print
their generated C++ to stdout during F* typechecking.
### `../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.
C++ header containing one `#define` macro per rewrite rule, whose correctness
is proved by F* lemmas in `FPARewriterRules.fst`. The ite-pushthrough macros
(`FPA_REWRITE_IS_NAN_ITE`, `FPA_REWRITE_IS_INF_ITE`, `FPA_REWRITE_IS_NORMAL_ITE`)
can be regenerated by running `RewriteCodeGen.fst`. Each macro is annotated
with an `[extract: MACRO_NAME]` comment in the corresponding F* lemma.
| Macro | F\* lemma(s) | Used in C++ function |
|---|---|---|

30
fstar/RewriteCodeGen.fst
View file

@ -105,7 +105,13 @@ let bvar_name (idx_map: list (nat & string)) (t: term) : Tac (option string) =
let bvv = inspect_bv bv in
(match List.Tot.assoc #nat bvv.index idx_map with
| Some n -> Some n
| None -> Some (FStar.Sealed.unseal bvv.ppname)) (* fallback *)
| None ->
(* de Bruijn index not in our map; use the printer name as a fallback
and warn so the caller knows the index map may be incomplete. *)
let pp = FStar.Sealed.unseal bvv.ppname in
print ("WARNING: bvar_name fallback for index "
^ string_of_int bvv.index ^ ", using ppname '" ^ pp ^ "'");
Some pp)
| _ -> None
(* Detect if-then-else in reflected terms.
@ -425,18 +431,16 @@ let extract_rewrite (lemma: term) : Tac string =
open FPARewriterRules
(* Demonstrate extraction of the three ite-pushthrough lemmas. *)
let _ =
run_tactic (fun () ->
print "\n=== lemma_is_nan_ite ===\n";
print (extract_rewrite (quote lemma_is_nan_ite)))
(* Helper: extract and print one lemma's C++ rewrite rule. *)
let print_rewrite (label: string) (lemma: term) : Tac unit =
print ("\n=== " ^ label ^ " ===\n");
print (extract_rewrite lemma)
(* Demonstrate extraction of the three ite-pushthrough lemmas.
Running this file with F* prints the generated C++ for each rule. *)
let _ =
run_tactic (fun () ->
print "\n=== lemma_is_inf_ite ===\n";
print (extract_rewrite (quote lemma_is_inf_ite)))
let _ =
run_tactic (fun () ->
print "\n=== lemma_is_normal_ite ===\n";
print (extract_rewrite (quote lemma_is_normal_ite)))
List.Tot.iter (fun (label, lemma) -> print_rewrite label lemma)
[ ("lemma_is_nan_ite", quote lemma_is_nan_ite);
("lemma_is_inf_ite", quote lemma_is_inf_ite);
("lemma_is_normal_ite", quote lemma_is_normal_ite) ])

6
src/ast/rewriter/fpa_rewriter_rules.h
View file

@ -12,10 +12,10 @@ Abstract:
The ite-pushthrough macros (FPA_REWRITE_IS_NAN_ITE, FPA_REWRITE_IS_INF_ITE,
FPA_REWRITE_IS_NORMAL_ITE) can be regenerated programmatically by running
the Meta-F* extraction tactic in fstar/RewriteCodeGen.fst:
the Meta-F* extraction tactic in fstar/RewriteCodeGen.fst (from the repo root):
fstar.exe --include fstar fstar/IEEE754.fst \
fstar/FPARewriterRules.fst fstar/RewriteCodeGen.fst
cd /path/to/z3/fstar
fstar.exe --include . IEEE754.fst FPARewriterRules.fst RewriteCodeGen.fst
The correspondence between each macro and the F* lemma it implements is
documented at each macro definition below.