sbv 5.1 → 5.2
raw patch · 4 files changed
+16/−11 lines, 4 files
Files
- CHANGES.md +6/−1
- Data/SBV/BitVectors/PrettyNum.hs +8/−8
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,7 +1,12 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.1, 2015-10-10+* Latest Hackage released version: 5.2, 2015-10-12++### Version 5.2, 2015-10-12++ * Regression on 5.1: Fix a minor bug in base 2/16 printing where uninterpreted constants were+ not handled correctly. ### Version 5.1, 2015-10-10
Data/SBV/BitVectors/PrettyNum.hs view
@@ -67,36 +67,36 @@ {hexS = shexI True True; binS = sbinI True True; hex = shexI False False; bin = sbinI False False;} instance PrettyNum CW where- hexS cw | cwIsBit cw = hexS (cwToBool cw)+ hexS cw | isUninterpreted cw = show cw ++ " :: " ++ show (cwKind cw)+ | cwIsBit cw = hexS (cwToBool cw) | isFloat cw = let CWFloat f = cwVal cw in show f ++ " :: Float\n" ++ show (floatToFP f) | isDouble cw = let CWDouble d = cwVal cw in show d ++ " :: Double\n" ++ show (doubleToFP d) | isReal cw = let CWAlgReal w = cwVal cw in show w ++ " :: Real" | not (isBounded cw) = let CWInteger w = cwVal cw in shexI True True w- | isUninterpreted cw = show cw ++ " :: " ++ show (cwKind cw) | True = let CWInteger w = cwVal cw in shex True True (hasSign cw, intSizeOf cw) w - binS cw | cwIsBit cw = binS (cwToBool cw)+ binS cw | isUninterpreted cw = show cw ++ " :: " ++ show (cwKind cw)+ | cwIsBit cw = binS (cwToBool cw) | isFloat cw = let CWFloat f = cwVal cw in show f ++ " :: Float\n" ++ show (floatToFP f) | isDouble cw = let CWDouble d = cwVal cw in show d ++ " :: Double\n" ++ show (doubleToFP d) | isReal cw = let CWAlgReal w = cwVal cw in show w ++ " :: Real" | not (isBounded cw) = let CWInteger w = cwVal cw in sbinI True True w- | isUninterpreted cw = show cw ++ " :: " ++ show (cwKind cw) | True = let CWInteger w = cwVal cw in sbin True True (hasSign cw, intSizeOf cw) w - hex cw | cwIsBit cw = hexS (cwToBool cw)+ hex cw | isUninterpreted cw = show cw+ | cwIsBit cw = hexS (cwToBool cw) | isFloat cw = let CWFloat f = cwVal cw in show f | isDouble cw = let CWDouble d = cwVal cw in show d | isReal cw = let CWAlgReal w = cwVal cw in show w | not (isBounded cw) = let CWInteger w = cwVal cw in shexI False False w- | isUninterpreted cw = show cw | True = let CWInteger w = cwVal cw in shex False False (hasSign cw, intSizeOf cw) w - bin cw | cwIsBit cw = binS (cwToBool cw)+ bin cw | isUninterpreted cw = show cw+ | cwIsBit cw = binS (cwToBool cw) | isFloat cw = let CWFloat f = cwVal cw in show f | isDouble cw = let CWDouble d = cwVal cw in show d | isReal cw = let CWAlgReal w = cwVal cw in show w | not (isBounded cw) = let CWInteger w = cwVal cw in sbinI False False w- | isUninterpreted cw = show cw | True = let CWInteger w = cwVal cw in sbin False False (hasSign cw, intSizeOf cw) w instance (SymWord a, PrettyNum a) => PrettyNum (SBV a) where
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Sat Oct 10 21:03:50 PDT 2015"+buildTime = "Sun Oct 11 23:08:47 PDT 2015"
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 5.1+Version: 5.2 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