Printing floating points

[Bruce Carneal]

On Thursday, 28 January 2021 at 08:30:40 UTC, Ola Fosheim Grøstad 
wrote:
> On Thursday, 28 January 2021 at 02:25:57 UTC, Bruce Carneal 
> wrote:
>> Regardless, you clearly do not understand what I'm asking in 
>> question 1) and I do not think it likely that additional 
>> interaction on this topic will be useful to either of us.
>
> Asking for a mapping does not really make much sense without 
> specifying the domain/codomain, but my answer actually holds 
> even then.

For the problem under discussion the domain is 0 .. 2**NBits 
(binary FP) and the codomain is the problem specified string 
output of the function.  This has not changed and I had thought 
it was clear to all concerned throughout.

The correctness check for the mapping in this case is trivial, by 
which I mean: obvious, readily understood, not needing further 
explanation, ... a *good* thing in this context.

>
> Anyway, if you _actually_ are interested in this topic then you 
> could start by looking at automatic test case generation using 
> SMT solvers.

I am actually interested in proving correctness by establishing 
full coverage of the domain with something less expensive than 
direct enumeration, less expensive than a for loop across all 
possibilities (an SMT-like solution).  This is what I thought 
that you said you had accomplished with a trivial coverage, your 
"no problem" remark.  IOW, I thought you claimed to have solved 
the problem.

I found such a claim remarkable, I did not see it, so I sought 
clarification.  IIUC now, I was mistaken then.  You have no 
particular insight to offer toward the solution of the above 
problem and, by your lights, never made such a claim.

Apparently I took your well meaning remarks much too seriously.