Choose numeric conversions by sort, not by target type

[HowardvanRooijen]

Fixes #76.

The defect

A double symbol could not be compared against a float variable:

float f = 1.5f;
using var context = new Z3Context();
context.NewTheorem<Symbols<double, int>>().Where(t => t.X1 == f).Solve();
// System.InvalidCastException: Unable to cast object of type 'Microsoft.Z3.RatNum'
//                              to type 'Microsoft.Z3.IntExpr'

C# widens the float to double, so the tree carries a Convert(Single -> Double) node, and the
visitor chose the conversion from the node's target type alone: every conversion to double was
MkInt2Real, on the assumption that the operand must have been an integer. Here it was a real.

It is wider than the issue says. Measured before the change, sixteen shapes:

Constraint	Before
double symbol == float variable - the issue	InvalidCastException
double symbol == (double) of a float or decimal variable	InvalidCastException
double symbol == float symbol	InvalidCastException
double symbol == float symbol * 2	InvalidCastException
long symbol == int symbol	NotImplementedException - no arm for long at all
decimal symbol == int symbol	NotImplementedException - no arm for decimal
float symbol == int symbol	NotImplementedException - no arm for float
float symbol == (float) of a double variable	NotImplementedException
double symbol == int, long or short variable, or int symbol	worked - the one widening the arm was written for
double symbol == float literal	worked - folded to a double constant before the visitor sees it, which is why the issue needed a variable

The bold rows are two symbols of the library's own supported types that could not appear in the
same constraint. Nothing about Symbols<double, float> or Symbols<long, int> suggests its
members cannot be compared.

The change

A numeric conversion means one of three things in Z3, and which one depends on the sorts, not
the CLR types: nothing at all when both types map to the same sort, integer-to-real, or
real-to-integer. The visitor now asks for the target type's sort from the same mapping the
symbols are declared with - TryGetSymbolSort, which #64 made the single source for that
question and which becomes internal here - and decides from that and the operand's sort:

if (inner.Sort.Equals(targetSort))              return inner;
if (inner.IsInt  && targetSort is RealSort)     return context.MkInt2Real((IntExpr)inner);
if (inner.IsReal && targetSort is IntSort)      return context.MkReal2Int((RealExpr)inner);

That replaces the switch on the target type, including the when inner.IsInt arm #63 added for
short and enums - which was this rule for one row. The mutation matrix shows the #63 coverage
carrying over: dropping the same-sort branch fails every short and enum test #63 wrote.

A conversion to a type the mapping has no row for still falls through to the existing catch-all,
with its message unchanged.

One behaviour changed on purpose beyond the issue. The char arm passed an integer operand
through and threw for a real one; a real operand converted to char now goes through
MkReal2Int, as it does for int. No test exercised the char arm in either direction; it is
kept as an integer-sort target so the integer case is unchanged.

Measured after the change

All sixteen shapes round-trip: the issue's repro gives 1.5, double == float symbol gives
1.5 on both sides, double == float * 2 gives 3, long == int symbol gives 5,
decimal == int symbol gives 7, float == int symbol gives 3, and every shape that worked
before still gives the same value.

Tests

230 → 239. A new NumericConversionTests.cs for the shapes above, since they are a subject of
their own rather than a marshalling detail, and one pin repointed.

Test	What it covers
Solve_DoubleSymbolComparedToAFloatVariable_RoundTripsTheValue	the issue's repro
Solve_DoubleSymbolComparedToAFloatSymbol_RelatesTheTwo / ..InArithmeticWithAFloatSymbol..	two symbols of different real types, directly and under a multiplication
Solve_DoubleSymbolComparedToAnIntSymbol_RelatesTheTwo	the widening the old arm handled - so the fix cannot be a regression in disguise
Solve_DecimalSymbolComparedToAnIntSymbol_RelatesTheTwo / ..Float..	the two real targets that had no arm
Solve_LongSymbolComparedToAnIntSymbol_RelatesTheTwo	the integer target that had no arm - the former "unsupported cast" pin, now positive
Solve_DoubleSymbolComparedToAWidenedDecimalVariable.. / Solve_FloatSymbolComparedToANarrowedDoubleVariable..	explicit casts between real types, widening and narrowing, both no-ops in Z3
Solve_CastToAnUnmappedType_ThrowsNotImplementedException (in UnsupportedExpressionTests)	the catch-all, repointed from (long) - which now works - to (byte), which the mapping has no row for

The real-to-integer direction already has its test from #63,
Solve_DoubleSymbolCastToInt_ConvertsRatherThanPassingThrough, which stays where it is.

Mutation results

Mutation	Failures	Which
Drop the same-sort no-op branch	20	the six new no-op cases, every short and enum test from #63, the short collection tests from #64, and the anonymous every-scalar test from #75
Drop the integer-to-real branch	3	double, decimal and float symbols against an int symbol - and nothing else in the suite, which is why the regression guard is there
Drop the real-to-integer branch	1	the #63 cast test alone

The first row is the useful one: four earlier fixes in this stack all ran through the arm this
change replaces, and all of them still fail when it is wrong.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 239/239 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 88.1% -> 88.5% line (689 of 778), 76.5% -> 77.2% branch (451 of 584)

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

Results for commit 1a7f5ec. ± Comparison against base commit c8c015d.