Support byte, sbyte and ushort as bounded integer symbols

[HowardvanRooijen]

Makes byte, sbyte and ushort usable as symbols - the case the bit-vector work (#101) left
with no user-side workaround: a byte or ushort member on an environment type a caller cannot
rewrite to uint.

Why they are integers, not bit-vectors

#101 explained that byte/ushort cannot be bit-vectors: C# promotes them to int in every
expression, so byte & byte is computed in int space, and a bit-vector byte symbol would lose
its sort at the Convert(byte -> int) the compiler inserts. This PR maps them to the integer
sort instead, which turns that same promotion into a no-op - the symbol is already an integer, so
Convert(byte -> int) passes straight through. That is exactly the mechanism that already makes
short work; byte, sbyte and ushort are its remaining siblings.

So they support equality, ordering and arithmetic; they do not support bitwise operators or
shifts, which have no integer counterpart and need uint/ulong.

The change

Additive, ~20 lines of library code:

• TryGetSymbolSort gains sbyte/byte/ushort in its integer row.
• GetBounds gains their ranges - [0,255], [-128,127], [0,65535] - so A short symbol is not bounded to short's range, so Z3 can pick a value it cannot hold #87 bounds a value
  the type cannot hold to unsatisfiable rather than reading it back wrong.
• Both read paths gain checked reads, like short.
• VisitConstantValue folds them into the integer-constant arm.

Measured across every shape: round-trip (incl. each boundary), Optimize returning the type's
extreme (byte -> 255, sbyte -> -128, ushort -> 65535), out-of-range -> unsatisfiable,
arithmetic, and array elements.

Enum and cast consequences, handled

Two existing pins changed subject because the supported-type set grew, and both are updated to
match the new truth rather than worked around:

• Every enum underlying type is now supported (byte/sbyte/short/ushort/int/long
  -> integer, uint/ulong -> bit-vector). So a byte-backed enum now round-trips like an
  int-backed one - measured. Solve_EnumPropertyWithAnUnsupportedUnderlyingType_ThrowsNotSupportedException
  becomes Solve_ByteBackedEnumProperty_RoundTripsTheValue. (Member-constraining is still Enum symbols are not constrained to the members of the enum #97.)
• The unmapped-cast pin moves from (byte) to (nint). byte is now a mapped type, so a
  cast to it resolves; nint's TypeCode is Object, which the mapping genuinely has no row
  for, so it still hits the conversion catch-all.

Tests

305 -> 321. A new SmallIntegerSymbolTests for the three types, plus the two repointed pins above
and the removal of the byte-not-supported pin from #101.

Test	Covers
Solve_{Byte,SByte,UShort}Symbol_RoundTripsTheValue	round-trip, each with boundary rows
Solve_ByteSymbolsInArithmetic_RoundTripTheValues	promotion is a no-op against the int-sorted symbols
Optimize_{Byte,SByte,UShort}Symbol{Max,Min}imised_*	the range bound makes the extreme the type's extreme
Solve_ByteSymbolConstrainedOutsideItsRange_IsUnsatisfiable	#87 bound enforced
Solve_ByteBitwise_ThrowsNotSupported	bitwise still refused - byte is an integer, not a bit-vector
Solve_ByteArrayElement_RoundTripsTheValue	the element read arm
Solve_ByteBackedEnumProperty_RoundTripsTheValue (repointed)	enum underlying types all supported

Mutation results

Mutation	Failures	Which
byte/sbyte/ushort not mapped to a sort	17	every small-integer test, the arithmetic and element ones, and the byte-backed enum
No byte bounds row	2	the byte maximise and out-of-range tests
No ushort bounds row	1	the ushort maximise test
No sbyte bounds row	1	the sbyte minimise test

The doc guard from #82 also earned its place mid-change: an unbalanced <para> in the reworded
BitVectorWidth remark was a CS1570 build error, caught and fixed before it could ship.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors and
  documentation generation on
• 321/321 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 89.0% -> 88.5% line (916 of 1034), 77.2% -> 78.2% branch (607 of 776); the line
  percentage dips only because the two read switches gained three arms each that the scalar tests
  exercise but the element tests reach for one type

Release note

Releases remain on hold under #60 until Microsoft.Z3 5.x reaches nuget.org, so this reaches main
but not consumers. The public surface gains byte/sbyte/ushort symbol support; nothing is
removed.

[github-actions]

Test Results

  1 files  ± 0    1 suites  ±0   10s ⏱️ -1s
308 tests +14  308 ✅ +14  0 💤 ±0  0 ❌ ±0 
321 runs  +16  321 ✅ +16  0 💤 ±0  0 ❌ ±0 

Results for commit eb2485f. ± Comparison against base commit 106735e.