sbv 10.4 → 10.5

raw patch · 12 files changed

+58/−41 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES.md +8/−1
• Data/SBV.hs +3/−3
• Data/SBV/Core/Floating.hs +1/−0
• Data/SBV/Internals.hs +4/−1
• Data/SBV/SMT/SMT.hs +2/−2
• Data/SBV/Utils/CrackNum.hs +34/−28
• 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
• sbv.cabal +1/−1

@@ -1,7 +1,14 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.io/sbv/> -* Latest Hackage released version: 10.4, 2024-02-15+* Latest Hackage released version: 10.5, 2024-02-20++### Version 10.5, 2024-02-20++  * Export svFloatingPointAsSWord through Data.SBV.Internals++  * crackNum: if verbose, alert the user if surface value of a NaN doesn't match its calculated value+    due to the redundancy in NaN representations.  ### Version 10.4, 2024-02-15 

@@ -502,9 +502,9 @@  -- | Show a value in detailed (cracked) form, if possible. -- This makes most sense with numbers, and especially floating-point types.-crack :: SBV a -> String-crack (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv Nothing = s-crack (SBV sv)                                                    = show sv+crack :: Bool -> SBV a -> String+crack verb (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv verb Nothing = s+crack _    (SBV sv)                                                         = show sv  -- Haddock section documentation {- $progIntro

@@ -28,6 +28,7 @@        , blastSFloat, blastSDouble,  blastSFloatingPoint        , sFloatAsComparableSWord32,  sDoubleAsComparableSWord64,  sFloatingPointAsComparableSWord        , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint+       , svFloatingPointAsSWord        ) where  import Data.Bits (testBit)

@@ -61,6 +61,9 @@   , sFloatAsComparableSWord32,  sDoubleAsComparableSWord64,  sFloatingPointAsComparableSWord   , sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint +  -- * Generalized floats+  , svFloatingPointAsSWord+   -- * lambdas and axioms   , lambda, lambdaStr, namedLambda, namedLambdaStr, constraint, constraintStr, Lambda(..), Constraint(..)   ) where@@ -74,7 +77,7 @@ import Data.SBV.Core.Model      (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod) import Data.SBV.Core.Symbolic   (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..)) -import Data.SBV.Core.Floating   ( sFloatAsComparableSWord32,  sDoubleAsComparableSWord64,  sFloatingPointAsComparableSWord)+import Data.SBV.Core.Floating   (sFloatAsComparableSWord32,  sDoubleAsComparableSWord64,  sFloatingPointAsComparableSWord, svFloatingPointAsSWord)  import qualified Data.SBV.Core.Floating as CF (sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint) 

@@ -634,7 +634,7 @@  -- | Show a constant value, in the user-specified base shCV :: SMTConfig -> String -> CV -> String-shCV SMTConfig{printBase, crackNum, crackNumSurfaceVals} nm cv = cracked (sh printBase cv)+shCV SMTConfig{printBase, crackNum, verbose, crackNumSurfaceVals} nm cv = cracked (sh printBase cv)   where sh 2  = binS         sh 10 = show         sh 16 = hexS@@ -642,7 +642,7 @@          cracked def           | not crackNum = def-          | True         = case CN.crackNum cv (nm `lookup` crackNumSurfaceVals) of+          | True         = case CN.crackNum cv verbose (nm `lookup` crackNumSurfaceVals) of                              Nothing -> def                              Just cs -> def ++ "\n" ++ cs 

