Add a BenchmarkDotNet suite for solve hot paths

[HowardvanRooijen]

Adds a Z3.Linq.Benchmarks project - a BenchmarkDotNet suite,
following the endjin BenchmarkDotNet guidelines, for finding performance and memory hot paths in
the library and confirming an optimisation actually helped. It measures; it changes no library
code.

What it measures, and why it's the right thing

SolveBenchmarks runs end-to-end Solve/Optimize over six environment shapes, each against a
theorem Z3 decides in microseconds. That is deliberate: with the solver's own work negligible,
the time and - more usefully - the MemoryDiagnoser Allocated column are dominated by the
library's per-solve work: building the environment by reflection, translating the constraint
expression trees, and marshalling the model back onto the CLR members. Nothing is cached across
solves today, so re-solving the same theorem re-does all of it - which is exactly what these numbers
can be used to change.

Benchmark	Exercises
ScalarSymbols (baseline)	a flat Symbols<int,int>
ValueTuple	the value-tuple environment path
NestedObject	recursive marshalling of a nested object
Collection	the array element loop
WideSymbols	more members to reflect and translate (Symbols<int,int,int,int,int>)
Optimize	the optimiser's own solve path

Each theorem is built once in [GlobalSetup]; the benchmark measures only the solve, and returns
the result so the JIT cannot eliminate the call.

It already points somewhere

A first --job dry run (allocation is meaningful even in Dry; the Dry Mean is not) - relative to
the flat-symbol baseline:

Shape	Allocated	vs baseline
ValueTuple	4.5 KB	0.4x
ScalarSymbols	11.6 KB	1.0x
NestedObject	20.1 KB	1.7x
Optimize	24.6 KB	2.1x
WideSymbols	24.7 KB	2.1x
Collection	26.3 KB	2.3x

The collection path allocates over twice the flat baseline, and the nested/wide/optimise shapes
around twice - the marshalling loop (ArrayList + ToArray, boxing), the recursive marshalling,
and the per-solve reflection. That is the map an optimisation would follow; this PR just draws it.

The loop it enables

1. Run the suite; the Allocated/Mean columns say which shape to look at.
2. Change the allocation in the library (the marshalling loop, the per-solve GetProperties /
   GetCustomAttributes reflection, boxing of value-type members).
3. Re-run the same filter; Ratio and Alloc Ratio against the baseline show the movement.

JSON export plus the bdna tool tracks regressions across commits, as the README and the endjin
guidelines describe.

Wiring

• New solutions/Z3.Linq.Benchmarks/ (Exe, IsPackable=false), referencing Z3.Linq.
• BenchmarkDotNet 0.15.8 added to central package management; the project references it
  version-less like every other package here.
• Added to Z3.Linq.slnx, so it builds with the solution (validated) but - being a plain Exe, not
  a test project - is not run by dotnet test.
• CS1591 suppressed as on the test/examples/demo projects; a [Benchmark] method is a tool
  surface, not an API.
• BenchmarkDotNet.Artifacts/ was already in .gitignore; no artifacts are committed.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors and
  documentation generation on
• The suite runs: dotnet run -c Release --project solutions/Z3.Linq.Benchmarks -- --filter '*' --job dry
  executed all six benchmarks and produced the memory table above
• 322/322 tests unchanged - this PR adds no library code
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings, with the new project in
  the build

Release note

No library or public-API change - a developer tool that ships with the source, not the package.
Releases remain on hold under #60 regardless.

🤖 Generated with Claude Code

[github-actions]

Test Results

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

Results for commit a4b7859. ± Comparison against base commit d018cd2.