CrackNum decimal printing

[LeventErkok]

Consider:

$ crackNum -f3+4 0b0000011
Satisfiable. Model:
  DECODED = 0.0938 :: FloatingPoint 3 4
                  6 543 210
                  S E3- S3-
   Binary layout: 0 000 011
      Hex layout: 03
       Precision: 3 exponent bits, 3 significand bits
            Sign: Positive
        Exponent: -2 (Subnormal, with fixed exponent value. Stored: 0, Bias: 3)
  Classification: FP_SUBNORMAL
          Binary: 0b1.1p-4
           Octal: 0o6p-6
         Decimal: 0.0938
             Hex: 0x1.8p-4

This is correct; but extremely confusing! Why, because the decimal value as printed is an "equal" value that maps to this representation. But at first look, one would like to see 0.09375.

Note that 0.0938 isn't incorrect; because it maps to that very same value representationally. And it's probably picked by the underlying FPLib library because it's "shorter."

But this is clearly confusing. I wonder if we can represent the info in a better way to avoid such pitfalls.

[LeventErkok]

Another confusing output:

[merzifon]~>crackNum -f3+4 0.9375
Satisfiable. Model:
  ENCODED = 0.938 :: FloatingPoint 3 4
                  6 543 210
                  S E3- S3-
   Binary layout: 0 010 111
      Hex layout: 17
       Precision: 3 exponent bits, 3 significand bits
            Sign: Positive
        Exponent: -1 (Stored: 2, Bias: 3)
  Classification: FP_NORMAL
          Binary: 0b1.111p-1
           Octal: 0o7.4p-3
         Decimal: 0.938
             Hex: 0xfp-4
   Rounding mode: RNE: Round nearest ties to even.
            Note: Conversion from "0.9375" was exact. No rounding happened.

Note that the "note" says the conversion was exact, but we see 0.938 printed, not 0.9375. Again, this isn't incorrect. It's just terribly confusing.

[LeventErkok]

Looking at the code, what we do is simply call show for haskell types and bfToString 10 True False for LibBF values.

Instead, we should call showFFloat with a user given precision value. (Not sure if there's an equivalent of that in bfToString.) This way we can control the output and make this much less confusing.

This is something we should do, but need a bit more digging to figure out exactly how to approach. For instance, it would be nice to add ... at the end if the remaining digits aren't 0. Doable? Perhaps?

[LeventErkok]

Triggering from sbv directly:

*Data.SBV> satWith z3{crackNum=True} $ \x -> x .== (0.9375  :: SFloatingPoint 3 4)
Satisfiable. Model:
  s0 = 0.938 :: FloatingPoint 3 4
                  6 543 210
                  S E3- S3-
   Binary layout: 0 010 111
      Hex layout: 17
       Precision: 3 exponent bits, 3 significand bits
            Sign: Positive
        Exponent: -1 (Stored: 2, Bias: 3)
  Classification: FP_NORMAL
          Binary: 0b1.111p-1
           Octal: 0o7.4p-3
         Decimal: 0.938
             Hex: 0xfp-4