Encode a DateTime as ticks rather than a file time

[HowardvanRooijen]

Fixes #83.

The defect

A DateTime travelled through Z3 as a Windows file time - 100ns intervals counted from
1601-01-01 UTC - so nothing earlier could be written or read:

using var ctx = new Z3Context();
var y1500 = new DateTime(1500, 1, 1, 0, 0, 0, DateTimeKind.Utc);

ctx.NewTheorem<Symbols<DateTime, int>>().Where(t => t.X1 == y1500).Solve();
// System.ArgumentOutOfRangeException: Not a valid Win32 FileTime.
//   - during translation, before Z3 sees the theorem

ctx.NewTheorem<Symbols<DateTime, int>>().Where(t => t.X1 < y1601).Solve();
// System.ArgumentOutOfRangeException: Not a valid Win32 FileTime. (Parameter 'fileTime')
//   - after Z3 found a model, while reading it back

Roughly two thirds of the type's range was unusable, and the second shape is the worse one:
nothing about it is malformed, Z3 solves it, and the read path then refuses to express the answer

• blaming a fileTime parameter no caller supplied.

Measured before the change, fifteen shapes. Beyond the issue's rows: one tick before 1601 fails
on the write; a DateTime[] element before 1601 fails the same way; and
t.X1 > DateTime.MaxValue - which has no solution in DateTime terms - returns a model and
dies on the read with the fileTime message.

The change

Ticks instead of a file time. DateTime.Ticks counts from 0001-01-01 and covers the whole
range, fits an Int64 exactly as the file time did, and the encoding is internal, so nothing
outside the library depends on the choice. The write path becomes ExpressionVisitor.ToUtcTicks,
the two read paths become Theorem.ToDateTime.

#56's kind convention is kept exactly. ToFileTimeUtc converted a Local value to UTC and
took Unspecified to be UTC already; ToUtcTicks does the same, and the read path produces
Utc as before. Rows K and L of the probe - a Local constant coming back as the same instant in
UTC, an Unspecified constant coming back with identical ticks - are unchanged before and after,
and the #56 tests pass untouched.

The read is guarded, and the guard names the symbol. The symbol is an unbounded integer, so
t.X1 > DateTime.MaxValue still has a model in Z3; the guard turns that into

OverflowException: The value Z3 chose for the DateTime symbol X1 is outside the range a DateTime
can hold, 0001-01-01 to 9999-12-31. See https://github.com/endjin/Z3.Linq/issues/87.

rather than the constructor's complaint. The same trade-off as the checked read of a short
(#63): loud rather than wrong, until #87 bounds the symbol so Z3 cannot choose such a value. With
the encoding starting at tick zero, the bottom of the range is now reachable only by constraining
below DateTime.MinValue itself.

One visible change beyond the fix. An unconstrained DateTime symbol completes to
DateTime.MinValue rather than 1601-01-01, because completion supplies zero and zero now means
something else. The issue flagged this; no test asserted the old value, and the remarks that
mentioned it are updated.

Measured after the change

Shape	Before	After
== 1500-01-01, == DateTime.MinValue, one tick before 1601	ArgumentOutOfRangeException on the write	exact, Utc
DateTime[] element == 1500-01-01	ArgumentOutOfRangeException on the write	exact, Utc
< 1601-01-01	ArgumentOutOfRangeException on the read	1600-12-31T23:59:59.9999999Z
> DateTime.MaxValue, < DateTime.MinValue	ArgumentOutOfRangeException (Parameter 'fileTime')	OverflowException naming X1 and the range
== DateTime.MaxValue, == 1601-01-01, Local kind, Unspecified kind	worked	unchanged
unconstrained	1601-01-01Z	0001-01-01Z

Tests

247 → 254. The two #83 pins in SymbolTypeMarshallingTests are replaced, and the remarks across
three files that described the encoding as a file time now describe it as ticks.

Test	What it covers
Solve_DateTimeSymbolBefore1601_RoundTripsTheValue	years 1, 1066, 1500 and 1600 - the range the old encoding could not express, with MinValue as the bottom boundary
Solve_DateTimeSymbolOneTickBefore1601_RoundTripsTheValue	the exact boundary of the old encoding, from the wrong side
Solve_DateTimeSymbolConstrainedBefore1601_ReturnsAnInstantBefore1601	the read half of the issue - the theorem that solved and then threw
Solve_DateTimeSymbolConstrainedBeyondMaxValue_ThrowsOverflowExceptionNamingIt / ..BelowMinValue..	the guard, both ends; asserts the symbol name and the range are in the message
Solve_DateTimeArrayElementBefore1601_RoundTripsTheValue (in CollectionSymbolTests)	the element read has its own DateTime arm

Mutation results

Mutation	Failures	Which
Write path uses raw ticks, no Local → UTC conversion	2	the Local-kind test and the OrderByDescending DateTime test. Only on a machine with a non-zero UTC offset - this one is on BST - which is the same blind spot #56 recorded: UTC CI cannot see a Local/UTC confusion
Read path drops the range guard	2	the two overflow pins alone, which become ArgumentOutOfRangeException from the constructor
Read path produces Unspecified rather than Utc	15	every kind assertion across four files
Read path back on file time - the two ends disagree	15	every DateTime round-trip, including the #56 ones

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors and
  documentation generation on
• 254/254 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 88.1% -> 88.3% line (702 of 795), 77.5% -> 77.9% branch (469 of 602)

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 ⏱️ -1s
243 tests +7  243 ✅ +7  0 💤 ±0  0 ❌ ±0 
254 runs  +7  254 ✅ +7  0 💤 ±0  0 ❌ ±0 

Results for commit 1a458e4. ± Comparison against base commit fa9a42c.