// ---- 3.5 DSL Z3.Linq : bandes ponderees -> MkPBGe/MkPBLe/MkPBEq natifs (fork #10605, PR #24) ----
// CS1701 (System.Linq.Expressions 8.0 vs 10.0) : cf. cellule 3.4.
#pragma warning disable CS1701
using Z3.Linq;
// (a) Une bande ponderee tient en clauses LINQ. MenuW : 8 recettes candidates pour 2 plats, poids =
// energie reelle (kJ) des 8 premieres recettes du cache. La bande est calibree sur les sommes
// atteignables (28 paires) : plancher/plafond = terciles des sommes triees -> SAT garanti, et le
// solveur doit vraiment PESER les indicateurs, pas juste en allumer un au hasard.
var wW = Enumerable.Range(0, 8).Select(r => vint[0][r]).ToArray();
var onesW = Enumerable.Repeat(1, 8).ToArray();
var sumsW = (from i in Enumerable.Range(0, 8) from j in Enumerable.Range(0, 8) where i < j select wW[i] + wW[j]).OrderBy(s => s).ToList();
int loW = sumsW[sumsW.Count / 3], hiW = sumsW[2 * sumsW.Count / 3];
var dctxW = new Z3Context();
var thW = dctxW.NewTheorem<MenuW>()
.Where(t => Z3Methods.WeightedExactly(2, onesW, t.S[0], t.S[1], t.S[2], t.S[3], t.S[4], t.S[5], t.S[6], t.S[7]))
.Where(t => Z3Methods.WeightedAtLeast(loW, wW, t.S[0], t.S[1], t.S[2], t.S[3], t.S[4], t.S[5], t.S[6], t.S[7]))
.Where(t => Z3Methods.WeightedAtMost(hiW, wW, t.S[0], t.S[1], t.S[2], t.S[3], t.S[4], t.S[5], t.S[6], t.S[7]));
var swDW = Stopwatch.StartNew();
var pickW = thW.Solve();
swDW.Stop();
if (pickW != null)
{
var namesW = Enumerable.Range(0, 8).Where(i => pickW.S[i]).Select(i => plats[i].title).ToList();
int eW = Enumerable.Range(0, 8).Where(i => pickW.S[i]).Sum(i => wW[i]);
Console.WriteLine($"DSL bandes ponderees (8 recettes, exactement 2 + bande energie [{loW},{hiW}] kJ) : {swDW.Elapsed.TotalSeconds:F3}s -> SAT, {eW} kJ : " + string.Join(" | ", namesW));
}
else
{
Console.WriteLine($"DSL bandes ponderees : UNSAT sur la bande [{loW},{hiW}] kJ (recalibrer si le cache a change).");
}
// (b) Echelle : meme formule (exactly-one + bande IQR des energies, recalculee sur le sous-ensemble),
// deux encodages, sous-ensembles croissants. Le natif = exactement ce que le visiteur du DSL emet
// pour WeightedAtLeast/AtMost. Guard 60s par solveur (le soft timeout Z3 borne ces tailles-la).
Console.WriteLine("Echelle bande ponderee reelle (coeffs = energie kJ des n premieres recettes) :");
foreach (var n in new[] { 200, 400, 800, 1600 })
{
var subE = Enumerable.Range(0, n).Select(r2 => vint[0][r2]).ToArray();
var sortedE = subE.OrderBy(x => x).ToArray();
int loS = sortedE[(int)(0.25 * (n - 1))], hiS = sortedE[(int)(0.75 * (n - 1))];
var ctxN = new Context(); var sN = ctxN.MkSolver(); sN.Set("timeout", 60000u);
var bN = Enumerable.Range(0, n).Select(i => ctxN.MkBoolConst($"ln_{i}")).ToArray();
var onesN = Enumerable.Repeat(1, n).ToArray();
sN.Assert(ctxN.MkPBEq(onesN, bN, 1));
sN.Assert(ctxN.MkPBGe(subE, bN, loS));
sN.Assert(ctxN.MkPBLe(subE, bN, hiS));
var swN = Stopwatch.StartNew(); var resN = sN.Check(); swN.Stop();
ctxN.Dispose();
var ctxE = new Context(); var sE = ctxE.MkSolver(); sE.Set("timeout", 60000u);
var bE = Enumerable.Range(0, n).Select(i => ctxE.MkBoolConst($"le_{i}")).ToArray();
var cardE = ctxE.MkAdd(bE.Select(b => (ArithExpr)ctxE.MkITE(b, ctxE.MkInt(1), ctxE.MkInt(0))).ToArray());
sE.Assert(ctxE.MkEq(cardE, ctxE.MkInt(1)));
var bandE = ctxE.MkAdd(bE.Select((b, ix) => (ArithExpr)ctxE.MkITE(b, ctxE.MkInt(subE[ix]), ctxE.MkInt(0))).ToArray());
sE.Assert(ctxE.MkGe(bandE, ctxE.MkInt(loS)));
sE.Assert(ctxE.MkLe(bandE, ctxE.MkInt(hiS)));
var swE = Stopwatch.StartNew(); var resE = sE.Check(); swE.Stop();
ctxE.Dispose();
Console.WriteLine($" n={n,4} bande [{loS},{hiS}] : natif PB {swN.Elapsed.TotalSeconds:F2}s -> {resN} | expansion MkIte {swE.Elapsed.TotalSeconds:F2}s -> {resE}");
}
// (c) L'echelle pleine, cote natif : R booleens, bande IQR de toutes les energies. L'expansion, elle,
// ne rend PAS a cette taille (3 executions coupees a 600 s en dev ; le soft timeout pose sur le
// solveur n'interrompt pas la normalisation des grands coefficients) -- d'ou l'echelle en (b).
int loB = (int)Pq(0, 0.25), hiB = (int)Pq(0, 0.75);
var ctxF = new Context(); var sF = ctxF.MkSolver(); sF.Set("timeout", 120000u);
var bF = Enumerable.Range(0, R).Select(r2 => ctxF.MkBoolConst($"fn_{r2}")).ToArray();
var onesF = Enumerable.Repeat(1, R).ToArray();
sF.Assert(ctxF.MkPBEq(onesF, bF, 1));
sF.Assert(ctxF.MkPBGe(vint[0], bF, loB));
sF.Assert(ctxF.MkPBLe(vint[0], bF, hiB));
var swF = Stopwatch.StartNew(); var resF = sF.Check(); swF.Stop();
Console.WriteLine($"Echelle pleine : natif PB R={R}, bande IQR [{loB},{hiB}] -> {resF} en {swF.Elapsed.TotalSeconds:F2}s ; expansion : pas de reponse sous 600 s (mur mesure entre n=1600 et R=3717).");
Console.WriteLine(" (cf. pb-bench c.8252 du fork : n=100 pondere -> 103 vs 307 noeuds AST ; la §3.4 mesurait 653x en resolution non ponderee, ici l'ecart devient qualitatif : plat vs mur)");
public class MenuW { public bool[] S { get; set; } = new bool[8]; }