sbv 10.7 → 10.8
raw patch · 11 files changed
+64/−39 lines, 11 files
Files
- CHANGES.md +5/−0
- Data/SBV/Core/SizedFloats.hs +31/−12
- Documentation/SBV/Examples/Misc/Floating.hs +18/−17
- SBVTestSuite/GoldFiles/allSat8.gold +1/−1
- SBVTestSuite/GoldFiles/arbFp_opt_1.gold +2/−2
- SBVTestSuite/GoldFiles/nested1.gold +1/−1
- SBVTestSuite/GoldFiles/nested2.gold +1/−1
- SBVTestSuite/GoldFiles/nested3.gold +1/−1
- SBVTestSuite/GoldFiles/nested4.gold +1/−1
- SBVTestSuite/GoldFiles/query1.gold +2/−2
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,6 +1,11 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### 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.
Data/SBV/Core/SizedFloats.hs view
@@ -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
Documentation/SBV/Examples/Misc/Floating.hs view
@@ -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"
SBVTestSuite/GoldFiles/allSat8.gold view
@@ -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
SBVTestSuite/GoldFiles/arbFp_opt_1.gold view
@@ -1,3 +1,3 @@ Optimal model:- s0 = 65504 :: FloatingPoint 5 11- x = 64511 :: Word16+ s0 = 65504.0 :: FloatingPoint 5 11+ x = 64511 :: Word16
SBVTestSuite/GoldFiles/nested1.gold view
@@ -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
SBVTestSuite/GoldFiles/nested2.gold view
@@ -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
SBVTestSuite/GoldFiles/nested3.gold view
@@ -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
SBVTestSuite/GoldFiles/nested4.gold view
@@ -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
SBVTestSuite/GoldFiles/query1.gold view
@@ -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)
sbv.cabal view
@@ -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