@@ -35,31 +35,31 @@ -- | A class for cracking things deeper, if we know how. class CrackNum a where   -- | Convert an item to possibly bit-level description, if possible.-  crackNum :: a -> Maybe Integer -> Maybe String+  crackNum :: a -> Bool -> Maybe Integer -> Maybe String  -- | CVs are easy to crack instance CrackNum CV where-  crackNum cv mbIV = case kindOf cv of-                       -- Maybe one day we'll have a use for these, currently cracking them-                       -- any further seems overkill-                       KBool      {}  -> Nothing-                       KUnbounded {}  -> Nothing-                       KReal      {}  -> Nothing-                       KUserSort  {}  -> Nothing-                       KChar      {}  -> Nothing-                       KString    {}  -> Nothing-                       KList      {}  -> Nothing-                       KSet       {}  -> Nothing-                       KTuple     {}  -> Nothing-                       KMaybe     {}  -> Nothing-                       KEither    {}  -> Nothing-                       KRational  {}  -> Nothing+  crackNum cv verbose mbIV = case kindOf cv of+                               -- Maybe one day we'll have a use for these, currently cracking them+                               -- any further seems overkill+                               KBool      {}  -> Nothing+                               KUnbounded {}  -> Nothing+                               KReal      {}  -> Nothing+                               KUserSort  {}  -> Nothing+                               KChar      {}  -> Nothing+                               KString    {}  -> Nothing+                               KList      {}  -> Nothing+                               KSet       {}  -> Nothing+                               KTuple     {}  -> Nothing+                               KMaybe     {}  -> Nothing+                               KEither    {}  -> Nothing+                               KRational  {}  -> Nothing -                       -- Actual crackables-                       KFloat{}       -> Just $ let CFloat   f = cvVal cv in float mbIV f-                       KDouble{}      -> Just $ let CDouble  d = cvVal cv in float mbIV d-                       KFP{}          -> Just $ let CFP      f = cvVal cv in float mbIV f-                       KBounded sg sz -> Just $ let CInteger i = cvVal cv in int   sg sz i+                               -- Actual crackables+                               KFloat{}       -> Just $ let CFloat   f = cvVal cv in float verbose mbIV f+                               KDouble{}      -> Just $ let CDouble  d = cvVal cv in float verbose mbIV d+                               KFP{}          -> Just $ let CFP      f = cvVal cv in float verbose mbIV f+                               KBounded sg sz -> Just $ let CInteger i = cvVal cv in int   sg sz i  -- How far off the screen we want displayed? Somewhat experimentally found. tab :: String@@ -229,8 +229,8 @@  -- | Show a float in detail. mbSurface is the integer equivalent if this is a NaN; so we -- can represent it faithfully to the original given. Used by crackNum executable.-float :: HasFloatData a => Maybe Integer -> a -> String-float mbSurface f = intercalate "\n" $ ruler ++ legend : info+float :: HasFloatData a => Bool -> Maybe Integer -> a -> String+float verbose mbSurface f = intercalate "\n" $ ruler ++ legend : info    where fd@FloatData{prec, eb, sb, bits = bitsAsStored, fpKind, fpVals} = getFloatData f           nanKind = case fpKind of@@ -240,9 +240,9 @@                      Subnormal -> False                      Normal    -> False -         (nanClassifier, bits)-           | nanKind, Just i <- mbSurface = (extraClassifier i,  i)-           | True                         = ("", bitsAsStored)+         (nanClassifier, bits, nanChanged)+           | nanKind, Just i <- mbSurface = (extraClassifier i,  i,            i /= bitsAsStored)+           | True                         = ("",                 bitsAsStored, False)           -- Is this surface representation a signaling NaN or a quiet nan?          -- The test is that the tip bit of the significand is high: If so, quiet. If top bit is low, then signaling.@@ -262,6 +262,9 @@          allBits :: [Bool]          allBits = [bits `testBit` i | i <- reverse [0 .. eb + sb - 1]] +         storedBits :: [Bool]+         storedBits = [bitsAsStored `testBit` i | i <- reverse [0 .. eb + sb - 1]]+          flatHex = concatMap mkHex (split (split4 (eb + sb)) allBits)          sign    = bits `testBit` (eb+sb-1) @@ -269,12 +272,15 @@           esInfo = "Stored: " ++ show storedExponent ++ ", Bias: " ++ show bias +         chunks bs = unwords [concatMap (\b -> if b then "1" else "0") is | is <- split splits bs]+          isSubNormal = case fpKind of                          Subnormal -> True                          _         -> False -         info =   [ "   Binary layout: " ++ unwords [concatMap (\b -> if b then "1" else "0") is | is <- split splits allBits]-                  , "      Hex layout: " ++ unwords (split (split4 (length flatHex)) flatHex)+         info =   [ "   Binary layout: " ++ chunks allBits]+               ++ [ " Calculated bits: " ++ chunks storedBits ++ " (Surface NaN value differs from calculated)" | verbose && nanChanged]+               ++ [ "      Hex layout: " ++ unwords (split (split4 (length flatHex)) flatHex)                   , "       Precision: " ++ prec                   , "            Sign: " ++ if sign then "Negative" else "Positive"                   ]

@@ -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.4-inplace:Data.SBV.Control.Utils+  error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.5-inplace:Data.SBV.Control.Utils

@@ -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.4-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.5-inplace:Data.SBV.Core.Symbolic

@@ -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.4-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.5-inplace:Data.SBV.Core.Symbolic

@@ -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.4-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.5-inplace:Data.SBV.Core.Symbolic

@@ -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.4-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.5-inplace:Data.SBV.Core.Symbolic

@@ -1,7 +1,7 @@ Cabal-Version: 2.2  Name        : sbv-Version     : 10.4+Version     : 10.5 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