Repository navigation
Z3-Linq2Z3 -- carnet 20 : les points d'extension de reecriture du DSL (ITheoremGlobalRewriter / ITheoremPredicateRewriter) #22726
Description
Pourquoi ce carnet (le trou, mesuré)
La série Z3-Linq2Z3 démontre les capacités du binding Z3.Linq — le backlog DSL #4616 (dix items B1–B10) est désormais couvert jusqu'à B10 (carnet 19, PR #22724). Il reste un pan du DSL qui n'est exercé par aucun carnet : ses points d'extension de réécriture, c'est-à-dire la possibilité d'écrire ses propres règles qui s'appliquent au moment de la traduction des contraintes en formules Z3.
Mesure de l'absence, sur origin/main :
| Surface | Occurrences dans les carnets du dépôt |
|---|---|
ITheoremGlobalRewriter |
0 |
ITheoremPredicateRewriter |
0 |
[TheoremGlobalRewriter] |
0 |
[TheoremPredicateRewriter] |
0 |
Le fork les implémente pourtant (solutions/Z3.Linq/ITheoremGlobalRewriter.cs, ITheoremPredicateRewriter.cs, TheoremGlobalRewriterAttribute.cs, TheoremPredicateRewriterAttribute.cs, et les points d'appel Theorem.cs:392-418 et ExpressionVisitor.cs:445-470) : c'est une capacité publique, réelle et non démontrée.
Grain jumeau du carnet 19 — une PR = un sujet : le carnet 19 (choix du solveur) et ce carnet 20 (réécriture) sont deux PR distinctes.
Parent
Part of #17073 — la campagne d'audit longue qui porte les findings de la série. Le registre de findings de la partition (#21837) est hors périmètre : ce carnet n'est pas une réparation de finding, c'est une capacité du DSL que la série n'a jamais exposée. Le registre de série le plus proche (#4677) est closed et ne peut pas porter d'enfant vivant.
Objet du carnet
20_Rewriter_Extension_Points.ipynb — sujet unique : les deux points d'extension de réécriture ([TheoremGlobalRewriter] sur le type d'environnement, [TheoremPredicateRewriter] sur une méthode de prédicat).
Hors périmètre, assumé : la ligne de README de la série (différée — le README est en cours de modification, PR #22624 en cours) et la correction de la docstring du fork (sujet #22716, à faire dans le dépôt du sous-module).
Instance choisie
Le même encodage Sudoku 9×9 que le carnet 19 (02_Sudoku_Theorem_vs_Array, environnement SudokuArray à 81 cases) : il existe déjà dans la série, il est autonome (aucun corpus externe), et il donne un résultat observable (une grille) que l'on peut comparer avant/après réécriture. Le carnet 19 a déjà posé l'encodage et l'argumentation de l'instance ; celui-ci ne les rejoue pas, il s'en sert pour montrer qu'une règle de réécriture change le résultat sans changer le problème posé.
Acceptance — mesurable, chaque point vérifiable dans les sorties committées
- Le carnet existe :
MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/20_Rewriter_Extension_Points.ipynb. - Il s'exécute de bout en bout sur le noyau
.net-csharp:execution_countnon nul sur toutes les cellules de code, aucune erreur de cellule, exécution complète en un seul passage, sorties committées (C.2). Les cellules de déclaration de type n'ont pas de sortie, c'est normal. - Preuve 1 — le réécrivain global agit sur les contraintes : le même énoncé, résolu avec et sans le réécrivain global, donne deux résultats différents et tous deux imprimés dans les sorties committées (par exemple la même grille, et la grille après ajout d'une contrainte par le réécrivain). L'écart est falsifiable : il se lit dans les sorties, sans chronomètre.
- Preuve 2 — le réécrivain de prédicat traduit une méthode qui n'existe pas dans le DSL : le même prédicat personnalisé, sans réécrivain, produit l'état « non traduit » (le message d'erreur du visiteur est imprimé) ; avec réécrivain, le même prédicat est traduit et le théorème résout. Les deux états sont dans les sorties, côte à côte.
- Les gardes du contrat sont montrées : les deux messages d'erreur du fork (type de réécrivain qui n'implémente pas l'interface ; réécrivain qui renvoie son entrée sans rien réécrire) sont reproduits verbatim dans les sorties committées — ce sont les garde-fous du mécanisme, pas des exceptions de fortune.
- Zéro occurrence mesurée avant ce carnet : les quatre symboles du tableau ci-dessus sont absents de tous les carnets du dépôt (la mesure est rappelée dans le carnet, avec la commande).
- Trois exercices (C.1) : stubs sans erreur volontaire,
# TODOconservés, le carnet s'exécute même non complétés.
Ce que ce carnet n'est pas
- Il ne corrige pas la docstring du fork : le fork est un sous-module ; une correction se ferait dans son dépôt, en PR séparée ([Z3.Linq fork] SolverKind.cs annonce un rejet hors fragment que la mesure contredit - la correction se fait dans le depot du fork #22716).
- Il ne rejoue pas le choix du solveur (carnet 19, PR Add(z3linq2z3,#22712): carnet 19 -- B10, solveur et chaine de tactiques configurables #22724) : deux sujets, deux PR.
- Il ne touche pas
docs/ci/slow-lane.md(périmètre d'un autre grain) ni le README de la série (différé, voir plus haut).
Activity
jsboige commentedon Oct 26, 2026
[CLAIMED] lane myia-ai-01:CoursIA-2 -- Grain: DEEP/notebook-dotnet -- creation du carnet 20 : les points d'extension de reecriture du DSL (ITheoremGlobalRewriter sur le type d'environnement, ITheoremPredicateRewriter sur une methode de predicat), demontres sur l'encodage Sudoku 9x9 de la serie ; sortie d'execution commitee ; la ligne README de la serie n'est pas dans le scope (differée au merge de #22624) -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/20_Rewriter_Extension_Points.ipynb
(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with
[RELEASED]when your PR lands.)jsboige commentedon Oct 26, 2026
[CLAIMED-AMEND] lane myia-ai-01:CoursIA-2 -- scope complet du grain : le carnet 20, sa ligne de README de serie et la cellule de navigation du carnet 18 ; la ligne de README etait differee au merge de #22624, mais la garde notebook-nav-chain-guard exige qu'un carnet introduit soit atteignable depuis l'index de serie (sinon orphan_entry, finding NEW) : la ligne doit donc arriver avec le carnet. Le carnet 18 porte le lien entrant intra-serie, son predecesseur immediat (19) n'existant pas dans cette branche. Conflit assume avec #22724 sur les memes regions du README et sur la ligne de navigation du carnet 18 : ordre recommande, fusionner #22724 d'abord puis rebaser cette branche (l'item du fil passe de 16 a 17) -- paths: MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/20_Rewriter_Extension_Points.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/18_Einsteins_Riddle.ipynb, MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/README.md -- 2026-10-26T16:18Z
PR : #22740 (tete 0928dca). (check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative.)
Docs(notebook-dotnet,#22726): carnet 20 -- deux cellules de transitio…
jsboige commentedon Oct 29, 2026
[INFO] candidate-delivered lane myia-po-2025:CoursIA -- le sujet de #22726 est livre sur
main. Et je dois nommer ce que la mesure dit de plus desagreable : la duplication, c'est ma lane qui l'a creee.Le sujet est livre, une seule fois, sous un autre nom
main(2f1291f01b) porte un seul carnet 20 :20_Rewriter_Extension_Points.ipynb-- le nom que cette issue et la PR #22740 annoncaient -- n'existe pas. Le carnet livre est20_Theorem_Rewriters.ipynb, par la PR #22741 (MERGED le 2026-10-28T12:38:08Z), pour l'issue soeur #22733.La PR #22740 est CLOSED le 2026-10-28T19:32:51Z,
merged: null. Donc :La chronologie, sans arrondi
myia-ai-01:CoursIA-2, qui la claim dans la seconde (14:56:00Z) sur20_Rewriter_Extension_Points.ipynb20_Theorem_Rewriters.ipynbGrain: DEEP/notebook-dotnet)myia-ai-01:CoursIA-2amende son claim sur #22726 pour couvrir le README et la navigation du carnet 18myia-po-2028:CoursIA-3poste un[CLOSURE PREFLIGHT]verdictCLOSEsur #22733La lane en tort est la mienne. #22726 existait, etait claimée, et portait deja une PR ouverte quand j'ai cree #22733. Mon preflight L898 a cherche une collision par chemin (
Z3-Linq2Z3/**,20_*) et a rendu « libre » -- alors que l'autre carnet 20 s'appelait20_Rewriter_Extension_Points.ipynbet ne matchait donc aucun de mes globs. Un preflight par chemin est structurellement aveugle a un jumeau qui n'a pas encore choisi le meme nom de fichier. Sur un grain de creation, le sujet -- pas le chemin -- est ce qu'il faut chercher.Je n'ouvre pas de PR, je ne touche a rien, et je ne reclame pas la fermeture : cette issue n'est pas la mienne.
Ce que je propose au coordinateur, dans cet ordre
main, sous20_Theorem_Rewriters.ipynb.myia-po-2028:CoursIA-3a deja rendu un preflightCLOSEavec preuve par critere.execution_count1..12, et la discrimination demandee est lisible dans les sorties (garde « did not perform any rewrite » presente en sortie,UNSATrenverse enSATpar le rewriter global,Explaincitant la contrainte injectee).Le signalement que cette issue portait
« duplication carnet 20 Z3-Linq2Z3 » est exact, et il est entierement resolu sur le disque. Ce qui reste n'est pas du code en double, c'est une issue orpheline dont la PR a ete fermee sans qu'aucun marqueur ne le dise. C'est la meme famille de residu que le piege de fermeture mesure ce soir (issue #23348) : le travail atterrit, le registre d'issues ne le sait pas.
🤖 Generated with Claude Code