sbv 10.8 → 10.9
raw patch · 14 files changed
+23/−32 lines, 14 files
Files
- CHANGES.md +4/−0
- Data/SBV/Core/SizedFloats.hs +2/−14
- Data/SBV/Utils/PrettyNum.hs +4/−5
- SBVTestSuite/GoldFiles/allSat8.gold +1/−1
- 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/optFloat1a.gold +1/−1
- SBVTestSuite/GoldFiles/optFloat1c.gold +1/−1
- SBVTestSuite/GoldFiles/optFloat2a.gold +1/−1
- SBVTestSuite/GoldFiles/optFloat2c.gold +1/−1
- SBVTestSuite/GoldFiles/optFloat3.gold +3/−3
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,6 +1,10 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 10.9, 2024-04-05++ * Fix printing of floats to be more consistent, using lowercase letters+ ### Version 10.8, 2024-04-05 * Increase the number of digits used in printing floats in decimal base, which leads to
Data/SBV/Core/SizedFloats.hs view
@@ -33,7 +33,7 @@ , fprCompareObject, fprToSMTLib2, mkBFOpts, bfToString, bfRemoveRedundantExp ) where -import Data.Char (intToDigit, toUpper)+import Data.Char (intToDigit) import Data.List (isSuffixOf) import Data.Proxy import GHC.TypeLits@@ -113,7 +113,7 @@ | 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- = cap $ trimZeros $ BF.bfToString b opts' a+ = 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"@@ -138,18 +138,6 @@ res -> res 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
Data/SBV/Utils/PrettyNum.hs view
@@ -22,7 +22,7 @@ ) where import Data.Bits ((.&.), countTrailingZeros)-import Data.Char (intToDigit, ord, chr, toUpper)+import Data.Char (intToDigit, ord, chr) import Data.Int (Int8, Int16, Int32, Int64) import Data.List (isPrefixOf) import Data.Maybe (fromJust, fromMaybe, listToMaybe)@@ -552,10 +552,9 @@ | all (== 0) digits = "" | True = "." ++ concatMap toDigit digits - toDigit v = map toUpper d- where d | v <= 15 = [intToDigit v]- | v < 36 = [chr (ord 'a' + v - 10)]- | True = '<' : show v ++ ">"+ toDigit v | v <= 15 = [intToDigit v]+ | v < 36 = [chr (ord 'a' + v - 10)]+ | True = '<' : show v ++ ">" -- | When we show a negative number in SMTLib, we must properly parenthesize. showNegativeNumber :: (Show a, Num a, Ord a) => a -> String
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.8-inplace:Data.SBV.Control.Utils+ error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.9-inplace:Data.SBV.Control.Utils
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.8-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-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.8-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-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.8-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-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.8-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.9-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/optFloat1a.gold view
@@ -12,7 +12,7 @@ Binary: -0b1.11111111111111111111111p+127 Octal: -0o3.77777774p+126 Decimal: -3.4028235e38- Hex: -0xF.FFFFFp+124+ Hex: -0xf.fffffp+124 min-x = 8388608 :: Word32 3 2 1 0 1098 7654 3210 9876 5432 1098 7654 3210
SBVTestSuite/GoldFiles/optFloat1c.gold view
@@ -12,7 +12,7 @@ Binary: 0b1.11111111111111111111111p+127 Octal: 0o3.77777774p+126 Decimal: 3.4028235e38- Hex: 0xF.FFFFFp+124+ Hex: 0xf.fffffp+124 max-x = 4286578687 :: Word32 3 2 1 0 1098 7654 3210 9876 5432 1098 7654 3210
SBVTestSuite/GoldFiles/optFloat2a.gold view
@@ -12,7 +12,7 @@ Binary: -0b1.1111111111111111111111111111111111111111111111111111p+1023 Octal: -0o1.777777777777777774p+1023 Decimal: -1.7976931348623157e308- Hex: -0xF.FFFFFFFFFFFF8p+1020+ Hex: -0xf.ffffffffffff8p+1020 min-x = 4503599627370496 :: Word64 6 5 4 3 2 1 0 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210
SBVTestSuite/GoldFiles/optFloat2c.gold view
@@ -12,7 +12,7 @@ Binary: 0b1.1111111111111111111111111111111111111111111111111111p+1023 Octal: 0o1.777777777777777774p+1023 Decimal: 1.7976931348623157e308- Hex: 0xF.FFFFFFFFFFFF8p+1020+ Hex: 0xf.ffffffffffff8p+1020 max-x = 18442240474082181119 :: Word64 6 5 4 3 2 1 0 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210 9876 5432 1098 7654 3210
SBVTestSuite/GoldFiles/optFloat3.gold view
@@ -12,7 +12,7 @@ Binary: 0b1.11111111111111111111111p+127 Octal: 0o3.77777774p+126 Decimal: 3.4028235e38- Hex: 0xF.FFFFFp+124+ Hex: 0xf.fffffp+124 x = 1.7014117e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210@@ -26,7 +26,7 @@ Binary: 0b1.11111111111111111111111p+126 Octal: 0o1.77777776p+126 Decimal: 1.7014117e38- Hex: 0x7.FFFFF8p+124+ Hex: 0x7.fffff8p+124 y = 1.7014117e38 :: Float 3 2 1 0 1 09876543 21098765432109876543210@@ -40,7 +40,7 @@ Binary: 0b1.11111111111111111111111p+126 Octal: 0o1.77777776p+126 Decimal: 1.7014117e38- Hex: 0x7.FFFFF8p+124+ Hex: 0x7.fffff8p+124 metric-max-x+y = 4286578687 :: Word32 3 2 1 0 1098 7654 3210 9876 5432 1098 7654 3210
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 10.8+Version : 10.9 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