Fix RealVal for floats requiring scientific notation

[daniel-larraz]

Alternative to #114, which addresses the same bug.

The bug

RealVal passes str(val) to mkReal. For small and large magnitudes str switches to scientific notation, which mkReal rejects:

>>> RealVal(1e-5)
RuntimeError: cannot construct Real or Int from string argument '1e-05'

This fix

if isinstance(val, float):
    return RatNumRef(ctx.tm.mkReal(format(Decimal(repr(val)), "f")), ctx)

repr gives the shortest decimal string that round-trips to the float, and formatting the resulting Decimal with "f" expands it without an exponent. The result is exactly the value Python itself would print, for every finite float — no rounding, no magnitude cutoff.

Why not #114

#114 fixes the crash, but its mechanism has two problems.

1. f"{val:.10f}" silently rounds every float to 10 fractional digits. This loses precision for values that worked correctly before the patch:

input	#114	this PR
RealVal(1.5e-10)	1/10000000000 (33% error)	3/20000000000
RealVal(2.5e-10)	1/2500000000 (20% error)	1/4000000000
RealVal(1/3)	3333333333/10000000000	3333333333333333/10000000000000000

Since RealVal backs _py2expr and ArithSortRef.cast, this also affects ordinary expressions like x + 1/3, not just direct RealVal calls.

2. The 1e-10 threshold gives floats two incompatible semantics. Below the threshold #114 uses as_integer_ratio(), i.e. the exact binary value; above it, a rounded decimal. So which meaning a user gets depends on magnitude:

RealVal(1e-9)  * 10**9  == 1   # True  (decimal branch)
RealVal(1e-11) * 10**11 == 1   # False (binary branch: 1e-11 is not exactly 1/10**11)
RealVal(1e-11).eq(RatVal(1, 10**11))  # False

Using the round-tripping decimal everywhere keeps a single semantics — RealVal(f) is the rational denoted by repr(f) — and both identities above hold.

as_integer_ratio() alone would also be defensible, but it makes RealVal(0.1) be 3602879701896397/36028797018963968 rather than 1/10, which is surprising and changes existing printed forms.

Notes

• Adds doctests for RealVal(1.5), RealVal(1e-5), and the 1e-11 exactness identity.
• RealVal(float('nan')) / RealVal(float('inf')) still raise RuntimeError from mkReal, as before.
• Rebased on main after Update the multiple_solvers test output #116; the full suite passes and black --check is clean.

[alex-ozdemir]

Yes, this approach is right, thanks @daniel-larraz .