From fc8b6899d8c0d27fa0c5f9ad8fbd93a7dc1944ef Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 15 Oct 2026 10:54:25 +0000 Subject: [PATCH 1/3] Fix(accents,#16638): z3-python-04-strings-regex, z3-python-06-advanced-optimization + Z3-16e-Meal-Planner-Optimize-Python.ipynb -- detache de #20785 (seuil de 15 fichiers) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Partie de la PR #20785 detachee pour la ramener sous le seuil de 15 fichiers (pr-review-discipline §A). Fichiers repris a l'identique de sa tete 42883a9ffb ; aucun n'a change sur main depuis sa base de fusion 1cef8a5502, donc les attestations jumelles restent valides. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01LRbWZZHE9jZscr8ya3niWA --- .../Z3-API/Z3-04-Strings-Regex-CSharp.ipynb | 2 +- .../Z3-06-Advanced-Optimization-CSharp.ipynb | 20 +++++++++---------- .../Z3-16e-Meal-Planner-Optimize-Python.ipynb | 12 +++++------ .../z3-python-04-strings-regex.yaml | 1 + ...0-14-hors-flotte-claude-session-16638.yaml | 6 ++++++ .../z3-python-06-advanced-optimization.yaml | 1 + ...0-14-hors-flotte-claude-session-16638.yaml | 6 ++++++ 7 files changed, 31 insertions(+), 17 deletions(-) create mode 100644 scripts/notebook_tools/twin_pairs.d/z3-python-04-strings-regex/0009-2026-10-14-hors-flotte-claude-session-16638.yaml create mode 100644 scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization/0007-2026-10-14-hors-flotte-claude-session-16638.yaml diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-04-Strings-Regex-CSharp.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-04-Strings-Regex-CSharp.ipynb index 0051897044..a29cc9f81f 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-04-Strings-Regex-CSharp.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-04-Strings-Regex-CSharp.ipynb @@ -24,7 +24,7 @@ "\n", "## Plan\n", "\n", - "1. Creation de chaînes, `Length`, `MkExtract`, concatenation.\n", + "1. Création de chaînes, `Length`, `MkExtract`, concatenation.\n", "2. Recherche et substitution : `MkIndexOf`, `MkReplace`.\n", "3. Trouver une chaîne sous contraintes (`MkPrefixOf`, `MkSuffixOf`, `MkContains`).\n", "4. Construction d'expressions regulieres (`MkToRe`, `MkRange`, `MkPlus`, `MkStar`).\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-06-Advanced-Optimization-CSharp.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-06-Advanced-Optimization-CSharp.ipynb index c342c63869..8984bec53b 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-06-Advanced-Optimization-CSharp.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-06-Advanced-Optimization-CSharp.ipynb @@ -254,7 +254,7 @@ "| Planification | Satisfaction des préférences | Cout horaire |\n", "| Ingenierie | Performance | Consommation energetique |\n", "\n", - "On ne peut pas « maximiser A et minimiser B » simultanement de facon absolue : il faut choisir une stratégie de compromis. Z3 offre trois approches complementaires :\n", + "On ne peut pas « maximiser A et minimiser B » simultanement de facon absolue : il faut choisir une stratégie de compromis. Z3 offre trois approches complémentaires :\n", "\n", "1. **Priorites hiérarchiques** (section 2) : chaque contrainte souple a un poids, on minimise la somme ponderee des violations.\n", "2. **Objectifs multiples lexicographiques** (section 3) : on optimise les objectifs les uns après les autres, par ordre de priorite.\n", @@ -494,7 +494,7 @@ "| Penalite | `ctx.MkITE(r_i, ctx.MkInt(poids), ctx.MkInt(0))` | Contribution au cout total si violation |\n", "| Objectif | `opt.MkMinimize(cout_total)` | Minimiser la somme des penalites |\n", "\n", - "**Points cles** :\n", + "**Points clés** :\n", "1. Les contraintes a **poids eleve** sont prioritaires : Z3 prefere violer plusieurs contraintes a faible poids qu'une seule a poids eleve.\n", "2. Toutes les contraintes dures sont satisfaites par construction (elles sont ajoutees avec `opt.Assert` sans relaxation).\n", "3. Le cout total obtenu est le **minimum** : aucune autre assignation ne donne une somme ponderee de violations inferieure.\n", @@ -696,14 +696,14 @@ "source": [ "### Quand lexicographique differe vraiment de la somme ponderee\n", "\n", - "L'exemple precedent convergeait : maximiser le revenu *puis* minimiser le cout donnait le meme resultat qu'un seul objectif (profit net), parce que les deux objectifs etaient monotones dans la meme variable `q`. La machinerie lexicographique de Z3 (`MkMaximize` puis `MkMinimize`, par ordre de declaration) n'etait donc pas *visible* dans la sortie.\n", + "L'exemple précédent convergeait : maximiser le revenu *puis* minimiser le cout donnait le même résultat qu'un seul objectif (profit net), parce que les deux objectifs etaient monotones dans la même variable `q`. La machinerie lexicographique de Z3 (`MkMaximize` puis `MkMinimize`, par ordre de declaration) n'etait donc pas *visible* dans la sortie.\n", "\n", - "Voici un cas ou les deux strategies **divergent** : un catalogue de deux produits partageant une capacite de production, dont l'un est un *loss-leader* (fort revenu brut, mais vendu a perte).\n", + "Voici un cas ou les deux stratégies **divergent** : un catalogue de deux produits partageant une capacite de production, dont l'un est un *loss-leader* (fort revenu brut, mais vendu a perte).\n", "\n", "- **Produit premium** : revenu 8 EUR/unite, cout 10 EUR/unite (perte de 2 EUR/unite).\n", "- **Produit standard** : revenu 3 EUR/unite, cout 1 EUR/unite (profit de 2 EUR/unite).\n", "\n", - "Un objectif de *chiffre d'affaires brut* pousse vers le premium ; un objectif de *profit net* pousse vers le standard. Le compromis est ici reel, et le choix strategique (priorite au CA vs priorite au profit) change la solution optimale -- c'est exactement ce que l'optimisation lexicographique permet de formaliser, et que la somme ponderee, elle, melange." + "Un objectif de *chiffre d'affaires brut* pousse vers le premium ; un objectif de *profit net* pousse vers le standard. Le compromis est ici reel, et le choix stratégique (priorite au CA vs priorite au profit) change la solution optimale -- c'est exactement ce que l'optimisation lexicographique permet de formaliser, et que la somme ponderee, elle, melange." ] }, { @@ -825,7 +825,7 @@ "| **Ponderee** (section 2) | Minimise la somme ponderee des violations | Compromis souhaites entre objectifs |\n", "| **Pareto** (section 4) | Enumere tous les compromis optimaux | Pas de priorite naturelle, decision humaine |\n", "\n", - "**Points cles** :\n", + "**Points clés** :\n", "1. `handle.Upper` donne la valeur optimale d'un objectif `MkMaximize` ; `handle.Lower` pour `MkMinimize` (caster le `Expr` retourne en `IntNum`).\n", "2. L'ordre de declaration des `MkMaximize`/`MkMinimize` définit la **priorite lexicographique**.\n", "3. L'approche lexicographique n'est **pas equivalente** a maximiser une somme ponderee : elle impose une hiérarchie stricte.\n", @@ -1150,7 +1150,7 @@ "| 2 | Ajouter `cout < cout_precedent`, re-maximiser | Point avec cout plus bas |\n", "| 3 | Repeter jusqu'a `UNSATISFIABLE` | Front complet |\n", "\n", - "**Points cles** :\n", + "**Points clés** :\n", "1. Le front de Pareto contient les **compromis optimaux** : aucun point n'est domine par un autre.\n", "2. Le nombre de points est fini (domains entiers petits), mais peut etre grand si les ranges sont larges.\n", "3. Cette méthode d'enumeration par exclusion successive est simple mais couteuse : a chaque itération, on ajoute une contrainte. Pour de grands fronts, on prefere des algorithmes specialises.\n", @@ -1451,10 +1451,10 @@ "| Compteur | `ctx.MkITE(r_i, 1, 0)` | Contribution unitaire au nombre de violations |\n", "| Objectif | `opt.MkMinimize(nb_violations)` | Maximiser le nombre de préférences satisfaites |\n", "\n", - "**Points cles** :\n", + "**Points clés** :\n", "1. Le problème MaxSAT est un cas particulier d'optimisation ponderee ou tous les poids sont egaux a 1.\n", "2. Les variables de relaxation `Bool` sont l'outil central : elles « absorbent » les violations impossibles a eviter.\n", - "3. `ctx.MkDistinct` impose que toutes les valeurs soient distinctes (equivalent AllDifferent).\n", + "3. `ctx.MkDistinct` impose que toutes les valeurs soient distinctes (équivalent AllDifferent).\n", "4. Si on avait donne des **poids différents** aux préférences, Z3 aurait privilege les préférences a poids eleve (retour a la section 2).\n", "\n", "> **Note technique (.NET)** : `opt.AssertSoft(BoolExpr c, uint weight, string group)` est la forme native du MaxSAT pondere dans Microsoft.Z3 : les contraintes d'un même `group` s'agregent, et Z3 minimise la somme ponderee des violations. Le codage manuel ci-dessus reste transparent ; `AssertSoft` est le raccourci idiomatique. MaxSAT est un domaine de recherche actif : Z3 utilise un algorithme de recherche dichotomique sur le nombre de violations pour converger rapidement vers l'optimum." @@ -1491,7 +1491,7 @@ "\n", "- `# Indice` : pour chaque préférence, créez une variable de relaxation `Bool` et ajoutez `ctx.MkOr(slot[item] == slot_pref, r)`.\n", "- `# Étape 1` : declarer `slot = new IntExpr[nItems]` avec bornes `[0, nSlots-1]`.\n", - "- `# Étape 2` : contrainte dure d'injectivite : `ctx.MkDistinct(slot)` (ou equivalent si `nItems < nSlots`).\n", + "- `# Étape 2` : contrainte dure d'injectivite : `ctx.MkDistinct(slot)` (ou équivalent si `nItems < nSlots`).\n", "- `# Étape 3` : pour chaque `(item, pref)`, créer `r = ctx.MkBoolConst(...)`, ajouter `ctx.MkOr(ctx.MkEq(slot[item], ctx.MkInt(pref)), r)`.\n", "- `# Étape 4` : minimiser la somme des `ctx.MkITE(r, 1, 0)`.\n", "- `# Étape 5` : extraire l'assignation et le nombre de préférences satisfaites." diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-16e-Meal-Planner-Optimize-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-16e-Meal-Planner-Optimize-Python.ipynb index 15222762f9..bebb48fce9 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-16e-Meal-Planner-Optimize-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-16e-Meal-Planner-Optimize-Python.ipynb @@ -734,11 +734,11 @@ "source": [ "### 6b. Le jouet a l'echelle : le plan hebdomadaire a cout minimal (24 plats, D=7)\n", "\n", - "La **section 5** du [16](Z3-16-Meal-Planner-Python.ipynb) a resolu le plan hebdomadaire avec un `Solver()` (recherche de **faisabilite** : une grille valide suffit). C'est passer a cote de la capacite signature de Z3 : l'**optimisation** sous contraintes via `Optimize()`. On veut desormais le plan hebdomadaire **le moins cher**, en respectant fenetre kcal + apport proteique + variete (chaque plat au plus 2 fois dans la semaine).\n", + "La **section 5** du [16](Z3-16-Meal-Planner-Python.ipynb) a resolu le plan hebdomadaire avec un `Solver()` (recherche de **faisabilite** : une grille valide suffit). C'est passer a cote de la capacite signature de Z3 : l'**optimisation** sous contraintes via `Optimize()`. On veut desormais le plan hebdomadaire **le moins cher**, en respectant fenêtre kcal + apport proteique + variete (chaque plat au plus 2 fois dans la semaine).\n", "\n", - "On met aussi le probleme a l'echelle : un corpus de **24 plats** (vs 9) et un plan sur **D=7 jours** (la semaine complete, vs 3). C'est le \"probleme riche\" (Prong-B) ou un glouton \"jour par jour\" echoue : minimiser le cout de chaque jour **independamment** violente la contrainte de variete hebdomadaire (les plats les moins chers reviennent trop souvent) et le couplage des apports proteiques. Le `minimize` de Z3, lui, optimise le **cout global de la semaine** en considerant toutes les contraintes simultanement.\n", + "On met aussi le problème a l'echelle : un corpus de **24 plats** (vs 9) et un plan sur **D=7 jours** (la semaine complete, vs 3). C'est le \"problème riche\" (Prong-B) ou un glouton \"jour par jour\" echoue : minimiser le cout de chaque jour **independamment** violente la contrainte de variete hebdomadaire (les plats les moins chers reviennent trop souvent) et le couplage des apports proteiques. Le `minimize` de Z3, lui, optimise le **cout global de la semaine** en considerant toutes les contraintes simultanement.\n", "\n", - "> Miroir \"Python-large\" de l'Epic #1206 : le corpus de 24 plats est un modele d'echelle (noms reels, kcal/proteines/couts realistes) du corpus RecipeML (~11 000 recettes). Le chemin vers les vraies donnees (`download_meal_data.py` : Ciqual ANSES 2025 + RecipeML) est un effort separe multi-jours ; ici on demontre la capacite d'optimisation SMT sur un tableau imbrique (jours x plats) a une echelle pedagogique bornee.\n" + "> Miroir \"Python-large\" de l'Epic #1206 : le corpus de 24 plats est un modèle d'echelle (noms reels, kcal/proteines/couts realistes) du corpus RecipeML (~11 000 recettes). Le chemin vers les vraies données (`download_meal_data.py` : Ciqual ANSES 2025 + RecipeML) est un effort separe multi-jours ; ici on demontre la capacite d'optimisation SMT sur un tableau imbrique (jours x plats) a une echelle pedagogique bornee.\n" ] }, { @@ -891,11 +891,11 @@ "source": [ "### Interpretation 5b — pourquoi le glouton ne trouve pas l'optimum global\n", "\n", - "Un glouton \"jour par jour\" choisirait, pour chaque jour, les 3 plats les moins chers satisfaisant la fenetre kcal — mais il **ignorerait le couplage hebdomadaire** : apres 2 repetitions, les plats les moins chers deviennent indisponibles (contrainte de variete), et le glouton se retrouve bloque ou contraint de prendre des plats chers en fin de semaine, sans avoir anticipe. Le `Optimize()` de Z3, lui, minimise le **cout total sur les 7 jours simultanement** : il repartit les repetitions bon marche sur toute la semaine pour minimiser la somme globale.\n", + "Un glouton \"jour par jour\" choisirait, pour chaque jour, les 3 plats les moins chers satisfaisant la fenêtre kcal — mais il **ignorerait le couplage hebdomadaire** : après 2 repetitions, les plats les moins chers deviennent indisponibles (contrainte de variete), et le glouton se retrouve bloque ou contraint de prendre des plats chers en fin de semaine, sans avoir anticipe. Le `Optimize()` de Z3, lui, minimise le **cout total sur les 7 jours simultanement** : il repartit les repetitions bon marche sur toute la semaine pour minimiser la somme globale.\n", "\n", - "**Capabilite exercee (Prong-B).** La matrice booleenne `Sel[7][24]` (168 variables) est resolue en quelques centaines de millisecondes : l'optimisation SMT reste tractable a cette echelle. La frontiere de convergence est plus loin — un corpus RecipeML a ~11 000 recettes (variables `Sel[7][11000]` = 77 000 Booleens par jour) sortirait du regime d'un simple `Optimize()` et demanderait une decomposition (column-generation, Lagrangian relaxation) : c'est la limite honnete de la \"couverture bornee\" d'un solveur SMT monocall, signalee dans l'Epic #1206.\n", + "**Capabilite exercee (Prong-B).** La matrice booleenne `Sel[7][24]` (168 variables) est resolue en quelques centaines de millisecondes : l'optimisation SMT reste tractable a cette echelle. La frontiere de convergence est plus loin — un corpus RecipeML a ~11 000 recettes (variables `Sel[7][11000]` = 77 000 Booléens par jour) sortirait du regime d'un simple `Optimize()` et demanderait une decomposition (column-generation, Lagrangian relaxation) : c'est la limite honnete de la \"couverture bornee\" d'un solveur SMT monocall, signalee dans l'Epic #1206.\n", "\n", - "**Lecture chiffree — quatre ordres de grandeur sur le corpus de jouet.** Le plan a cout minimal ci-dessus (D=7, 24 plats) se resout en une fraction de seconde dans ce notebook (le temps exact est imprime par la cellule de code ci-dessus) ; le [16](Z3-16-Meal-Planner-Python.ipynb) mesure, sur le meme corpus de jouet, l'enumeration des 36 combinaisons **0,06 ms**, le plan SMT booleen D=3 **2,4 ms** et l'`Optimize` a cout minimal D=1 **17,7 ms**. L'enumeration gagne partout ou elle reste tractable — mais sa pente est exponentielle en le nombre de variables quand celle du solveur suit la combinatoire contrainte. Passer de 3 a 7 jours avec corpus elargi et contrainte de variete coute environ deux ordres de grandeur (millisecondes -> fraction de seconde) : observation sur cette paire de runs, pas une loi (jours et corpus changent en meme temps). La lecture pratique : le temps du solveur achete l'exactitude a l'echelle ou l'enumeration explose, et la fenetre [1400, 1900] kcal avec 40 g de proteines reste resolue en moins d'une seconde a D=7.\n" + "**Lecture chiffree — quatre ordres de grandeur sur le corpus de jouet.** Le plan a cout minimal ci-dessus (D=7, 24 plats) se resout en une fraction de seconde dans ce notebook (le temps exact est imprime par la cellule de code ci-dessus) ; le [16](Z3-16-Meal-Planner-Python.ipynb) mesure, sur le même corpus de jouet, l'enumeration des 36 combinaisons **0,06 ms**, le plan SMT booléen D=3 **2,4 ms** et l'`Optimize` a cout minimal D=1 **17,7 ms**. L'enumeration gagne partout ou elle reste tractable — mais sa pente est exponentielle en le nombre de variables quand celle du solveur suit la combinatoire contrainte. Passer de 3 a 7 jours avec corpus elargi et contrainte de variete coute environ deux ordres de grandeur (millisecondes -> fraction de seconde) : observation sur cette paire de runs, pas une loi (jours et corpus changent en même temps). La lecture pratique : le temps du solveur achete l'exactitude a l'echelle ou l'enumeration explose, et la fenêtre [1400, 1900] kcal avec 40 g de proteines reste resolue en moins d'une seconde a D=7.\n" ] }, { diff --git a/scripts/notebook_tools/twin_pairs.d/z3-python-04-strings-regex.yaml b/scripts/notebook_tools/twin_pairs.d/z3-python-04-strings-regex.yaml index c2e3aec841..256d768159 100644 --- a/scripts/notebook_tools/twin_pairs.d/z3-python-04-strings-regex.yaml +++ b/scripts/notebook_tools/twin_pairs.d/z3-python-04-strings-regex.yaml @@ -6,6 +6,7 @@ bridge_verdict: SOTA-OK bridge_verdict_reason: "Z3 string/regex theory (SeqSort) branchee NATIVEMENT des deux cotes : Microsoft.Z3 .NET (`#r \"nuget: Microsoft.Z3\"` + `using Microsoft.Z3;`, ctx.MkRange/MkConcat/MkRe/MkInRe sur Seq) et pyz3 (`from z3 import *`, Range/Concat/Plus/Re/InRe sur Seq) sont les deux bindings officiels du meme coeur C++ Z3 sous-jacent — pas un pont intermediaire type IKVM/PythonNet. Concept string-regex (date AAAA-MM-JJ sous-contrainte en groupes longueur-fixe) demontre des deux cotes. Aucune asymetrie de machinerie a corriger." known_differences: + - "Re-baseline 2026-10-14 (hors-flotte:claude-session-16638, #16638) : restauration des accents de la prose markdown (tranche z3-api #16638, outil canonique restore_accents_canonical.py, invariance strip_accents a 0 finding), cote C# seul ; cote Python byte-identique a main. Aucune cellule de code, sortie ni execution_count touchee. Parite inchangee : attestation (le blob SHA se deplace), pas reparation. --update en DERNIERE operation (cf #8957)." - "Edition C# twin 2026-08-14 (myia-po-2024:CoursIA-2, #10488 density) : enrichissement markdown du jumeau C# seul (474->882 c/cell), 8 sections 'Implémentation C#' ajoutees apres les explications existantes -- detail binding-spcifique .NET (types de retour SeqExpr/IntExpr/ReExpr/BoolExpr, casts obligatoires, MkExtract exigent des IntExpr, MkConcat/MkUnion tableaux types, Status enum vs is_sat, Model.Eval + trim guillemets, decidable sans quantificateurs). Rattrapage partiel du Python twin, deja dense avec son propre contenu binding pyz3. Aucune divergence algorithmique : C.3 byte-identique (0 cellule code touchee, sources+outputs+exec_count inchanges) -- divergence markdown-only, le C# comble son retard pedagogique vers le Python, pas l'inverse (precedent Sudoku-06 AIMA-CSP 2026-08-12 po-2025)." - "Python : pyz3 (Range, Concat, Plus, Re, InRe, Length sur Seq). C# : Microsoft.Z3 .NET (ctx.MkRange, MkConcat, MkRe...)." - "Cote Python : fix code-correctness c.17 (PR #8040) — date AAAA-MM-JJ sous-contrainte (Plus(Range)=[0-9]+ variable) resverree en groupes longueur-fixe [0-9]{n} via helper chiffres(n). Le concept (string regex Z3) est commun aux deux cotes ; le detail du fix date est specifique au notebook Python." diff --git a/scripts/notebook_tools/twin_pairs.d/z3-python-04-strings-regex/0009-2026-10-14-hors-flotte-claude-session-16638.yaml b/scripts/notebook_tools/twin_pairs.d/z3-python-04-strings-regex/0009-2026-10-14-hors-flotte-claude-session-16638.yaml new file mode 100644 index 0000000000..14c7136d1c --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/z3-python-04-strings-regex/0009-2026-10-14-hors-flotte-claude-session-16638.yaml @@ -0,0 +1,6 @@ +date: '2026-10-14' +by: hors-flotte:claude-session-16638 +python_sha: 43183ba6ba6db135429bd14c57da433a32e6400e +csharp_sha: a29cc9f81f9f6929d09038aba9c3138b3d5135bc +content_python_sha: 6d57d025634f3141bdb12056e73ebb60e8a75b96cd8911abd2ba83769303019c +content_csharp_sha: a95b056fdaf46dd2071772ae2f8a16a5c47d869545699ab72a9897587e16a508 diff --git a/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization.yaml b/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization.yaml index dd987ef2a3..e00868911a 100644 --- a/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization.yaml +++ b/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization.yaml @@ -6,6 +6,7 @@ bridge_verdict: SOTA-OK bridge_verdict_reason: "Z3 optimization (MaxSAT / objectifs hierarchiques / front de Pareto) branchee NATIVEMENT des deux cotes : Microsoft.Z3 .NET (`#r \"nuget: Microsoft.Z3\"` + `using Microsoft.Z3;`, ctx.MkOptimize/MkMaximize/MkAssertSoft) et pyz3 (`from z3 import *`, Optimize/maximize/assert_soft) sont les deux bindings officiels du meme coeur C++ Z3 — pas un pont intermediaire. Concept porte au twin C# c.8052/#3801 (capstone budget 100->80, cas non-degenere, DRIFT resorbe). Aucune asymetrie de machinerie a corriger." known_differences: + - "Re-baseline 2026-10-14 (hors-flotte:claude-session-16638, #16638) : restauration des accents de la prose markdown (tranche z3-api #16638, outil canonique restore_accents_canonical.py, invariance strip_accents a 0 finding), cote C# seul ; cote Python byte-identique a main. Aucune cellule de code, sortie ni execution_count touchee. Parite inchangee : attestation (le blob SHA se deplace), pas reparation. --update en DERNIERE operation (cf #8957)." - "Python : pyz3 (Optimize, maximize/minimize, assert_soft pour MaxSAT, front de Pareto). C# : Microsoft.Z3 .NET (ctx.MkOptimize, MkMaximize, MkAssertSoft)." - "Concept demontre (objectifs hierarchiques, MaxSAT, front de Pareto) verifie cote Python (structure CLEAN c.20)." - "2026-07-24 (po-2026) : doc-honesty #8052 -- cell#21 prose disait 'budget de 100 unites' alors que code[22] tourne budget_total=80 (et cell#23 interprete deja correctement 'budget de 80, inferieur a la demande ideale 5x20=100'). Markdown-only align du nombre a l'output (100->80), code et outputs intacts. python_sha rebaseline suite a ce changement de blob." diff --git a/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization/0007-2026-10-14-hors-flotte-claude-session-16638.yaml b/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization/0007-2026-10-14-hors-flotte-claude-session-16638.yaml new file mode 100644 index 0000000000..e2d7975a7a --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization/0007-2026-10-14-hors-flotte-claude-session-16638.yaml @@ -0,0 +1,6 @@ +date: '2026-10-14' +by: hors-flotte:claude-session-16638 +python_sha: f514383306282b7f9a006e394177fe0017790c8e +csharp_sha: 8984bec53bf4c19d443683bd2c4fd49e628cb46f +content_python_sha: 6289c298a3b1d8627119a088d5019b0f48d1a8ddd2afcc9d51eecdd26b40c473 +content_csharp_sha: 81fad94776d601860676cfbdb790a0ee4f6f8fd29b6e63279ef752640d8fd6af From 21476b1eeae3e682b87188ec53298a84493dc019 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 17 Oct 2026 12:37:14 +0000 Subject: [PATCH 2/3] Fix: re-atteste la paire twin z3-python-06 a l'index 0008 apres #20617 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01LRbWZZHE9jZscr8ya3niWA --- .../0008-2026-10-17-hors-flotte-claude-session-16638.yaml | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization/0008-2026-10-17-hors-flotte-claude-session-16638.yaml diff --git a/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization/0008-2026-10-17-hors-flotte-claude-session-16638.yaml b/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization/0008-2026-10-17-hors-flotte-claude-session-16638.yaml new file mode 100644 index 0000000000..e153c12b91 --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/z3-python-06-advanced-optimization/0008-2026-10-17-hors-flotte-claude-session-16638.yaml @@ -0,0 +1,6 @@ +date: '2026-10-17' +by: hors-flotte:claude-session-16638 +python_sha: 065882eb974daed967e7e97fa5eb7e5f3e606870 +csharp_sha: 8984bec53bf4c19d443683bd2c4fd49e628cb46f +content_python_sha: f79e3bf7c13869726ff59c9199b4cff7530e9768eaa1e8bc045d8660d8aeab82 +content_csharp_sha: 81fad94776d601860676cfbdb790a0ee4f6f8fd29b6e63279ef752640d8fd6af From 1075995dac8461b5d039a237c4628638c08066be Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 17 Oct 2026 12:46:05 +0000 Subject: [PATCH 3/3] Fix(ci): reporte la renumerotation des index twins dupliques (#21182) main porte depuis 12:20Z deux attestations sous le meme index pour gametheory-6-evolutiontrust et search-07-mcts-and-beyond : test_audit_index_unique echoue et rougit Scripts Tests (CPU) sur cette PR. Meme renommage que #21182 (0022 -> 0023, 0019 -> 0021) ; il devient sans effet des que #21182 est sur main. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01LRbWZZHE9jZscr8ya3niWA --- ...-flotte.yaml => 0023-2026-10-13-claude-cloud-hors-flotte.yaml} | 0 ...-flotte.yaml => 0021-2026-10-14-claude-cloud-hors-flotte.yaml} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename scripts/notebook_tools/twin_pairs.d/gametheory-6-evolutiontrust/{0022-2026-10-13-claude-cloud-hors-flotte.yaml => 0023-2026-10-13-claude-cloud-hors-flotte.yaml} (100%) rename scripts/notebook_tools/twin_pairs.d/search-07-mcts-and-beyond/{0019-2026-10-14-claude-cloud-hors-flotte.yaml => 0021-2026-10-14-claude-cloud-hors-flotte.yaml} (100%) diff --git a/scripts/notebook_tools/twin_pairs.d/gametheory-6-evolutiontrust/0022-2026-10-13-claude-cloud-hors-flotte.yaml b/scripts/notebook_tools/twin_pairs.d/gametheory-6-evolutiontrust/0023-2026-10-13-claude-cloud-hors-flotte.yaml similarity index 100% rename from scripts/notebook_tools/twin_pairs.d/gametheory-6-evolutiontrust/0022-2026-10-13-claude-cloud-hors-flotte.yaml rename to scripts/notebook_tools/twin_pairs.d/gametheory-6-evolutiontrust/0023-2026-10-13-claude-cloud-hors-flotte.yaml diff --git a/scripts/notebook_tools/twin_pairs.d/search-07-mcts-and-beyond/0019-2026-10-14-claude-cloud-hors-flotte.yaml b/scripts/notebook_tools/twin_pairs.d/search-07-mcts-and-beyond/0021-2026-10-14-claude-cloud-hors-flotte.yaml similarity index 100% rename from scripts/notebook_tools/twin_pairs.d/search-07-mcts-and-beyond/0019-2026-10-14-claude-cloud-hors-flotte.yaml rename to scripts/notebook_tools/twin_pairs.d/search-07-mcts-and-beyond/0021-2026-10-14-claude-cloud-hors-flotte.yaml