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.