diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,14 @@ * Hackage: * GitHub: -* 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 diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -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 diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -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)) diff --git a/Data/SBV/BitVectors/Operations.hs b/Data/SBV/BitVectors/Operations.hs --- a/Data/SBV/BitVectors/Operations.hs +++ b/Data/SBV/BitVectors/Operations.hs @@ -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 diff --git a/Data/SBV/Dynamic.hs b/Data/SBV/Dynamic.hs --- a/Data/SBV/Dynamic.hs +++ b/Data/SBV/Dynamic.hs @@ -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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -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" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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