Convert the demos to single-file Spectre.Console apps

README.md

@@ -6,7 +6,7 @@ Based on the proof of concept by [Bart De Smet](https://github.com/bartdesmet) w
 
 ## Examples
 
-A number of examples are included in this solution, which you can run [from .NET Interactive](examples/z3-problems.dib) (requires [Visual Studio Code](https://code.visualstudio.com/)) or [from Visual Studio](solutions/Z3.Linq.Demo/Program.cs).
+A number of examples are included as standalone [Spectre.Console](https://spectreconsole.net/) demos in [`demos/`](demos), each a single-file .NET app. Run the interactive launcher with `dotnet run demos/menu.cs`, or run any one directly, e.g. `dotnet run demos/sudoku.cs`; see the [demos README](demos/README.md) for the full list.
 
 ### Problem - 1st Order Propositional Logic
 
@@ -239,20 +239,6 @@ throws, so it can never be mistaken for one.
 
 You can install the [Z3.Linq NuGet Package](https://www.nuget.org/packages/Z3.Linq/).
 
-### For Polyglot Notebooks
-
-Add the package:
-```
-#r "nuget:Z3.Linq"
-```
-Then add the following using statements:
-
-```csharp
-using System;
-using Z3.Linq;
-```
-Then you can copy any of the above samples.
-
 ### For Visual Studio
 
 Add the `Z3.Linq` package. No platform target is needed: `Microsoft.Z3` supplies native binaries for x64 and arm64 on Windows, Linux and macOS, and the default `AnyCPU` resolves the right one.
@@ -296,7 +282,7 @@ All PRs are welcome.
 
 2020: [Karel Frajtak](https://github.com/kfrajtak) adds [support for fractions](https://github.com/kfrajtak/Z3.LinqBinding).
 
-2021: [Howard van Rooijen](https://github.com/HowardvanRooijen) and [Ian Griffiths](https://github.com/idg10) ([endjin](https://github.com/endjin)) upgrade the project to `.NET 6.0`, added `Optimize` support via LINQ's `OrderBy`, [ValueTuple](https://docs.microsoft.com/en-us/dotnet/api/system.valuetuple?view=net-6.0) support, demonstrate using `record` types, and fix nullability issues. They upgraded the solution to use [Z3 NuGet package](https://www.nuget.org/packages/Microsoft.Z3.x64/), merged in features from [Jean-Sylvain Boige](https://github.com/jsboige) and [Karel Frajtak](https://github.com/kfrajtak) forks, created archives of Bart's original blog posts and talks. They republished the project as [Z3.Linq](https://github.com/endjin/Z3.Linq), created a new [Polyglot Notebook](https://github.com/dotnet/interactive) of [samples](examples/z3-problems.dib), and published a NuGet package [Z3.Linq](https://www.nuget.org/packages/Z3.Linq/).
+2021: [Howard van Rooijen](https://github.com/HowardvanRooijen) and [Ian Griffiths](https://github.com/idg10) ([endjin](https://github.com/endjin)) upgrade the project to `.NET 6.0`, added `Optimize` support via LINQ's `OrderBy`, [ValueTuple](https://docs.microsoft.com/en-us/dotnet/api/system.valuetuple?view=net-6.0) support, demonstrate using `record` types, and fix nullability issues. They upgraded the solution to use [Z3 NuGet package](https://www.nuget.org/packages/Microsoft.Z3.x64/), merged in features from [Jean-Sylvain Boige](https://github.com/jsboige) and [Karel Frajtak](https://github.com/kfrajtak) forks, created archives of Bart's original blog posts and talks. They republished the project as [Z3.Linq](https://github.com/endjin/Z3.Linq) and published a NuGet package [Z3.Linq](https://www.nuget.org/packages/Z3.Linq/).
 
 2023: [Whit Waldo](https://github.com/WhitWaldo) upgrades the project to `.NET 8.0`
 

demos/README.md

@@ -0,0 +1,44 @@
+# Z3.Linq demos
+
+A set of standalone [Spectre.Console](https://spectreconsole.net/) demos for `Z3.Linq`, each a
+single-file [.NET file-based app](https://learn.microsoft.com/dotnet/core/whats-new/dotnet-10#file-based-apps).
+No project, no solution entry - just run the file:
+
+```bash
+dotnet run demos/sudoku.cs
+```
+
+The first run of a file restores its packages and builds it; later runs are fast. Each file
+declares its own dependencies at the top (`#:package Spectre.Console`, `#:project ...` to the
+`Z3.Linq` and `Z3.Linq.Examples` projects in [`../solutions`](../solutions)), so they build against
+your local source.
+
+## The demos
+
+| File | Problem |
+|------|---------|
+| [`menu.cs`](menu.cs) | An interactive launcher - pick a demo from a Spectre menu and it runs the others. |
+| [`river-crossing.cs`](river-crossing.cs) | Missionaries & Cannibals, showing `Solve` (any plan) against `Optimize`/`orderby` (the shortest plan). |
+| [`sudoku.cs`](sudoku.cs) | Two Sudoku puzzles solved on a rendered 9x9 grid, clues driven through expression-tree constraints. |
+| [`boolean-logic.cs`](boolean-logic.cs) | `x XOR y` over an anonymous type, a value tuple, and a record - the same theorem, three environment shapes. |
+| [`linear-systems.cs`](linear-systems.cs) | Small integer constraint systems, including Bart De Smet's TechEd Europe 2012 example. |
+| [`oil-purchase.cs`](oil-purchase.cs) | A least-cost linear program (`orderby` minimises the bill). |
+| [`warehouse.cs`](warehouse.cs) | Least-cost shipping across two warehouses to four customers. |
+
+## Running everything
+
+```bash
+# interactive launcher
+dotnet run demos/menu.cs
+
+# or one at a time
+dotnet run demos/river-crossing.cs
+dotnet run demos/sudoku.cs
+dotnet run demos/boolean-logic.cs
+dotnet run demos/linear-systems.cs
+dotnet run demos/oil-purchase.cs
+dotnet run demos/warehouse.cs
+```
+
+Output is styled when run in a terminal and degrades to plain text when redirected (piped to a file
+or another program), so the demos are safe to capture in scripts.

demos/boolean-logic.cs

@@ -0,0 +1,76 @@
+#:project ../solutions/Z3.Linq/Z3.Linq.csproj
+#:project ../solutions/Z3.Linq.Examples/Z3.Linq.Examples.csproj
+#:package Spectre.Console@0.57.2
+
+// The same Boolean theorem - find x, y with x XOR y true - expressed three ways: an anonymous type,
+// a value tuple, and a record. Shows that the environment type is just a shape Z3.Linq marshals to.
+//
+//   dotnet run demos/boolean-logic.cs
+
+using System.Diagnostics;
+
+using Spectre.Console;
+
+using Z3.Linq;
+using Z3.Linq.Examples;
+
+AnsiConsole.Write(new FigletText("Boolean Logic").Color(Color.Aqua).Centered());
+AnsiConsole.Write(new Rule("[aqua]x XOR y[/]"));
+AnsiConsole.WriteLine();
+
+AnsiConsole.Write(new Panel(
+    "Find Boolean [aqua]x[/] and [aqua]y[/] such that [yellow]x ^ y[/] holds - the one theorem written\n" +
+    "over three different environment types. Z3 solves each the same way.")
+    .Header("[white]The problem[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey));
+AnsiConsole.WriteLine();
+
+var table = new Table().Border(TableBorder.Rounded).BorderColor(Color.Grey)
+    .AddColumn("[white]Environment type[/]")
+    .AddColumn(new TableColumn("[white]x[/]").Centered())
+    .AddColumn(new TableColumn("[white]y[/]").Centered())
+    .AddColumn(new TableColumn("[white]x ^ y[/]").Centered())
+    .AddColumn(new TableColumn("[white]Time[/]").RightAligned());
+
+using (var ctx = new Z3Context())
+{
+    var theorem = from t in ctx.NewTheorem(new { x = default(bool), y = default(bool) })
+                  where t.x ^ t.y
+                  select t;
+    // Solve() returns T?, null only when unsatisfiable - which x ^ y never is. The ! is needed
+    // for the reference-type environments (this and the record below); the value tuple is not null.
+    var (r, ms) = Time(() => theorem.Solve()!);
+    table.AddRow("[grey]anonymous type[/]", Bool(r.x), Bool(r.y), Bool(r.x ^ r.y), Ms(ms));
+}
+
+using (var ctx = new Z3Context())
+{
+    var theorem = from t in ctx.NewTheorem<(bool x, bool y)>()
+                  where t.x ^ t.y
+                  select t;
+    var (r, ms) = Time(() => theorem.Solve());
+    table.AddRow("[grey]value tuple[/]", Bool(r.x), Bool(r.y), Bool(r.x ^ r.y), Ms(ms));
+}
+
+using (var ctx = new Z3Context())
+{
+    var theorem = from t in ctx.NewTheorem(new RecordTheorem<bool, bool>())
+                  where t.X ^ t.Y
+                  select t;
+    var (r, ms) = Time(() => theorem.Solve()!);
+    table.AddRow("[grey]record[/]", Bool(r.X), Bool(r.Y), Bool(r.X ^ r.Y), Ms(ms));
+}
+
+AnsiConsole.Write(table);
+AnsiConsole.MarkupLine("[grey]  Each row is an independent solve; XOR has two solutions, so Z3 may pick either.[/]");
+
+static string Bool(bool b) => b ? "[green]true[/]" : "[red]false[/]";
+
+static string Ms(double ms) => $"[grey]{ms:F1} ms[/]";
+
+static (T Result, double Ms) Time<T>(Func<T> solve)
+{
+    var sw = Stopwatch.StartNew();
+    T result = solve();
+    sw.Stop();
+    return (result, sw.Elapsed.TotalMilliseconds);
+}

demos/linear-systems.cs

@@ -0,0 +1,94 @@
+#:project ../solutions/Z3.Linq/Z3.Linq.csproj
+#:package Spectre.Console@0.57.2
+
+// Small systems of linear integer constraints, solved as Z3 theorems and rendered with
+// Spectre.Console. Includes Bart De Smet's example from TechEd Europe 2012, shown over both a
+// Symbols<int,int,int> environment and an equivalent value tuple.
+//
+//   dotnet run demos/linear-systems.cs
+
+using System.Diagnostics;
+
+using Spectre.Console;
+
+using Z3.Linq;
+
+AnsiConsole.Write(new FigletText("Linear Systems").Color(Color.Yellow).Centered());
+AnsiConsole.Write(new Rule("[yellow]integer constraint solving[/]"));
+AnsiConsole.WriteLine();
+
+// Bart's TechEd Europe 2012 example, over Symbols<int, int, int>.
+using (var ctx = new Z3Context())
+{
+    var theorem = from t in ctx.NewTheorem<Symbols<int, int, int>>()
+                  where t.X1 - t.X2 >= 1
+                  where t.X1 - t.X2 <= 3
+                  where t.X1 == (2 * t.X3) + t.X2
+                  select t;
+
+    // Solve() returns T?, null only when unsatisfiable; ! since Symbols<...> is a reference type.
+    var (r, ms) = Time(() => theorem.Solve()!);
+    Section("Bart's example (TechEd Europe 2012)",
+        ["x1 - x2 >= 1", "x1 - x2 <= 3", "x1 == 2*x3 + x2"],
+        [("x1", r.X1), ("x2", r.X2), ("x3", r.X3)], ms);
+}
+
+// The same system over a value tuple.
+using (var ctx = new Z3Context())
+{
+    var theorem = from t in ctx.NewTheorem<(int x, int y, int z)>()
+                  where t.x - t.y >= 1
+                  where t.x - t.y <= 3
+                  where t.x == (2 * t.z) + t.y
+                  select t;
+
+    var (r, ms) = Time(() => theorem.Solve());
+    Section("The same system over a value tuple",
+        ["x - y >= 1", "x - y <= 3", "x == 2*z + y"],
+        [("x", r.x), ("y", r.y), ("z", r.z)], ms);
+}
+
+// A Symbols<int, int> example with an inequality and a distinctness constraint.
+using (var ctx = new Z3Context())
+{
+    var theorem = from t in ctx.NewTheorem<Symbols<int, int>>()
+                  where t.X1 < t.X2 + 1
+                  where t.X1 > 2
+                  where t.X1 != t.X2
+                  select t;
+
+    var (r, ms) = Time(() => theorem.Solve()!);
+    Section("A Symbols<int, int> example",
+        ["x1 < x2 + 1", "x1 > 2", "x1 != x2"],
+        [("x1", r.X1), ("x2", r.X2)], ms);
+}
+
+void Section(string title, string[] constraints, (string Name, int Value)[] solution, double ms)
+{
+    AnsiConsole.Write(new Rule($"[yellow]{title}[/]").LeftJustified());
+
+    var constraintList = new Panel(string.Join("\n", constraints.Select(c => $"[white]{c}[/]")))
+        .Header("[white]Constraints[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey);
+
+    var table = new Table().Border(TableBorder.Rounded).BorderColor(Color.Yellow)
+        .AddColumn(new TableColumn("[white]Symbol[/]").Centered())
+        .AddColumn(new TableColumn("[white]Value[/]").Centered());
+    foreach (var (name, value) in solution)
+    {
+        table.AddRow($"[yellow]{name}[/]", $"[white]{value}[/]");
+    }
+
+    var layout = new Grid().AddColumn().AddColumn();
+    layout.AddRow(constraintList, new Panel(table).Header("[white]Solution[/]").Border(BoxBorder.None));
+    AnsiConsole.Write(layout);
+    AnsiConsole.MarkupLine($"[grey]  Solved in {ms:F1} ms[/]");
+    AnsiConsole.WriteLine();
+}
+
+static (T Result, double Ms) Time<T>(Func<T> solve)
+{
+    var sw = Stopwatch.StartNew();
+    T result = solve();
+    sw.Stop();
+    return (result, sw.Elapsed.TotalMilliseconds);
+}

demos/menu.cs

@@ -0,0 +1,75 @@
+#:package Spectre.Console@0.57.2
+
+// An interactive launcher for the Z3.Linq demos. Presents a Spectre.Console menu and runs the
+// chosen demo as its own file-based app (`dotnet run demos/<name>.cs`).
+//
+//   dotnet run demos/menu.cs
+
+using System.Diagnostics;
+
+using Spectre.Console;
+
+var demos = new (string Name, string File, string Blurb)[]
+{
+    ("River crossing", "river-crossing.cs", "Missionaries & Cannibals - Solve, Optimize and orderby"),
+    ("Sudoku", "sudoku.cs", "Two puzzles solved on a 9x9 grid"),
+    ("Boolean logic", "boolean-logic.cs", "x XOR y over an anonymous type, a tuple and a record"),
+    ("Linear systems", "linear-systems.cs", "Integer constraint systems, incl. Bart's TechEd example"),
+    ("Oil purchase", "oil-purchase.cs", "A least-cost linear program"),
+    ("Warehouse logistics", "warehouse.cs", "Least-cost shipping across two warehouses"),
+};
+
+// Run from the repo root (`dotnet run demos/menu.cs`) or from within demos/.
+string dir = File.Exists("river-crossing.cs") ? "." : "demos";
+
+AnsiConsole.Write(new FigletText("Z3.Linq").Color(Color.Aqua).Centered());
+AnsiConsole.Write(new Rule("[aqua]demos[/]"));
+AnsiConsole.WriteLine();
+
+const string quit = "Quit";
+
+while (true)
+{
+    var choice = AnsiConsole.Prompt(
+        new SelectionPrompt<string>()
+            .Title("Choose a [green]demo[/] to run:")
+            .PageSize(10)
+            .UseConverter(name => name == quit
+                ? "[grey]Quit[/]"
+                : $"{name}  [grey]- {demos.First(d => d.Name == name).Blurb}[/]")
+            .AddChoices([.. demos.Select(d => d.Name), quit]));
+
+    if (choice == quit)
+    {
+        break;
+    }
+
+    var demo = demos.First(d => d.Name == choice);
+
+    AnsiConsole.WriteLine();
+    AnsiConsole.Write(new Rule($"[green]{Markup.Escape(demo.Name)}[/]"));
+
+    var start = new ProcessStartInfo("dotnet") { UseShellExecute = false };
+    start.ArgumentList.Add("run");
+    start.ArgumentList.Add(Path.Combine(dir, demo.File));
+
+    try
+    {
+        using var process = Process.Start(start);
+        process!.WaitForExit();
+    }
+    catch (Exception ex)
+    {
+        AnsiConsole.WriteException(ex, ExceptionFormats.ShortenPaths);
+    }
+
+    AnsiConsole.WriteLine();
+    if (!AnsiConsole.Confirm("Run [green]another[/] demo?"))
+    {
+        break;
+    }
+
+    AnsiConsole.WriteLine();
+}
+
+AnsiConsole.MarkupLine("[grey]Bye![/]");

demos/oil-purchase.cs

@@ -0,0 +1,60 @@
+#:project ../solutions/Z3.Linq/Z3.Linq.csproj
+#:package Spectre.Console@0.57.2
+
+// The classic oil-purchase linear program, solved as a Z3 theorem and rendered with
+// Spectre.Console. Buy crude from Saudi Arabia and Venezuela to meet minimum yields of three
+// products at the least cost. `orderby` asks Z3 to minimise total spend.
+//
+//   dotnet run demos/oil-purchase.cs
+
+using System.Diagnostics;
+using System.Globalization;
+
+using Spectre.Console;
+
+using Z3.Linq;
+
+var money = CultureInfo.CreateSpecificCulture("en-US");
+
+AnsiConsole.Write(new FigletText("Oil Purchase").Color(Color.Orange1).Centered());
+AnsiConsole.Write(new Rule("[orange1]a least-cost linear program[/]"));
+AnsiConsole.WriteLine();
+
+AnsiConsole.Write(new Panel(
+    "Each barrel of [orange1]Saudi[/] crude yields 0.3 gasoline / 0.4 jet fuel / 0.2 lubricant;\n" +
+    "each [orange1]Venezuelan[/] barrel yields 0.4 / 0.2 / 0.3. Demand is at least [white]1900[/] / [white]1500[/] / [white]500[/].\n" +
+    "Saudi is [green]$20[/]/barrel, Venezuela [green]$15[/] - [italic]orderby[/] minimises the total bill.")
+    .Header("[white]The problem[/]").Border(BoxBorder.Rounded).BorderColor(Color.Grey));
+AnsiConsole.WriteLine();
+
+using var ctx = new Z3Context();
+var solveable = from t in ctx.NewTheorem<(double vz, double sa)>()
+                where 0.3 * t.sa + 0.4 * t.vz >= 1900
+                where 0.4 * t.sa + 0.2 * t.vz >= 1500
+                where 0.2 * t.sa + 0.3 * t.vz >= 500
+                where 0 <= t.sa && t.sa <= 9000
+                where 0 <= t.vz && t.vz <= 6000
+                orderby (20.0 * t.sa) + (15.0 * t.vz)
+                select t;
+
+(double vz, double sa) result = default;
+var sw = Stopwatch.StartNew();
+AnsiConsole.Status().Spinner(Spinner.Known.Dots).SpinnerStyle(Style.Parse("orange1"))
+    .Start("[orange1]Optimising...[/]", _ => result = solveable.Solve());
+sw.Stop();
+
+double saCost = result.sa * 20;
+double vzCost = result.vz * 15;
+
+var table = new Table().Border(TableBorder.Rounded).BorderColor(Color.Orange1)
+    .Title("[orange1]Cheapest purchase[/]")
+    .AddColumn("[white]Source[/]")
+    .AddColumn(new TableColumn("[white]Barrels[/]").RightAligned())
+    .AddColumn(new TableColumn("[white]Cost[/]").RightAligned());
+table.AddRow("Saudi Arabia", $"{result.sa:N0}", $"[green]{saCost.ToString("C", money)}[/]");
+table.AddRow("Venezuela", $"{result.vz:N0}", $"[green]{vzCost.ToString("C", money)}[/]");
+table.AddEmptyRow();
+table.AddRow("[white]Total[/]", string.Empty, $"[bold green]{(saCost + vzCost).ToString("C", money)}[/]");
+
+AnsiConsole.Write(table);
+AnsiConsole.MarkupLine($"[grey]  Optimised in {sw.Elapsed.TotalMilliseconds:F1} ms[/]");