Bound each integer symbol to the range of its type

[HowardvanRooijen]

Fixes #87.

The defect

A short, int, long or DateTime symbol travels through Z3 as an unbounded integer, and
nothing told Z3 the range of the type. A constraint no value of the type could satisfy still had a
model, and the failure came on the way out:

using var ctx = new Z3Context();
int beyondShortRange = 40000;

ctx.NewTheorem<Symbols<short, int>>().Where(t => t.X1 == beyondShortRange).Solve();
// System.OverflowException     - from the checked read #63 added; loud, but the wrong answer

There is no short equal to 40000. The theorem is unsatisfiable, and that is what should come back.

#87's own table needs one correction. It recorded the int route as unreachable, because a
comparison against a long variable fell into the conversion catch-all. #76 made that widening a
no-op and the route opened: measured before this change, t.X1 == 3_000_000_000L on an int
symbol solves and the read throws Z3Exception: Numeral is not an int. Recorded on the issue.

Measured before, twelve shapes. The other finding worth stating: optimising a symbol with no
other bound returned an arbitrary value - zero, every time - because Z3 reports an unbounded
objective and supplies whatever model it likes. Maximising a short gave 0.

The change

The bounds are asserted alongside the constraints. AssertConstraints now walks the
environment and, for every scalar symbol whose type has a range - short, int, long,
DateTime in ticks - asserts low <= symbol <= high, descending into nested objects. An enum
is its underlying type and is bounded as one.

Shape	Before	After
short == 40000 (via an int variable)	OverflowException on the read	unsatisfiable
int == 3_000_000_000L	Z3Exception: Numeral is not an int	unsatisfiable
DateTime > DateTime.MaxValue, < DateTime.MinValue	OverflowException from the #83 guard	unsatisfiable
maximise a short with no other bound	0	32767
maximise an int / minimise a long	0	2147483647 / -9223372036854775808
maximise / minimise a DateTime	0001-01-01	9999-12-31T23:59:59.9999999Z / 0001-01-01
short == short.MaxValue, == short.MinValue	worked	unchanged - the bounds are inclusive
DateTime[] element > DateTime.MaxValue	OverflowException naming the symbol	unchanged - see below

Only scalars are bounded, deliberately. A collection is an array from Int to the element
sort; its length is not known when the constraints are asserted - it comes from the instance when
the solution is read - and bounding every element would take a quantifier, which can cost Z3 its
completeness. So an element keeps the checked read from #63 and the guard from #83, and a value
outside its type is loud rather than wrong. The last row of the table, and the two element tests,
hold that in place; the comments on both reads now say which case each is for.

The bounds are not logged. TheoremCompositionTests counts logged lines, and the log is for
the constraints the caller wrote.

No existing test changed its answer. Sudoku, the shipping and oil problems, every
optimisation test - all pass unchanged, because every one of them bounds its symbols itself, as a
caller normally does. The bounds only matter at the edges, which is where they were missing.

Tests

270 → 281. Three pins rewritten from "throws" to "unsatisfiable", and a new SymbolBoundsTests.

Test	What it covers
Optimize_ShortSymbolMaximised_ReturnsShortMaxValue / ..Minimised.., ..Int.., ..Long.., ..DateTime.. ×2	one per type: the extreme of the type, which was an arbitrary value before. Each fails by itself if its type's row of the bounds is dropped
Solve_IntSymbolConstrainedBeyondIntRange_IsUnsatisfiable	the route #87 recorded as unreachable, which #76 opened
Solve_ShortSymbolAtBothEndsOfItsRange_IsSatisfiable	the bounds are inclusive - the extremes are still values
Optimize_ShortSymbolInANestedObjectMaximised_ReturnsShortMaxValue	the walk descends into nested objects
TryOptimize_ShortSymbolConstrainedOutsideItsRange_ReturnsFalse	the optimiser path reports unsatisfiable too
Solve_ShortSymbolConstrainedOutsideShortRange_IsUnsatisfiable, Solve_DateTimeSymbolConstrainedBeyondMaxValue_IsUnsatisfiable, ..BelowMinValue..	the three former overflow pins, now the true answer
Solve_DateTimeArrayElementConstrainedBeyondMaxValue_ThrowsOverflowExceptionNamingIt (in CollectionSymbolTests)	the #83 guard, now reachable only through an element, kept load-bearing

Mutation results

Mutation	Failures	Which
Bounds never asserted	11	eight of the new bounds tests and the three rewritten pins. Two survive by coincidence, not by passing: minimising a DateTime returns tick 0, which is MinValue, and the inclusive-ends test is satisfiable with or without the bounds
No row for short	5	the three short tests, the nested-object test, and the short TryOptimize
No row for DateTime	3	both DateTime optimisation extremes and the beyond-range unsatisfiability
No descent into nested objects	1	the nested-object test alone
Bounds exclusive rather than inclusive	16	every extreme test - the extreme is now excluded - plus the inclusive-ends and the #83 max-value round-trip

New issue

#97 - an enum symbol is bounded as its underlying integer, not to the members of the
enum: maximising a DayOfWeek symbol now returns (DayOfWeek)2147483647. Before this change it
returned Sunday only because Z3 supplied zero for an unbounded objective; nothing was respecting
the enum either way. A different rule - membership, not range - with a [Flags] question attached,
so raised rather than folded in.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors and
  documentation generation on
• 281/281 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 88.7% -> 88.9% line (820 of 922); branch 78.8% -> 78.6% (557 of 708). The branch percentage slips because the two new switches carry defensive default arms the guard above them makes unreachable - GetBounds is only called when the symbol is an IntExpr, which is only short/int/long/DateTime, so its _ => null never runs, and SymbolType only ever sees a property or a field. Both are there for exhaustiveness, and both count as uncovered

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   9s ⏱️ ±0s
270 tests +11  270 ✅ +11  0 💤 ±0  0 ❌ ±0 
281 runs  +11  281 ✅ +11  0 💤 ±0  0 ❌ ±0 

Results for commit c9035f4. ± Comparison against base commit 3615d7b.