Convert the demos to single-file Spectre.Console apps

[HowardvanRooijen]

Replaces the Z3.Linq.Demo project - a single Program.cs that dumped every scenario through
Console.WriteLine - with a series of standalone single-file Spectre.Console
apps under demos/. Each is a
.NET file-based app:
one .cs file that declares its own dependencies at the top and runs with dotnet run demos/<name>.cs

• no project, no .slnx entry.

The demos

File	Problem	Spectre UI
river-crossing.cs	Missionaries & Cannibals	figlet banner, the crossing as a table, a Solve vs Optimize/orderby comparison
sudoku.cs	Two puzzles	side-by-side 9x9 puzzle/solution grids, clues in white and Z3-derived cells in green
boolean-logic.cs	x XOR y, three ways	one table over an anonymous type, a value tuple and a record
linear-systems.cs	Integer systems (incl. Bart's TechEd 2012)	constraints panel next to a solution table
oil-purchase.cs	Least-cost LP	purchase table with currency, spinner while optimising
warehouse.cs	Least-cost shipping	a warehouse x customer matrix
menu.cs	Launcher	a SelectionPrompt that runs any of the above

Each file references the library with #:project ../solutions/Z3.Linq/... (and
Z3.Linq.Examples where it uses the sample theorems), so the demos build against local source and
pick up the native Z3 package transitively. Sudoku's clues are turned into Cell{r}{c} == v
constraints with expression trees, so the printed puzzle and the constraints come from one array.

Why the examples project is untouched

Z3.Linq.Examples is the reusable theorem library (MissionariesAndCannibals,
SudokuTheorem/SudokuTable, RecordTheorem) - it has no console I/O and even ships as a NuGet
package. The Spectre work is purely presentation, so the demos consume the examples as-is rather
than changing them.

Portability

Non-ASCII is limited to the Sudoku box-drawing (near-universal, and what Spectre's own borders use);
the maths and logic are ASCII, per the guide's advice against fragile Unicode. Spectre auto-detects
terminal capability and degrades to plain text when output is redirected, so the demos are safe to
capture in scripts.

Verified

• Every content demo run with dotnet run demos/<name>.cs - all six produce correct results
  (both Sudoku puzzles solved, the river-crossing Solve plan at 24 steps vs the minimal 12 from
  Optimize/orderby, the LPs at their known optima). menu.cs compiles.
• Old project removed: solutions/Z3.Linq.Demo deleted, dropped from Z3.Linq.slnx, README
  updated, and a new demos/README.md added.
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings with the Demo project gone.
• File-based apps build to a temp directory, so nothing new lands in bin/obj or needs ignoring.

Reference

Built following the endjin Spectre.Console guide (read from the local knowledge-base clone; the URL
provided carried an access token, which was not fetched or transmitted).

Release note

No library or public-API change - developer-facing demos only. Releases remain on hold under #60.

🤖 Generated with Claude Code

[github-actions]

Test Results

  1 files  ±0    1 suites  ±0   10s ⏱️ ±0s
309 tests ±0  309 ✅ ±0  0 💤 ±0  0 ❌ ±0 
322 runs  ±0  322 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit b425802. ± Comparison against base commit 8f0659d.

♻️ This comment has been updated with latest results.

[jsboige]

Ran the full stack on an independent fresh Windows machine (win-x64, .NET SDK 10.0.400) — validation notes, in case they're useful before the Z3 release unblocks:

Suite: 322/322 green. dotnet run --project solutions/Z3.Linq.Tests/Z3.Linq.Tests.csproj (MTP), ~4.3 s wall. The folder-feed mechanism works exactly as designed: Install-Z3Package.ps1 fetched the hash-pinned 5.1.0 nupkg and restore picked it up. Two Windows-quirk footnotes:

• powershell -File invoked from Git Bash leaves $PSScriptRoot empty in the param default, so -FeedPath has to be passed explicitly (Windows PowerShell 5.1 only; pwsh unaffected, CI unaffected).
• dotnet test (as opposed to dotnet run) returns exit code 5 / "zero tests" against the MTP project on SDK 10.0.400 — possibly a known dotnet test ↔ Testing.Platform bridge gap rather than anything in the stack.

Merge rehearsal against our fork (context: MyIntelligenceAgency/Z3.Linq sits 45 commits ahead / 0 behind main, same base as this stack; both lines are unmerged proposals off the same ancestor). Merging this branch's tip into our line conflicts on 10 files — 5 library (ExpressionVisitor.cs, Theorem.cs, Theorem{T}.cs, Z3Context.cs, Environment.cs) and 5 infra (build.yml, .gitignore, README.md, build.ps1, tests csproj). Taking the stack side on all ten, two residual blockers remain, both on ours:

1. fork-only feature files trip the Generate and validate the XML documentation #94 doc-XML gate (CS1591 on Rational.cs operators, CS1574 on SolverKind.cs) — so feature PRs from our side will carry full XML docs on public members, which is a good gate to have;
2. the two test projects collide in one folder — our 14 xUnit suites do not compile inside the stack's MSTest/MTP project (221 errors after suppressing the doc gate, a mix of harness mismatch and API drift against the refactored visitor). When the stack lands, our test contributions will be ported to the MSTest/MTP harness.

The rehearsal branch is pushed as integration/howard-stack on our fork for reproducibility.

Also opened #111 in support: a minimal xUnit floor pinned to current main semantics (10 facts) — complementary to your 322-suite, since it documents what main does today and would make any semantic drift introduced along the stack visible as a red test rather than a silent change. No action needed on it for this stack; it's there when you want a pre-stack baseline.