Z3-Linq2Z3 — carnet 20 : points d'extension de réécriture (prédicat et global) du DSL du fork #22733

Z3-Linq2Z3 — carnet 20 : points d'extension de réécriture (prédicat et global) du DSL du fork

Pourquoi ce carnet (le trou, mesuré)

Part of #17073 (campagne d'audit longue). Suite directe du carnet 19 (#22712) dont le body déclarait : « les points d'extension de réécriture ([TheoremPredicateRewriter], [TheoremGlobalRewriter], également 0 occurrence au dépôt) sont un grain distinct — carnet 20 ».

Mesure de l'absence sur origin/main et dans le sous-module (26/10) :

• les deux interfaces ITheoremPredicateRewriter / ITheoremGlobalRewriter et leurs attributs existent dans le fork (solutions/Z3.Linq/ExpressionVisitor.cs:643-675, Theorem.cs:613-650) ;
• aucun carnet du dépôt ne les exerce, aucun demo du fork (demos/*.cs) ne les utilise ;
• TheoremUndecidedException (le refus DSL qui force une solution) est le seul mécanisme de refus documenté, la réécriture est la capacité d'extension qui permet d'exprimer un prédicat métier que le traducteur ne comprend pas.

Objet du carnet

MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/20_Theorem_Rewriters.ipynb — sujet unique : étendre le DSL en réécrivant les contraintes avant traduction Z3.

Deux mécanismes, sur des instances autonomes (pas de corpus externe) :

1. Réécriture de prédicat : une méthode C# annotée [TheoremPredicateRewriter(typeof(...))] dont les appels sont remplacés par une expression que le traducteur comprend. Instance : prédicat métier EstPair(int) / Entre(int,int,int) non traduisibles directement, réécrits en x % 2 == 0 / conjonction. Témoin négatif : le rewriter qui renvoie son entrée est rejeté (InvalidOperationException « did not perform any rewrite ») — mesuré, dans les sorties.
2. Réécriture globale : un environnement annoté [TheoremGlobalRewriter(typeof(...))] qui reçoit toutes les contraintes du théorème et en retourne l'ensemble à asserter (ajout/suppression/remplacement). Instance : déduplication ou injection d'une contrainte de domaine commune, vérifiée sur un théorème à plusieurs contraintes. Le même chemin alimente Explain (GetConstraintsToAssert partagé solve/Explain, Theorem.cs:620-622) — la cohérence diagnostic/solveur est montrée, pas seulement affirmée.

Acceptance — mesurable dans les sorties committées

1. Carnet créé, exécuté de bout en bout sur .net-csharp (cell-by-cell MCP, pas papermill), execution_count non nuls, 0 erreur de cellule, sorties committées (C.1/C.2), banner probeAddresses strippé post-exec (strip_probe_banner.py).
2. Discrimination hors timing, falsifiable : (a) un prédicat que le traducteur seul ne sait pas traduire est résolu grâce au rewriter (preuve de la grille/solution obtenue) ; (b) le rewriter identité est refusé avec l'exception attendue ; (c) un rewriter global qui supprime une contrainte change le verdict du théorème (SAT là où l'original était UNSAT, ou témoin différent mesuré).
3. Les deux mécanismes sont distingués dans la prose : portée (un appel de méthode vs l'ensemble des contraintes), point d'accroche (méthode vs type d'environnement), moment (à la traduction vs avant assertion), exigence du constructeur public sans paramètre.
4. ≥3 exercices C.1 (stubs sans erreur volontaire, # TODO conservés, exécution complète même non complétés).
5. Chargement du fork via .deploy/ (même convention que 01-06, script z3-build-deploy), cohérence avec la série ; ligne README de série différée après merge de Docs(20975): resorption compteurs prose README -- tranche SymbolicAI hors Lean (15 fichiers) #22624 (même garde que Z3-Linq2Z3 — carnet 19 : B10, solveur et chaine de tactiques configurables (deux stacks sur le Sudoku 9x9) #22712).
6. Une PR = un sujet : pas de correction du fork, pas de carnet 19, pas de README de série.

Hors périmètre

• Aucune modification du sous-module (une correction de rewriter se ferait dans MyIntelligenceAgency/Z3.Linq, PR séparée).
• Pas de SolverKind/.Logic/.Tactics : c'est le carnet 19 (Z3-Linq2Z3 — carnet 19 : B10, solveur et chaine de tactiques configurables (deux stacks sur le Sudoku 9x9) #22712, PR Add(z3linq2z3,#22712): carnet 19 -- B10, solveur et chaine de tactiques configurables #22724).
• Pas de nouvelle capacité : on démontre l'existant, on ne ré-implémente pas le traducteur (organ-first : le fork possède l'organe, le carnet l'invoque).