sbv 2.7 → 2.8
raw patch · 8 files changed
+93/−38 lines, 8 files
Files
- Data/SBV.hs +3/−3
- Data/SBV/BitVectors/Data.hs +1/−1
- Data/SBV/BitVectors/Model.hs +60/−29
- Data/SBV/BitVectors/Splittable.hs +1/−1
- Data/SBV/Tools/Polynomial.hs +1/−1
- RELEASENOTES +25/−1
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- sbv.cabal +1/−1
Data/SBV.hs view
@@ -113,7 +113,7 @@ , STree, readSTree, writeSTree, mkSTree -- ** Operations on symbolic words -- *** Word level- , sbvTestBit, sbvPopCount, setBitTo, oneIf, lsb, msb+ , sbvTestBit, sbvPopCount, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight, setBitTo, oneIf, lsb, msb -- *** List level , allEqual, allDifferent -- *** Blasting/Unblasting@@ -130,8 +130,8 @@ , EqSymbolic(..) -- ** Symbolic ordering , OrdSymbolic(..)- -- ** Symbolic numbers- , SNum+ -- ** Symbolic integral numbers+ , SIntegral -- ** Division , SDivisible(..) -- ** The Boolean class
Data/SBV/BitVectors/Data.hs view
@@ -863,7 +863,7 @@ -- | One stop allocator mkSymWord :: Maybe Quantifier -> Maybe String -> Symbolic (SBV a) - -- minimal complete definiton, Nothing.+ -- minimal complete definition, Nothing. -- Giving no instances is ok when defining an uninterpreted sort, but otherwise you really -- want to define: mbMaxBound, mbMinBound, literal, fromCW, mkSymWord forall = mkSymWord (Just ALL) . Just
Data/SBV/BitVectors/Model.hs view
@@ -21,8 +21,9 @@ {-# LANGUAGE Rank2Types #-} module Data.SBV.BitVectors.Model (- Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SNum- , sbvTestBit, sbvPopCount, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE+ Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral+ , sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight+ , allEqual, allDifferent, oneIf, blastBE, blastLE , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_ , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32 , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64@@ -455,30 +456,30 @@ (a0, b0, c0, d0, e0, f0, g0) .< (a1, b1, c1, d1, e1, f1, g1) = (a0, b0, c0, d0, e0, f0) .< (a1, b1, c1, d1, e1, f1) ||| ((a0, b0, c0, d0, e0, f0) .== (a1, b1, c1, d1, e1, f1) &&& g0 .< g1) --- | Symbolic Numbers. This is a simple class that simply incorporates all 'OrdSymbolic' and--- 'Num' values together, simplifying writing polymorphic type-signatures that work for all+-- | Symbolic Numbers. This is a simple class that simply incorporates all number like+-- base types together, simplifying writing polymorphic type-signatures that work for all -- symbolic numbers, such as 'SWord8', 'SInt8' etc. For instance, we can write a generic -- list-minimum function as follows: -- -- @--- mm :: SNum a => [a] -> a+-- mm :: SIntegral a => [SBV a] -> SBV a -- mm = foldr1 (\a b -> ite (a .<= b) a b) -- @ ----- It is similar to the standard 'Num' class, except ranging over symbolic instances.-class (OrdSymbolic a, Num a) => SNum a+-- It is similar to the standard 'Integral' class, except ranging over symbolic instances.+class (SymWord a, Num a, Bits a) => SIntegral a --- 'SNum' Instances, including all possible variants except 'SBool', since booleans+-- 'SIntegral' Instances, including all possible variants except 'Bool', since booleans -- are not numbers.-instance SNum SWord8-instance SNum SWord16-instance SNum SWord32-instance SNum SWord64-instance SNum SInt8-instance SNum SInt16-instance SNum SInt32-instance SNum SInt64-instance SNum SInteger+instance SIntegral Word8+instance SIntegral Word16+instance SIntegral Word32+instance SIntegral Word64+instance SIntegral Int8+instance SIntegral Int16+instance SIntegral Int32+instance SIntegral Int64+instance SIntegral Integer -- Boolean combinators instance Boolean SBool where@@ -672,6 +673,39 @@ setBitTo :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a setBitTo x i b = ite b (setBit x i) (clearBit x i) +-- | Generalization of 'shiftL', when the shift-amount is symbolic. Since Haskell's+-- 'shiftL' only takes an 'Int' as the shift amount, it cannot be used when we have+-- a symbolic amount to shift with. The shift amount must be an unsigned quantity.+sbvShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a+sbvShiftLeft x i+ | isSigned i = error "sbvShiftLeft: shift amount should be unsigned"+ | True = select [x `shiftL` k | k <- [0 .. bitSize x - 1]] 0 i++-- | Generalization of 'shiftR', when the shift-amount is symbolic. Since Haskell's+-- 'shiftR' only takes an 'Int' as the shift amount, it cannot be used when we have+-- a symbolic amount to shift with. The shift amount must be an unsigned quantity.+--+-- NB. If the shiftee is signed, then this is an arithmetic shift; otherwise it's logical,+-- following the usual Haskell convention. See 'sbvSignedShiftArithRight' for a variant+-- that explicitly uses the msb as the sign bit, even for unsigned underlying types.+sbvShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a+sbvShiftRight x i+ | isSigned i = error "sbvShiftRight: shift amount should be unsigned"+ | True = select [x `shiftR` k | k <- [0 .. bitSize x - 1]] 0 i++-- | Arithmetic shift-right with a symbolic unsigned shift amount. This is equivalent+-- to 'sbvShiftRight' when the argument is signed. However, if the argument is unsigned,+-- then it explicitly treats its msb as a sign-bit, and uses it as the bit that+-- gets shifted in. Useful when using the underlying unsigned bit representation to implement+-- custom signed operations. Note that there is no direct Haskell analogue of this function.+sbvSignedShiftArithRight:: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a+sbvSignedShiftArithRight x i+ | isSigned i = error "sbvSignedShiftArithRight: shift amount should be unsigned"+ | isSigned x = sbvShiftRight x i+ | True = ite (msb x)+ (complement (sbvShiftRight (complement x) i))+ (sbvShiftRight x i)+ -- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class. blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool] blastLE x@@ -932,7 +966,7 @@ -- | Total indexing operation. @select xs default index@ is intuitively -- the same as @xs !! index@, except it evaluates to @default@ if @index@ -- overflows- select :: (Bits b, SymWord b, Integral b) => [a] -> a -> SBV b -> a+ select :: (SymWord b, Num b) => [a] -> a -> SBV b -> a -- default definitions ite s a b | Just t <- unliteral s = if t then a else b@@ -945,11 +979,8 @@ -- list is really humongous, which is not very common in general. (Also, -- for the case when the list is bit-vectors, we use SMT tables anyhow.) select xs err ind- | isReal ind = error "SBV.select: unsupported real valued select/index expression"- | Just i <- unliteral ind = if i < 0 || i >= genericLength xs- then err- else xs `genericIndex` i- | True = walk xs ind err+ | isReal ind = error "SBV.select: unsupported real valued select/index expression"+ | True = walk xs ind err where walk [] _ acc = acc walk (e:es) i acc = walk es (i-1) (ite (i .== 0) e acc) @@ -1037,12 +1068,12 @@ () -> newExpr st k (SBVApp Ite [swt, swa, swb]) -- Custom version of select that translates to SMT-Lib tables at the base type of words select xs err ind- | Just i <- unliteral ind- = let i' :: Integer- i' = fromIntegral i- in if i' < 0 || i' >= genericLength xs then err else genericIndex xs i'- select [] err _ = err- select xs err ind = SBV kElt $ Right $ cache r+ | SBV _ (Left c) <- ind = case cwVal c of+ CWInteger i -> if i < 0 || i >= genericLength xs+ then err+ else xs `genericIndex` i+ _ -> error "SBV.select: unsupported real valued select/index expression"+ select xs err ind = SBV kElt $ Right $ cache r where kInd = kindOf ind kElt = kindOf err r st = do sws <- mapM (sbvToSW st) xs
Data/SBV/BitVectors/Splittable.hs view
@@ -118,7 +118,7 @@ -- is the sign digit. This is a bit awkward, but it is more consistent with the "reverse" view of -- little-big-endian representations ----- Minimal complete definiton: 'fromBitsLE'+-- Minimal complete definition: 'fromBitsLE' class FromBits a where fromBitsLE, fromBitsBE :: [SBool] -> a fromBitsBE = fromBitsLE . reverse
Data/SBV/Tools/Polynomial.hs view
@@ -33,7 +33,7 @@ -- -- for all @x@ (including @0@) ----- Minimal complete definiton: 'pMult', 'pDivMod', 'showPolynomial'+-- Minimal complete definition: 'pMult', 'pDivMod', 'showPolynomial' class (Num a, Bits a) => Polynomial a where -- | Given bit-positions to be set, create a polynomial -- For instance
RELEASENOTES view
@@ -1,7 +1,31 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub: <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 2.7+Latest Hackage released version: 2.8++======================================================================+Version 2.8, 2012-11-29++ - Rename the SNum class to SIntegral, and make it index over regular+ types. This makes it much more useful, simplifying coding of+ polymorphic symbolic functions over integral types, which is+ the common case.+ - Add the functions:+ - sbvShiftLeft+ - sbvShiftRight+ which can accommodate unsigned symbolic shift amounts. Note that+ one cannot use Haskell's shiftL/shiftR from the Bits class since+ they are hard-wired to take 'Int' values as the shift amounts only.+ - Add a new function 'sbvArithShiftRight', which is the same as+ a shift-right, except it uses the MSB of the input as the bit to fill+ in (instead of always filling in with 0 bits). Note that this is+ the same as shiftRight for signed values, but differs from a shiftRight+ when the input is unsigned. (There is no Haskell analogue of this+ function, as Haskell's shiftR is always arithmetic for signed+ types and logical for unsigned ones.) This variant is designed for+ use cases when one uses the underlying unsigned SMT-Lib representation+ to implement custom signed operations, for instance.+ - Several typo fixes. ====================================================================== Version 2.7, 2012-10-21
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Sat Oct 20 19:41:13 PDT 2012"+buildTime = "Wed Nov 28 19:14:22 PST 2012"
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 2.7+Version: 2.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