Cut per-solve managed allocations by caching per-type reflection

[HowardvanRooijen]

Uses the Z3.Linq.Benchmarks suite from the PR below it to find, fix and verify a memory hot
path: every Solve/Optimize re-does reflection whose answer is fixed for the life of the
environment type, and the collection marshaller allocates twice over. Caching the reflection and
filling the collection array in place cuts managed allocation per solve by ~18-26% across every
shape, with no behaviour change.

The hot path the benchmarks pointed at

Running the suite (BenchmarkDotNet, MemoryDiagnoser) and reading the Allocated column - which
is deterministic, unlike the native-bound Mean - the per-solve managed allocation is dominated by
the library rebuilding, from reflection, what it already knew:

• The TheoremVariableTypeMappingAttribute on a member's type is looked up three times per member
  per solve - once in the environment builder, once in the bounds asserter, once in the marshaller
  • and each lookup allocates an attribute array, even though almost no type carries the attribute.
• GetProperties/GetFields hand back a fresh array on every call, so the environment builder
  reallocates the member list of every type on every solve.
• The global- and predicate-rewriter attribute lookups allocate an array to ask a yes/no question;
  the predicate one runs once per call node in every constraint.
• The anonymous-type check allocates an attribute array via GetCustomAttributes(...).Any().
• The collection marshaller fills an ArrayList (a boxed object[] backing store) and then copies
  it into a typed array with ToArray - two arrays where one will do.

The fix

All small, local, and behaviour-preserving:

Change	Effect
Cache TheoremVariableTypeMappingAttribute per type (absence cached too)	3 reflection calls + array allocs per member per solve -> one dictionary lookup
Cache public instance property/field arrays per type	no GetProperties/GetFields array per type per solve
IsDefined guard on the global- and predicate-rewriter lookups	no attribute array on the common no-rewriter path
IsDefined for the anonymous-type CompilerGenerated check	no attribute array
Fill a typed array in place in the collection marshaller	no ArrayList, no boxed object[] backing store, no copy-out array

The cached arrays are private and only ever read, so sharing one instance is safe. Nothing changes
about what a solve computes - only how much it allocates getting there.

Verified

Measured with Z3.Linq.Benchmarks (short job, MemoryDiagnoser), same machine, before vs after:

Shape	Allocated before	Allocated after	Reduction
ScalarSymbols	4.48 KB	3.32 KB	-25.9%
ValueTuple	4.51 KB	3.39 KB	-24.8%
NestedObject	6.44 KB	4.93 KB	-23.4%
Collection	5.59 KB	4.60 KB	-17.7%
WideSymbols	8.05 KB	6.23 KB	-22.6%
Optimize	5.44 KB	4.30 KB	-21.0%

• No time claim. Each solve creates and disposes a native Z3 context, which dominates the
  wall-clock and swamps the managed work; the short-job Mean values move in both directions well
  inside their error bars. Allocated is the metric that is stable enough to stand behind, and it
  is what a caching change is expected to move.
• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors and
  documentation generation on.
• 322/322 tests green in Release, unchanged - the marshalling, bounds, rewriter and
  anonymous/named/nested/collection paths this touches are all covered, so the identical test pass
  is the behaviour-preservation evidence.
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings.

Release note

No public-API or behaviour change - an internal allocation reduction on the solve path. Releases
remain on hold under #60 regardless.

🤖 Generated with Claude Code

[github-actions]

Test Results

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

Results for commit 323baca. ± Comparison against base commit a4b7859.