Marshal anonymous environments like every other shape

[HowardvanRooijen]

Fixes #75.

The defect

An anonymous environment holding a nested object threw a bare NullReferenceException from
inside the native interop:

public sealed class Leaf { public int A { get; set; } }

using var ctx = new Z3Context();
ctx.NewTheorem(new { inner = new Leaf(), n = default(int) }).Where(t => t.n == 1).Solve();
// System.NullReferenceException: Object reference not set to an instance of an object.

A nested environment has no Z3 handle of its own, only children. The three evaluation sites in
ConvertZ3Expression guard against that null and throw an ArgumentException naming the member;
the fourth site - the anonymous-type branch of GetSolution - evaluated the handle before looking
at the type, so the null went straight to Model.Eval. The NotSupportedException two lines
later, which would at least have named the property, was never reached.

Why the fix is bigger than the issue suggested

#75 proposed moving the type check above the evaluation, so the existing NotSupportedException
fires first. That would have improved the message and kept the branch as it was: a third copy of
the marshaller, handling bool and int only, so that a double, long, string,
decimal, short, float or DateTime that is perfectly usable in a named environment was
refused in an anonymous one - pinned in EnvironmentTypeTests as "a real restriction rather
than a defect".

Measured, the alternative costs less and delivers more. Replacing that branch's marshaller with a
call to ConvertZ3Expression - the one every other environment shape uses - makes all of the
following work, with nothing else changed:

Shape	Before	After
new { inner = new Leaf(), n = 0 } - the issue's repro	NullReferenceException	inner constructed, n = 1
the same, constrained through it: t.inner.A == 5	NullReferenceException	inner.A = 5
new { inner = new { a = 0 }, n = 0 } - nested anonymous	NullReferenceException	inner.a = 4
new { p = new Pair(), n = 0 } where Pair has a double	NullReferenceException	p.Y = 2.5
double, long, string, decimal, short, float, DateTime properties	NotSupportedException	each round-trips exactly
new { v = new int[2], n = 0 }	NotSupportedException: Unsupported parameter type for v.	NotSupportedException: ... a collection in an anonymous environment cannot be pre-sized.

So #75 stops being a bad diagnostic on an unsupported shape and becomes a supported shape. The
scope was put to the maintainer with these numbers and chosen over the diagnostic-only fix.

The change

field.SetValue(result, ConvertZ3Expression(result, context, model, subEnv, parameter));

replaces the inline bool/int chain. A nested object is materialised by the recursion inside
ConvertZ3Expression - the same recursion that handles it for a named environment - rather than
evaluated here, so the null never reaches Z3 because nothing evaluates it.

Collections are the one exception, and are refused by name. The shared path reads the element
count from the collection already on the instance, and an anonymous instance is created
uninitialised - NewTheorem<T>(T dummy) discards the argument, as its parameter name says - so
there is nothing to read. Without a guard that is #78's NullReferenceException on the count;
with it, the message says which member and why. The guard uses a new IsCollection helper, which
also replaces the two places in GetEnvironment that spelled the same test out inline.

EvaluateWithCompletion takes a non-nullable Expr again. #51 made it Expr? for exactly
one reason - this branch passed a nullable - and documented that in a paragraph of remarks. Both
the annotation and the paragraph are gone; the clean build under TreatWarningsAsErrors is the
compiler confirming no caller can hand it a null any more.

Net: 26 lines out, 28 in, in Theorem.cs.

Tests

225 → 230, in EnvironmentTypeTests.cs.

Test	What it covers
Solve_AnonymousTypeWithAnUnconstrainedNestedObject_ConstructsIt	#75's repro verbatim - the nested object is not even constrained
Solve_AnonymousTypeWithANestedObject_PopulatesTheNestedProperties	the same shape constrained through the anonymous root, including a constraint across the nesting boundary
Solve_AnonymousTypeWithANestedAnonymousType_PopulatesIt	the recursion re-entering the anonymous branch
Solve_AnonymousTypeWithDoubleProperty_PopulatesIt	the former ThrowsNotSupportedException pin, now a round-trip
Solve_AnonymousTypeWithEveryScalarType_PopulatesEachOne	nine properties, one of each supported type, in a single anonymous environment - a regression to a marshaller that knows some of them fails by name rather than passing on the two it handled
Solve_AnonymousTypeWithACollectionProperty_ThrowsNotSupportedException	the guard; asserts the member name and the reason are both in the message

Three existing remarks that described the anonymous branch's separate evaluation call are
rewritten to say what is now true.

Mutation results

Mutation	Failures	Which
Drop the collection guard	1	the collection pin alone - it becomes #78's NullReferenceException
Restore the old bool/int marshaller	5	the double round-trip, the every-scalar test, and all three nested-object tests. Solve_AnonymousTypeEnvironment_PopulatesEveryProperty and the unconstrained-property test stay green, because they are bool and int - which is precisely why the restriction survived as long as it did

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 230/230 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage: line unchanged at 88.1% (683 of 775, from 687 of 779); branch 77.0% -> 76.5% (444 of 580, from 456 of 592). Both totals fall because the removed bool/int chain was covered code with covered branches - twelve branches no longer exist - and the one-line call that replaces it has none

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org, so this reaches main
but not consumers. Nothing about the hold changes.

[github-actions]

Test Results

  1 files  ±0    1 suites  ±0   5s ⏱️ +2s
219 tests +5  219 ✅ +5  0 💤 ±0  0 ❌ ±0 
230 runs  +5  230 ✅ +5  0 💤 ±0  0 ❌ ±0 

Results for commit c8c015d. ± Comparison against base commit 2735c6e.