sbv 5.7 → 5.8
raw patch · 8 files changed
+46/−13 lines, 8 files
Files
- CHANGES.md +8/−1
- COPYRIGHT +1/−1
- Data/SBV/BitVectors/Model.hs +2/−2
- Data/SBV/BitVectors/Operations.hs +29/−5
- Data/SBV/Dynamic.hs +3/−1
- LICENSE +1/−1
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,7 +1,14 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.7, 2015-12-21+* Latest Hackage released version: 5.8, 2016-01-01++### Version 5.8, 2016-01-01++ * Fix some typos+ * Add 'svEnumFromThenTo' to the Dynamic interface, allowing dynamic construction+ of [x, y .. z] and [x .. y] when the involved values are concrete.+ * Add 'svExp' to the Dynamic interface, implementing exponentation ### Version 5.7, 2015-12-21
COPYRIGHT view
@@ -1,4 +1,4 @@-Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2016, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbv library is distributed with the BSD3 license. See the LICENSE file
Data/SBV/BitVectors/Model.hs view
@@ -695,7 +695,7 @@ sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sShiftLeft x i | not (isBounded x)- = error "SBV.sShiftRight: Shifted about should be a bounded quantity!"+ = error "SBV.sShiftRight: Shifted amount should be a bounded quantity!" | True = ite (i .< 0) (select [x `shiftR` k | k <- [0 .. ghcBitSize x - 1]] z (-i))@@ -712,7 +712,7 @@ sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a sShiftRight x i | not (isBounded x)- = error "SBV.sShiftRight: Shifted about should be a bounded quantity!"+ = error "SBV.sShiftRight: Shifted amount should be a bounded quantity!" | True = ite (i .< 0) (select [x `shiftL` k | k <- [0 .. ghcBitSize x - 1]] z (-i))
Data/SBV/BitVectors/Operations.hs view
@@ -13,7 +13,7 @@ ( -- ** Basic constructors svTrue, svFalse, svBool- , svInteger, svFloat, svDouble, svReal+ , svInteger, svFloat, svDouble, svReal, svEnumFromThenTo -- ** Basic destructors , svAsBool, svAsInteger, svNumerator, svDenominator -- ** Basic operations@@ -28,6 +28,7 @@ , svIte, svLazyIte, svSymbolicMerge , svSelect , svSign, svUnsign+ , svExp -- ** Derived operations , svToWord1, svFromWord1, svTestBit , svShiftLeft, svShiftRight@@ -76,7 +77,6 @@ svReal :: Rational -> SVal svReal d = SVal KReal (Left (CW KReal (CWAlgReal (fromRational d)))) - -------------------------------------------------------------------------------- -- Basic destructors @@ -100,7 +100,20 @@ svDenominator (SVal KReal (Left (CW KReal (CWAlgReal (AlgRational True r))))) = Just $ denominator r svDenominator _ = Nothing ---------------------------------------------------------------------------------+-------------------------------------------------------------------------------------+-- | Constructing [x, y, .. z] and [x .. y]. Only works when all arguments are concrete and integral and the result is guaranteed finite+-- Note that the it isn't "obviously" clear why the following works; after all we're doing the construction over Integer's and mapping+-- it back to other types such as SIntN/SWordN. The reason is that the values we receive are guaranteed to be in their domains; and thus+-- the lifting to Integers preserves the bounds; and then going back is just fine. So, things like @[1, 5 .. 200] :: [SInt8]@ work just+-- fine (end evaluate to empty list), since we see @[1, 5 .. -56]@ in the @Integer@ domain. Also note the explicit check for @s /= f@+-- below to make sure we don't stutter and produce an infinite list.+svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]+svEnumFromThenTo bf mbs bt+ | Just bs <- mbs, Just f <- svAsInteger bf, Just s <- svAsInteger bs, Just t <- svAsInteger bt, s /= f = Just $ map (svInteger (kindOf bf)) [f, s .. t]+ | Nothing <- mbs, Just f <- svAsInteger bf, Just t <- svAsInteger bt = Just $ map (svInteger (kindOf bf)) [f .. t]+ | True = Nothing++------------------------------------------------------------------------------------- -- Basic operations -- | Addition.@@ -139,6 +152,16 @@ where -- should never happen die = error "impossible: integer valued data found in Fractional instance" +-- | Exponentiation.+svExp :: SVal -> SVal -> SVal+svExp b e | hasSign (kindOf e) = error "svExp: exponentiation only works with unsigned exponents"+ | True = prod $ zipWith (\use n -> svIte use n one)+ (blastLE e)+ (iterate (\x -> svTimes x x) b)+ where blastLE x = map (svTestBit x) [0 .. intSizeOf x - 1]+ prod = foldr svTimes one+ one = svInteger (kindOf b) 1+ -- | Quotient: Overloaded operation whose meaning depends on the kind at which -- it is used: For unbounded integers, it corresponds to the SMT-Lib -- "div" operator ("Euclidean" division, which always has a@@ -534,7 +557,7 @@ svShiftLeft :: SVal -> SVal -> SVal svShiftLeft x i | not (isBounded x)- = error "SBV.svShiftLeft: Shifted about should be a bounded quantity!"+ = error "SBV.svShiftLeft: Shifted amount should be a bounded quantity!" | True = svIte (svLessThan i zi) (svSelect [svShr x k | k <- [0 .. intSizeOf x - 1]] z (svUNeg i))@@ -550,7 +573,7 @@ svShiftRight :: SVal -> SVal -> SVal svShiftRight x i | not (isBounded x)- = error "SBV.svShiftLeft: Shifted about should be a bounded quantity!"+ = error "SBV.svShiftLeft: Shifted amount should be a bounded quantity!" | True = svIte (svLessThan i zi) (svSelect [svShl x k | k <- [0 .. intSizeOf x - 1]] z (svUNeg i))@@ -700,6 +723,7 @@ _ -> True -- | Quot/Rem operations require a nonzero check on the divisor.+-- nonzeroCheck :: CW -> CW -> Bool nonzeroCheck _ b = cwVal b /= CWInteger 0
Data/SBV/Dynamic.hs view
@@ -38,11 +38,13 @@ , svReal, svNumerator, svDenominator -- *** Symbolic equality , svEqual, svNotEqual+ -- *** Constructing concrete lists+ , svEnumFromThenTo -- *** Symbolic ordering , svLessThan, svGreaterThan, svLessEq, svGreaterEq -- *** Arithmetic operations , svPlus, svTimes, svMinus, svUNeg, svAbs- , svDivide, svQuot, svRem+ , svDivide, svQuot, svRem, svExp -- *** Logical operations , svAnd, svOr, svXOr, svNot , svShl, svShr, svRol, svRor
LICENSE view
@@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2015, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2016, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Mon Dec 21 15:35:40 PST 2015"+buildTime = "Fri Jan 1 12:25:00 PST 2016"
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 5.7+Version: 5.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