diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,11 @@ * Hackage: * GitHub: +### Version 10.8, 2024-04-05 + + * Increase the number of digits used in printing floats in decimal base, which leads to + better output in most cases. + ### Version 10.7, 2024-03-23 * Fix SMTDefinable instances for functions of arity 8-12. Thanks to Nick Lewchenko for the patch. diff --git a/Data/SBV/Core/SizedFloats.hs b/Data/SBV/Core/SizedFloats.hs --- a/Data/SBV/Core/SizedFloats.hs +++ b/Data/SBV/Core/SizedFloats.hs @@ -33,7 +33,7 @@ , fprCompareObject, fprToSMTLib2, mkBFOpts, bfToString, bfRemoveRedundantExp ) where -import Data.Char (intToDigit) +import Data.Char (intToDigit, toUpper) import Data.List (isSuffixOf) import Data.Proxy import GHC.TypeLits @@ -112,14 +112,22 @@ | BF.bfIsNaN a = "NaN" | BF.bfIsInf a = if BF.bfIsPos a then "Infinity" else "-Infinity" | BF.bfIsZero a = if BF.bfIsPos a then "0.0" else "-0.0" - | True = trimZeros $ BF.bfToString b opts' a - where opts = BF.showRnd BF.NearEven <> BF.showFree (Just (fromIntegral sb)) - opts' = case (withPrefix, forceExponent) of - (False, False) -> opts - (False, True ) -> BF.forceExp <> opts - (True, False) -> BF.addPrefix <> opts - (True, True ) -> BF.addPrefix <> BF.forceExp <> opts + | True + = cap $ trimZeros $ BF.bfToString b opts' a + where opts = BF.showRnd BF.NearEven <> BF.showFree (Just (fromIntegral prec)) + -- For base 10, use a larger precision. It's really difficult to "pick" + -- the correct value here; but 2*sb seems to work ok. Note that even picking + -- sb is fine: The output isn't incorrect. It's just confusing. + prec | b == 10 = 2*sb + | True = sb + + opts' + | withPrefix && forceExponent = BF.addPrefix <> BF.forceExp <> opts + | withPrefix = BF.addPrefix <> opts + | forceExponent = BF.forceExp <> opts + | True = opts + -- In base 10, exponent starts with 'e'. Otherwise (2, 8, 16) it starts with 'p' expChar = if b == 10 then 'e' else 'p' @@ -131,6 +139,18 @@ in pre' ++ post | True = s + cap xs + | withPrefix = take 2 xs ++ capitalize (drop 2 xs) + | True = capitalize xs + + -- capitalize till we see the expChar + capitalize "" = "" + capitalize (x:xs) + | ux == ue = x:xs + | True = ux : capitalize xs + where ux = toUpper x + ue = toUpper expChar + -- | Default options for BF options. mkBFOpts :: Integral a => a -> a -> RoundMode -> BFOpts mkBFOpts eb sb rm = BF.allowSubnormal <> BF.rnd rm <> BF.expBits (fromIntegral eb) <> BF.precBits (fromIntegral sb) @@ -288,10 +308,9 @@ -- | Real-frac instance for big-floats. Beware, not that well tested! instance RealFrac FP where - properFraction (FP eb sb r) = case BF.bfRoundInt BF.ToNegInf r of - (r', BF.Ok) | BF.bfSign r == BF.bfSign r' -> (getInt r', FP eb sb r - FP eb sb r') - x -> error $ "RealFrac.FP.properFraction: Failed to convert: " ++ show (r, x) - where getInt x = case BF.bfToRep x of + properFraction (FP eb sb r) = (getInt r', FP eb sb r - FP eb sb r') + where (r', _) = BF.bfRoundInt BF.ToNegInf r + getInt x = case BF.bfToRep x of BF.BFNaN -> error $ "Data.SBV.FloatingPoint.properFraction: Failed to convert: " ++ show (r, x) BF.BFRep s n -> case n of BF.Zero -> 0 diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs --- a/Documentation/SBV/Examples/Misc/Floating.hs +++ b/Documentation/SBV/Examples/Misc/Floating.hs @@ -163,10 +163,12 @@ -- Unfortunately Haskell floats do not allow computation with arbitrary rounding modes, but SBV's -- 'SFloatingPoint' type does. We have: -- --- >>> fpAdd sRoundTowardZero 1.7499695 1.2539366 :: SFPSingle --- 3.00390601 :: SFloatingPoint 8 24 --- >>> fpAdd sRoundNearestTiesToEven 1.7499695 1.2539366 :: SFPSingle --- 3.00390625 :: SFloatingPoint 8 24 +-- >>> sat $ \x -> x .== (fpAdd sRoundTowardZero 1.7499695 1.2539366 :: SFloat) +-- Satisfiable. Model: +-- s0 = 3.003906 :: Float +-- >>> sat $ \x -> x .== (fpAdd sRoundNearestTiesToEven 1.7499695 1.2539366 :: SFloat) +-- Satisfiable. Model: +-- s0 = 3.0039063 :: Float -- -- We can see why these two results are indeed different: The 'RoundTowardZero' -- (which rounds towards the origin) produces a smaller result, closer to 0. Indeed, if we treat these numbers @@ -198,24 +200,23 @@ -- -- >>> fp54Bounds -- Objective "max": Optimal model: --- x = 61400 :: FloatingPoint 5 4 +-- x = 61440 :: FloatingPoint 5 4 -- max = 503 :: WordN 9 -- min = 503 :: WordN 9 -- Objective "min": Optimal model: --- x = 0.00000763 :: FloatingPoint 5 4 --- max = 257 :: WordN 9 --- min = 257 :: WordN 9 +-- x = 0.000007629 :: FloatingPoint 5 4 +-- max = 257 :: WordN 9 +-- min = 257 :: WordN 9 -- --- The careful reader will notice that the numbers @61400@ and @0.00000763@ are quite suspicious, but the metric --- space equivalents are correct. The reason for this is due to the sparcity of floats. The "computed" value of --- the maximum in this bound is actually @61440@, however in @FloatingPoint 5 4@ representation all numbers --- between @57344@ and @61440@ collapse to the same bit-pattern, and the pretty-printer picks a string --- representation in decimal that falls within range that it considers is the "simplest." (Printing --- floats precisely is a thorny subject!) Likewise, the minimum value we're looking for is actually --- 2^-17, but any number between 2^-16 and 2^-17 will map to this number. It turns out that 0.00000763 --- in decimal is one such value. Moral of the story is that when reading floating-point numbers in +-- An important note is in order. When printing floats in decimal, one can get correct yet surprising results. +-- There's a large body of publications in how to render floats in decimal, or in bases that are not powers of +-- two in general. So, when looking at such values in decimal, keep in mind that what you see might be +-- a representative value: That is, it preserves the value when translated back to the format. For instance, +-- the more precise answer for the min value would be 2^-17, which is 0.00000762939453125. But we see +-- it truncated here. In fact, any number between 2^-16 and 2^-17 would be correct as they all map to the same +-- underlying representation in this format. Moral of the story is that when reading floating-point numbers in -- decimal notation one should be very careful about the printed representation and the numeric value; while --- they will match in vsalue (if there are no bugs!), they can print quite differently! (Also keep in +-- they will match in value (if there are no bugs!), they can print quite differently! (Also keep in -- mind the rounding modes that impact how the conversion is done.) fp54Bounds :: IO OptimizeResult fp54Bounds = optimize Independent $ do x :: SFloatingPoint 5 4 <- sFloatingPoint "x" diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -61,4 +61,4 @@ *** NB. If this is a use case you'd like SBV to support, please get in touch! CallStack (from HasCallStack): - error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.7-inplace:Data.SBV.Control.Utils + error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.8-inplace:Data.SBV.Control.Utils diff --git a/SBVTestSuite/GoldFiles/arbFp_opt_1.gold b/SBVTestSuite/GoldFiles/arbFp_opt_1.gold --- a/SBVTestSuite/GoldFiles/arbFp_opt_1.gold +++ b/SBVTestSuite/GoldFiles/arbFp_opt_1.gold @@ -1,3 +1,3 @@ Optimal model: - s0 = 65504 :: FloatingPoint 5 11 - x = 64511 :: Word16 + s0 = 65504.0 :: FloatingPoint 5 11 + x = 64511 :: Word16 diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -37,4 +37,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack): - error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic + error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.8-inplace:Data.SBV.Core.Symbolic diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -77,7 +77,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version) -[RECV] (:version "4.13.0") +[RECV] (:version "4.13.1") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -108,7 +108,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.13.0") +[RECV] (:version "4.13.1") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 10.7 +Version : 10.8 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT