Size collections from the instance passed to NewTheorem

[HowardvanRooijen]

Fixes #78.

The defect

A collection symbol takes its length from the collection already on the solution instance, and
read it with no null check:

private sealed class Env { public int[]? Values { get; set; } }   // no initialiser

using var ctx = new Z3Context();
ctx.NewTheorem<Env>().Solve();
// System.NullReferenceException: Object reference not set to an instance of an object.

Two halves, as the issue puts it. The diagnostic half: a forgettable mistake produced a bare
NRE with nothing naming the member - in an environment with several collections, nothing said
which. The structural half: a value tuple could never hold a collection at all, because the
instance is built with Activator.CreateInstance and a tuple has nowhere to put an initialiser.
Nothing the caller could write fixed that.

Measured before the change: a null field, a null property, a null List<T>, a null collection on
a nested object, and a tuple - with or without element constraints - all threw the same bare NRE.

The change

The instance passed to NewTheorem(T) is now the template for the solution. That overload
already existed; its parameter was named dummy and the method discarded it. Its collections
now give the solution's collections their length, so:

ctx.NewTheorem((Values: new int[2], Other: 0))
   .Where(t => t.Values[0] == 3)
   .Where(t => t.Values[1] == 4)
   .Solve();                                  // (Values: [3, 4], Other: ...)

works, and so does an anonymous type with a collection - which #75 had to refuse by name two PRs
ago, for exactly the reason this fixes: the anonymous instance is created uninitialised, and the
initialised one the caller passed was being thrown away.

Rules, each pinned by a test and a mutation:

• The template beats the type's own initialiser. The caller who passes an instance has said what
  they want more directly than the type has. With no template, the initialiser applies as before.
• The template is followed into nested objects: the recursion carries the corresponding member
  of the template alongside the environment.
• It survives Where (each of which builds a new theorem) and reaches the optimiser, so
  OrderBy sees it.
• Only lengths are read. The template's element values do not reach the solution, and the
  template is never written to.
• A collection with no length from either source is rejected by name:
  Collection symbol B has no length. A collection must be pre-sized: initialise it on the environment type, or pass an instance with it initialised to NewTheorem.

The //todo: deal with length in a more robust way that sat above the count read for years is
gone with it.

Public surface

Z3Context.NewTheorem<T>(T dummy) becomes NewTheorem<T>(T template) and reads the argument.
Binary-compatible; source-breaking only for a caller using the named argument dummy:. The XML
documentation on the overload is rewritten to say what the instance is for, with a tuple example
beside the anonymous-type one.

This was put to the maintainer against the diagnostic-only fix the issue suggested as the safe
minimum, with the measurements above, and chosen.

Tests

239 → 247. Three pins rewritten in CollectionSymbolTests, one in EnvironmentTypeTests, and
new coverage for each rule.

Test	What it covers
Solve_NullCollectionInAPublicField_ThrowsNotSupportedExceptionNamingIt / ..Property..	the diagnostic; the message starts with the member name
Solve_TwoCollectionsWithOneUnsized_NamesTheUnsizedOne	the point of naming it - A is sized, B is not, and the message says B
Solve_CollectionInAValueTupleEnvironment_IsSizedByTheTemplate	the structural half: a tuple holding a collection, for the first time
Solve_CollectionInAValueTupleEnvironmentWithoutATemplate_ThrowsNotSupportedException	the type-only overload still has nothing to size a tuple from, and says so - naming Item1, which is what the field is called at runtime
Solve_NullCollectionProperty_IsSizedByTheTemplate / ..NullGenericCollection.. / ..InANestedObject..	a class, a List<T>, and a collection two levels down
Solve_TemplateCollection_TakesPrecedenceOverTheInitialiser	the type says three, the template says five, the answer is five
Solve_TemplateElementValues_DoNotReachTheSolution	template [99, 99], solution constrained to 1; the template is untouched afterwards
OrderByDescending_OnATemplatedTheorem_KeepsTheTemplate	the optimiser path
Solve_AnonymousTypeWithACollectionProperty_SizesItFromTheTemplate (in EnvironmentTypeTests)	the #75 refusal, now a round-trip

Mutation results

Mutation	Failures	Which
Count read ignores the template	9	every templated test
Initialiser beats the template	1	the precedence test alone
Where drops the template	9	every templated test - all of them go through Where
The optimiser path drops the template	1	the OrderBy test alone
No null check - the old cast	4	the four diagnostic pins, which become NREs again

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 247/247 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 88.5% -> 88.1% line (693 of 786) and 77.2% -> 77.5% branch (459 of 592). Eight more coverable lines, four of them covered: the uncovered four are the two constructor overloads that keep the old signatures and the unreachable default arm of the new member-reading helper

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   6s ⏱️ -1s
236 tests +8  236 ✅ +8  0 💤 ±0  0 ❌ ±0 
247 runs  +8  247 ✅ +8  0 💤 ±0  0 ❌ ±0 

Results for commit 4acc666. ± Comparison against base commit 1a7f5ec.