Read a float symbol back as a float

[HowardvanRooijen]

Fixes #54.

The defect

TypeCode.Single read the model value with double.Parse:

case TypeCode.Single:
    value = double.Parse(((RatNum)val).ToDecimalString(32), CultureInfo.InvariantCulture);

so a solved float symbol came back boxed as a double, and the reflection write that follows
refused it:

using var ctx = new Z3Context();
ctx.NewTheorem<Symbols<float, int>>().Where(t => t.X1 == 1.5f).Solve();
// System.ArgumentException: Object of type 'System.Double' cannot be converted to
// type 'System.Single'.

Nothing else about the solve was wrong. Declaring the symbol (MkRealConst), translating the
constant and solving all succeeded; only the last step lost the answer. Measured across the shapes
a float symbol can take:

Shape	Before	After
X1 == 1.5f	ArgumentException	1.5
X1 == 0.1f - not exactly representable in binary	ArgumentException	0.1
X1 == 1.2345678f - eight significant digits	ArgumentException	1.2345678
X1 == -2.75f	ArgumentException	-2.75
X1 == float.MaxValue	ArgumentException	3.4028235E+38
2.5f < X1 < 2.75f	ArgumentException	2.625
unconstrained	ArgumentException	0
maximised with OrderByDescending	ArgumentException	4.5
in a public field, and in a nested object	ArgumentException	1.5
alongside a double symbol	ArgumentException	1.5 / 2.5
float[]	Z3Exception (#64)	Z3Exception (#64)
X1 * 3 == 1	FormatException (#6)	FormatException (#6)
X1 == float.Epsilon	FormatException (#6)	FormatException (#6)

The change

Two characters at each of two sites:

case TypeCode.Single:
    value = float.Parse(((RatNum)val).ToDecimalString(32), CultureInfo.InvariantCulture);

Why float.Parse rather than (float)double.Parse. The issue notes a design choice about
precision here. Parsing to double and narrowing rounds twice - to the nearest double, then to the
nearest float - and the two roundings can disagree with a single rounding to float. Parsing
straight to float rounds once, which is the answer the model actually names.

Being straight about the evidence: I could not make that difference observable. Both forms were
tried against the strings this path produces, including the classic double-rounding candidates
16777217 and 1.00000005960464477539062, and every result was bit-identical; the whole suite
passes either way. So the choice rests on the argument rather than on a failing test, and the PR
should not pretend otherwise.

The array element arm at Theorem.cs:471 carried the same defect and is corrected in the same
commit, on the issue's own reading. It cannot be verified: a float[] declares a floating-point
range against a real-valued constraint and dies during translation under #64, so reverting that
site alone fails nothing at all. Stated plainly rather than counted as covered - the same position
PR #73 took on the decimal element site.

What is deliberately not changed is the 32 in ToDecimalString(32). It reads as a nod to
float's 32 bits but is a count of decimal places, and it is too coarse for float's range - which is
why float.Epsilon comes back as 0.00000000000000000000000000000000? and fails to parse. That is
#6, not #54: the Double arm has exactly the same shape at 64 places against a range reaching
5e-324, and X1 * 3 == 1 over a double fails identically today. Fixing the type without
disturbing the precision keeps the two arms parallel and leaves #6 as one defect rather than half of
one.

Tests

166 -> 177. The #54 pin becomes a round-trip test, and the #52 culture test that could only
assert an ArgumentException now says what it always wanted to.

Test	What it covers
Solve_FloatSymbol_RoundTripsTheValue (6 rows)	exactly representable, zero, negative, not representable in binary, eight significant digits, Single.MaxValue
Solve_FloatAndDoubleSymbolsTogether_MarshalEachToItsOwnType	the two share the real sort and adjacent switch arms - a fix that made float work by treating it as a double passes every other test and fails this one
Solve_UnconstrainedFloatSymbol_ReturnsAResult	fills the one hole in the existing unconstrained-symbol family, which listed float as absent because of this defect
Solve_FloatConstantUnderANonInvariantCulture_RoundTripsTheValue	rewritten from _FailsInMarshallingNotTranslation
Solve_FloatSymbolWithANonTerminatingValue_ThrowsFormatException	#6 pin
Solve_DoubleSymbolWithANonTerminatingValue_ThrowsFormatException	#6 pin - the double form, so the defect is recorded as shared rather than looking like a float problem
Solve_FloatSymbolAtItsSmallestPositiveValue_ThrowsFormatException	#6 pin - 32 decimal places cannot express Single.Epsilon at all
Solve_FloatArraySymbol_ThrowsZ3Exception	#64 pin, and the record of why the array half of this fix is unverifiable

The three #6 pins are the first coverage that defect has had. It was found by measuring rather than
inferred: float.Epsilon and a third both fail before ever reaching the write this PR fixes.

Mutation results

Mutation	Failures	Which
Revert the scalar site to double.Parse	9	all six round-trip rows, the float/double pair, the unconstrained float, and the culture test
Revert the array site to double.Parse	0	unreachable behind #64, exactly as stated above
(float)double.Parse(...) - the alternative fix	0	the tests do not distinguish the two, and neither did any input I could construct
value = 0f	9	the five non-zero round-trip rows, the float/double pair, and - the interesting part - both #6 pins, which stop throwing. Confirms they assert a real parse attempt rather than incidental behaviour

Verification

• dotnet build solutions/Z3.Linq.slnx -c Release - clean, TreatWarningsAsErrors on
• 177/177 locally, 1.8s
• ./build.ps1 -Configuration Release - 46 tasks, 0 errors, 0 warnings
• Coverage 76.0% -> 76.7% line (641 of 835), 69.3% -> 69.6% branch. The float marshalling path
  previously ran into a dead end, so these are lines that had never completed before

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.

[Copilot]

Pull request overview

This PR fixes marshalling of solved float symbols so TypeCode.Single values are read back as float (not double), preventing reflection assignment failures when populating the solution object.

Changes:

• Updated TypeCode.Single result parsing in Theorem.ConvertZ3Expression (both scalar and array-element paths) from double.Parse(...) to float.Parse(...).
• Added/updated tests to validate float round-tripping (including alongside double), and adjusted culture-invariance coverage to assert correct float results now that marshalling succeeds.
• Added characterization tests to explicitly pin known defects (#6 non-terminating decimal expansions; #64 float-array translation failure) while documenting why some code paths remain unreachable.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.

File	Description
solutions/Z3.Linq/Theorem.cs	Fixes float model-value parsing to produce boxed float values for TypeCode.Single (scalar + array element loop).
solutions/Z3.Linq.Tests/SymbolTypeMarshallingTests.cs	Adds float round-trip coverage, float/double cohabitation coverage, and new pins for #6-related parse failures.
solutions/Z3.Linq.Tests/CultureInvarianceTests.cs	Updates the float culture test to round-trip assert (no longer only asserting an exception).
solutions/Z3.Linq.Tests/CollectionSymbolTests.cs	Adds a pinned test for float[] still failing under #64 and documents why the array-element fix is currently unobservable.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[github-actions]

Test Results

  1 files  ± 0    1 suites  ±0   6s ⏱️ +2s
170 tests + 8  170 ✅ + 8  0 💤 ±0  0 ❌ ±0 
177 runs  +11  177 ✅ +11  0 💤 ±0  0 ❌ ±0 

Results for commit 432653a. ± Comparison against base commit e468c5a.