Give collections the same sorts as scalars

[HowardvanRooijen]

Fixes #64.

The defect

Collection symbols only worked with int elements. Every other element type built a Z3 array
whose domain or range contradicted how its elements were constrained and read back, and the
theorem threw a raw Z3Exception about sorts:

public class Env { public long[] Values { get; set; } = new long[2]; public int Length { get; set; } }

using var context = new Z3Context();
context.NewTheorem<Env>().Where(t => t.Values[0] == 1L).Where(t => t.Length == 2).Solve();
// Microsoft.Z3.Z3Exception: Sorts (_ BitVec 64) and Int are incompatible

The array sort mapping - which existed in two identical copies - paired a domain and a range per
element type:

Element	Domain (index)	Range (element)	What was wrong
int	Int	Int	nothing - the only self-consistent row
short	Int	BitVec 16	range: constraints translate to Int
long, DateTime	Int	BitVec 64	range
bool	Bool	Bool	domain: elements are read with an integer index
string	String	BitVec 16	both
float, decimal	Real	FloatingPoint 8 24	range - and a decimal could never have fitted
double	Real	FloatingPoint 11 53	range

Measured before the change, every non-int type failed in one of two places depending on the
constraint - during translation when it named a constant of the element type, or in the
marshalling loop when the elements were left free - which is why the tests cover both shapes.
bool and string failed in the same place either way, because the index is supplied by the
library rather than by the constraint.

The change

The collection mapping is deleted. There is one function from CLR type to sort, and a
collection is an array from Int to whatever that function says a scalar of the element type
is.

private static Sort? TryGetSymbolSort(Context context, TypeCode typeCode) => typeCode switch
{
    TypeCode.String => context.StringSort,
    TypeCode.Int16 or TypeCode.Int32 or TypeCode.Int64 or TypeCode.DateTime => context.IntSort,
    TypeCode.Boolean => context.BoolSort,
    TypeCode.Single or TypeCode.Decimal or TypeCode.Double => context.RealSort,
    _ => null,
};

The scalar path calls it for its constant; both collection paths call it for their range and use
Int for their domain. That is the actual fix, not the corrected table: the defect was two
mappings that could drift, and now there is nothing to drift. The mutation matrix below is the
evidence - reverting one row of the shared mapping fails scalar and collection tests together.

The rest is 54 net lines removed, three NotSupportedException messages preserved exactly, and
one more thing:

The array-element read for short gets the checked cast the scalar arm has had since #63.
That arm was unreachable until this change - noted on #64 at the time, with the reason - and is
covered for the first time here, including the overflow pin.

Measured after the change

Every element type, both shapes, arrays and List<T>:

Element	Constrained	Free elements
long	[9000000000, -9000000000] exact	[0, 0]
bool	[true, false]	[false, false]
double	[1.5, -2.25]; relational [3.5, 7]	[0, 0]
float	[1.5, 0.1] - the array half of #54, observable for the first time	[0, 0]
decimal	[1.5, 0.1]; decimal.MaxValue exact, 29 significant digits	[0, 0]
string	["abc", ""]	["", ""]
DateTime	two instants exact, kind Utc	1601-01-01Z, file time zero, kind Utc
short	[4, 6] through arithmetic; out-of-range → OverflowException	[0, 0]

decimal.MaxValue is the load-bearing one. No floating-point sort Z3 offers could return it
exactly, so it passing is direct evidence the range is an unbounded Real rather than a wider
float that would pass the ordinary values and lose precision quietly on large ones.

What is deliberately not changed

Object collections stay broken, and are now #89. A Holder[] whose elements have scalar
properties fails in every shape - constraining t.Items[0].Value dies in the visitor
(Unknown parameter encountered: Value), and leaving the elements free dies in the marshaller
(requires subEnv.Expr to be non-null). Measured before and after this change; identical.
It is a different mechanism from #64: the library builds one per-property array for these and
then neither end of the pipeline can use it, and Environment.IsArray - the flag that would
route either end - is written and never read. The per-property arrays now go through the shared
mapping, so the sort side is settled for whoever finishes it. The library's own error message,
Only one level of object collections is currently supported, promises something that does not
work; #89 says so.

#87 applies to elements too. A short element is an unbounded Int exactly as a short
scalar is, so Z3 can still pick a value the element cannot hold. The checked read makes that loud
rather than wrong, which is the same trade-off #63 made and for the same reason.

Tests

214 → 225, in CollectionSymbolTests.cs. The nine characterisation pins that asserted the old
failures are replaced by round-trips, and the three #55 tests - which until now could only
observe that fix in which type the failing cast named - become positive tests that reverting
#55 fails outright.

Test	What it covers
Solve_LongArraySymbol_RoundTripsEveryElement / ..LongList.. / ..LongArrayInAPublicField..	the range fix; values beyond Int32 so a narrowing read cannot pass by accident
Solve_BoolArraySymbol.. / ..BoolList..	the domain fix
Solve_StringArraySymbol_RoundTripsEveryElement	both halves were wrong; includes "" so a constrained element is distinguishable from a free one
Solve_DoubleArraySymbol.. / ..WithRelationalConstraints..	real range; the relational shape the int tests use, now available to every type
Solve_FloatArraySymbol_RoundTripsEveryElement	the first test ever to reach the element loop's Single arm
Solve_DecimalArraySymbol_RoundTripsEveryElement / ..AtFullPrecision / ..DecimalList..	real range; decimal.MaxValue proves it is not a float
Solve_DateTimeArraySymbol.. / ..DateTimeList.. / ..WithFreeElements_ReadsBackAsUtc	the row a comment on #64 had already measured; kind asserted where the value cannot be
Solve_ShortArraySymbol_RoundTripsEveryElement	three stacked defects - #64, the #63 guard over a select, and the element arm's Int16 case
Solve_ShortArrayElementConstrainedOutsideShortRange_ThrowsOverflowException	the checked read; the only thing between current behaviour and a silent wrap
Solve_DecimalArrayWithFreeElements_ReturnsTheInitialisedLength and siblings	#55, now covered by a passing test instead of an exception message

Mutation results

Mutation	Failures	Which
Domain back to the element sort	3	bool array, bool list, string array - exactly the domain cases. Real-domained arrays tolerate an integer index, which is why double did not fail on domain in the original table either
Shared mapping: real row → FloatingPoint	43	double/float/decimal scalars and collections together, across five test files
Shared mapping: long/DateTime row → BitVec 64	18	long/DateTime scalars and collections together
Revert #55	6	every decimal collection test
Element short read unchecked	1	the overflow pin alone
Object-collection per-property arrays: domain back to the element sort	0	unreachable behind #89 - stated rather than implied

The second and third rows are the point of the design. Before this change a wrong row in the
collection mapping failed only collections and the scalar suite stayed green; that is how #64
went unnoticed. Now there is no row that can be wrong for one and not the other.

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 225/225 locally
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 78.3% -> 88.1% line (687 of 779) and 70.9% -> 77.0% branch (456 of 592). Most of the line movement is 82 coverable lines that no longer exist - the two copies of the collection mapping - rather than new coverage; the twelve newly covered lines are the element arms this change made reachable

New issue

#89 - object collections cannot be constrained or read back. Found by probing whether the
second copy of the mapping was reachable; it is not, by any theorem.

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   3s ⏱️ -1s
214 tests +11  214 ✅ +11  0 💤 ±0  0 ❌ ±0 
225 runs  +11  225 ✅ +11  0 💤 ±0  0 ❌ ±0 

Results for commit 2735c6e. ± Comparison against base commit 18d4971.