sbv 2.6 → 2.7
raw patch · 20 files changed
+90/−91 lines, 20 files
Files
- Data/SBV/BitVectors/Data.hs +1/−1
- Data/SBV/BitVectors/Model.hs +32/−32
- Data/SBV/BitVectors/PrettyNum.hs +1/−1
- Data/SBV/BitVectors/STree.hs +2/−2
- Data/SBV/BitVectors/Splittable.hs +6/−6
- Data/SBV/Examples/BitPrecise/PrefixSum.hs +2/−2
- Data/SBV/Examples/Existentials/CRCPolynomial.hs +3/−1
- Data/SBV/Examples/Puzzles/U2Bridge.hs +1/−1
- Data/SBV/Provers/Prover.hs +6/−7
- Data/SBV/Provers/Z3.hs +1/−1
- Data/SBV/Tools/Optimize.hs +1/−1
- Data/SBV/Tools/Polynomial.hs +7/−7
- RELEASENOTES +14/−16
- SBVUnitTest/Examples/Basics/BasicTests.hs +1/−1
- SBVUnitTest/Examples/Basics/ProofTests.hs +1/−1
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +4/−4
- SBVUnitTest/TestSuite/Basics/ArithSolver.hs +4/−4
- SBVUnitTest/TestSuite/CodeGeneration/Uninterpreted.hs +1/−0
- sbv.cabal +1/−2
Data/SBV/BitVectors/Data.hs view
@@ -29,7 +29,7 @@ , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), mkSFunArray, SArray(..), arrayUIKind , sbvToSW, sbvToSymSW , SBVExpr(..), newExpr- , cache, uncache, uncacheAI, HasKind(..)+ , cache, Cached, uncache, uncacheAI, HasKind(..) , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) , getTraceInfo, getConstraints, addConstraint , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom
Data/SBV/BitVectors/Model.hs view
@@ -18,7 +18,6 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE Rank2Types #-} module Data.SBV.BitVectors.Model (@@ -31,7 +30,7 @@ ) where -import Control.Monad (when)+import Control.Monad (when, liftM) import Data.Array (Array, Ix, listArray, elems, bounds, rangeSize) import Data.Bits (Bits(..))@@ -61,22 +60,21 @@ where c st = do swa <- sbvToSW st a opS st k swa -liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b-liftSym2 _ okCW opCR opCI (SBV k (Left a)) (SBV _ (Left b)) | okCW a b = SBV k $ Left $ mapCW2 opCR opCI noUnint2 a b-liftSym2 opS _ _ _ a@(SBV k _) b = SBV k $ Right $ cache c+liftSW2 :: (State -> Kind -> SW -> SW -> IO SW) -> Kind -> SBV a -> SBV b -> Cached SW+liftSW2 opS k a b = cache c where c st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b opS st k sw1 sw2 +liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b+liftSym2 _ okCW opCR opCI (SBV k (Left a)) (SBV _ (Left b)) | okCW a b = SBV k $ Left $ mapCW2 opCR opCI noUnint2 a b+liftSym2 opS _ _ _ a@(SBV k _) b = SBV k $ Right $ liftSW2 opS k a b+ liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> SBV b -> SBV b -> SBool liftSym2B _ okCW opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI noUnint2 a b)-liftSym2B opS _ _ _ a b = SBV (KBounded False 1) $ Right $ cache c- where c st = do sw1 <- sbvToSW st a- sw2 <- sbvToSW st b- opS st (KBounded False 1) sw1 sw2+liftSym2B opS _ _ _ a b = SBV (KBounded False 1) $ Right $ liftSW2 opS (KBounded False 1) a b -liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool)- -> SBool -> SBool+liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool) -> SBool -> SBool liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a liftSym1Bool opS _ a = SBV (KBounded False 1) $ Right $ cache c where c st = do sw <- sbvToSW st a@@ -524,12 +522,12 @@ -- | Returns (symbolic) true if all the elements of the given list are different. allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBool-allDifferent (x:xs@(_:_)) = bAll ((./=) x) xs &&& allDifferent xs+allDifferent (x:xs@(_:_)) = bAll (x ./=) xs &&& allDifferent xs allDifferent _ = true -- | Returns (symbolic) true if all the elements of the given list are the same. allEqual :: (Eq a, SymWord a) => [SBV a] -> SBool-allEqual (x:xs@(_:_)) = bAll ((.==) x) xs+allEqual (x:xs@(_:_)) = bAll (x .==) xs allEqual _ = true -- | Returns 1 if the boolean is true, otherwise 0.@@ -585,7 +583,7 @@ -- NB. In the optimizations below, use of -1 is valid as -- -1 has all bits set to True for both signed and unsigned values-instance (Bits a, SymWord a) => Bits (SBV a) where+instance (Num a, Bits a, SymWord a) => Bits (SBV a) where x .&. y | x `isConcretely` (== 0) = 0 | x `isConcretely` (== -1) = y@@ -605,6 +603,7 @@ complement = liftSym1 (mkSymOp1 Not) (noRealUnary "Not") complement bitSize _ = intSizeOf (undefined :: a) isSigned _ = hasSign (undefined :: a)+ bit i = 1 `shiftL` i shiftL x y | y < 0 = shiftR x (-y) | y == 0 = x@@ -627,27 +626,25 @@ x `testBit` i | isConcrete x = (x .&. bit i) /= 0 | True = error $ "SBV.testBit: Called on symbolic value: " ++ show x ++ ". Use sbvTestBit instead."-#if __GLASGOW_HASKELL__ >= 704 -- NB. popCount is *not* implementable on non-concrete symbolic words popCount x | isConcrete x = let go !c 0 = c go !c w = go (c+1) (w .&. (w-1)) in go 0 x | True = error $ "SBV.popCount: Called on symbolic value: " ++ show x ++ ". Use sbvPopCount instead."-#endif -- Since the underlying representation is just Integers, rotations has to be careful on the bit-size rot :: Bool -> Int -> Int -> Integer -> Integer rot toLeft sz amt x | sz < 2 = x- | True = (norm x y') `shiftL` y .|. norm (x `shiftR` y') y+ | True = norm x y' `shiftL` y .|. norm (x `shiftR` y') y where (y, y') | toLeft = (amt `mod` sz, sz - y) | True = (sz - y', amt `mod` sz) norm v s = v .&. ((1 `shiftL` s) - 1) -- | Replacement for 'testBit'. Since 'testBit' requires a 'Bool' to be returned, -- we cannot implement it for symbolic words. Index 0 is the least-significant bit.-sbvTestBit :: (Bits a, SymWord a) => SBV a -> Int -> SBool+sbvTestBit :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool sbvTestBit x i = (x .&. bit i) ./= 0 -- | Replacement for 'popCount'. Since 'popCount' returns an 'Int', we cannot implement@@ -659,7 +656,7 @@ -- purposes. In any case, we do not support 'sbvPopCount' for unbounded symbolic integers, -- as the only possible implementation wouldn't symbolically terminate. So the only overflow -- issue is with really-really large concrete 'SInteger' values.-sbvPopCount :: (Bits a, SymWord a) => SBV a -> SWord8+sbvPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8 sbvPopCount x | isReal x = error "SBV.sbvPopCount: Called on a real value" | isConcrete x = go 0 x@@ -672,30 +669,30 @@ -- | Generalization of 'setBit' based on a symbolic boolean. Note that 'setBit' and -- 'clearBit' are still available on Symbolic words, this operation comes handy when -- the condition to set/clear happens to be symbolic.-setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a+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) -- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class.-blastLE :: (Bits a, SymWord a) => SBV a -> [SBool]+blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool] blastLE x | isReal x = error "SBV.blastLE: Called on a real value" | not (isBounded x) = error "SBV.blastLE: Called on an infinite precision value"- | True = map (sbvTestBit x) [0 .. (intSizeOf x)-1]+ | True = map (sbvTestBit x) [0 .. intSizeOf x - 1] -- | Big-endian blasting of a word into its bits. Also see the 'FromBits' class.-blastBE :: (Bits a, SymWord a) => SBV a -> [SBool]+blastBE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool] blastBE = reverse . blastLE -- | Least significant bit of a word, always stored at index 0.-lsb :: (Bits a, SymWord a) => SBV a -> SBool+lsb :: (Num a, Bits a, SymWord a) => SBV a -> SBool lsb x = sbvTestBit x 0 -- | Most significant bit of a word, always stored at the last position.-msb :: (Bits a, SymWord a) => SBV a -> SBool+msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool msb x | isReal x = error "SBV.msb: Called on a real value" | not (isBounded x) = error "SBV.msb: Called on an infinite precision value"- | True = sbvTestBit x ((intSizeOf x) - 1)+ | True = sbvTestBit x (intSizeOf x - 1) -- Enum instance. These instances are suitable for use with concrete values, -- and will be less useful for symbolic values around. Note that `fromEnum` requires@@ -910,7 +907,7 @@ arbitrary = arbitrary >>= \r -> return $ SFunArray (const r) instance (SymWord a, Arbitrary a) => Arbitrary (SBV a) where- arbitrary = arbitrary >>= return . literal+ arbitrary = liftM literal arbitrary -- | Symbolic choice operator, parameterized via a class -- 'select' is a total-indexing function, with the default.@@ -1099,7 +1096,7 @@ -- Functions instance Mergeable b => Mergeable (a -> b) where- symbolicMerge t f g = \x -> symbolicMerge t (f x) (g x)+ symbolicMerge t f g x = symbolicMerge t (f x) (g x) {- Following definition, while correct, is utterly inefficient. Since the application is delayed, this hangs on to the inner list and all the impending merges, even when ind is concrete. Thus, it's much better to@@ -1171,8 +1168,8 @@ -- will suffer from efficiency issues; so we don't define it instance SymArray SFunArray where newArray _ = newArray_ -- the name is irrelevant in this case- newArray_ mbiVal = return $ SFunArray $ const $ maybe (error "Reading from an uninitialized array entry") id mbiVal- readArray (SFunArray f) a = f a+ newArray_ mbiVal = return $ SFunArray $ const $ fromMaybe (error "Reading from an uninitialized array entry") mbiVal+ readArray (SFunArray f) = f resetArray (SFunArray _) a = SFunArray $ const a writeArray (SFunArray f) a b = SFunArray (\a' -> ite (a .== a') b (f a')) mergeArrays t (SFunArray f) (SFunArray g) = SFunArray (\x -> ite t (f x) (g x))@@ -1381,8 +1378,8 @@ -- Uncurried functions of two arguments instance (SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV c, SBV b) -> SBV a) where- sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc2 `fmap` mbCgData) nm in \(arg0, arg1) -> f arg0 arg1- where uc2 (cs, fn) = (cs, \a b -> fn (a, b))+ sbvUninterpret mbCgData nm = let f = sbvUninterpret (uc2 `fmap` mbCgData) nm in uncurry f+ where uc2 (cs, fn) = (cs, curry fn) -- Uncurried functions of three arguments instance (SymWord d, SymWord c, SymWord b, HasKind a) => Uninterpreted ((SBV d, SBV c, SBV b) -> SBV a) where@@ -1460,3 +1457,6 @@ let xsbv = SBV (kindOf x) (Right (cache (const (return xsw)))) res = f xsbv sbvToSW st res++{-# ANN module "HLint: ignore Eta reduce" #-}+{-# ANN module "HLint: ignore Reduce duplication" #-}
Data/SBV/BitVectors/PrettyNum.hs view
@@ -9,7 +9,7 @@ -- Number representations in hex/bin ----------------------------------------------------------------------------- -{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeSynonymInstances #-} module Data.SBV.BitVectors.PrettyNum (PrettyNum(..), readBin, shex, shexI, sbin, sbinI) where
Data/SBV/BitVectors/STree.hs view
@@ -43,7 +43,7 @@ -- | Reading a value. We bit-blast the index and descend down the full tree -- according to bit-values.-readSTree :: (Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e+readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e readSTree s i = walk (blastBE i) s where walk [] (SLeaf v) = v walk (b:bs) (SBin l r) = ite b (walk bs r) (walk bs l)@@ -51,7 +51,7 @@ -- | Writing a value, similar to how reads are done. The important thing is that the tree -- representation keeps updates to a minimum.-writeSTree :: (Mergeable (SBV e), Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e+writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e writeSTree s i j = walk (blastBE i) s where walk [] _ = SLeaf j walk (b:bs) (SBin l r) = SBin (ite b l (walk bs l)) (ite b (walk bs r) r)
Data/SBV/BitVectors/Splittable.hs view
@@ -9,11 +9,11 @@ -- Implementation of bit-vector concatanetation and splits ----------------------------------------------------------------------------- -{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE BangPatterns #-} module Data.SBV.BitVectors.Splittable (Splittable(..), FromBits(..)) where @@ -124,14 +124,14 @@ fromBitsBE = fromBitsLE . reverse -- | Construct a symbolic word from its bits given in little-endian-fromBinLE :: (Bits a, SymWord a) => [SBool] -> SBV a+fromBinLE :: (Num a, Bits a, SymWord a) => [SBool] -> SBV a fromBinLE = go 0 0 where go !acc _ [] = acc go !acc !i (x:xs) = go (ite x (setBit acc i) acc) (i+1) xs -- | Perform a sanity check that we should receive precisely the same -- number of bits as required by the resulting type. The input is little-endian-checkAndConvert :: (Bits a, SymWord a) => Int -> [SBool] -> SBV a+checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a checkAndConvert sz xs | sz /= l = error $ "SBV.fromBits.SWord" ++ ssz ++ ": Expected " ++ ssz ++ " elements, got: " ++ show l
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -12,7 +12,7 @@ -- and <http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf>. ----------------------------------------------------------------------------- -{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} module Data.SBV.Examples.BitPrecise.PrefixSum where@@ -77,7 +77,7 @@ ---------------------------------------------------------------------- -- | Correctness theorem, for a powerlist of given size, an associative operator, and its left-unit element.-flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool+flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool flIsCorrect n zf = do args :: PowerList SWord32 <- mkForallVars n return $ ps zf args .== lf zf args
Data/SBV/Examples/Existentials/CRCPolynomial.hs view
@@ -75,7 +75,7 @@ cnt <- displayModels disp res putStrLn $ "Found: " ++ show cnt ++ " polynomail(s)." where disp :: Int -> (Bool, Word16) -> IO ()- disp n (_, s) = do putStrLn $ "Polynomial #" ++ show n ++ ". x^16 + " ++ showPolynomial False s+ disp n (_, s) = putStrLn $ "Polynomial #" ++ show n ++ ". x^16 + " ++ showPolynomial False s -- | Find and display all degree 16 polynomials with hamming distance at least 4, for 48 bit messages. --@@ -96,3 +96,5 @@ -- generated in about 5 minutes.) findHD4Polynomials :: IO () findHD4Polynomials = genPoly 4++{-# ANN crc_48_16 "HLint: ignore Use camelCase" #-}
Data/SBV/Examples/Puzzles/U2Bridge.hs view
@@ -9,7 +9,7 @@ -- The famous U2 bridge crossing puzzle: <http://www.brainj.net/puzzle.php?id=u2> ----------------------------------------------------------------------------- -{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-} module Data.SBV.Examples.Puzzles.U2Bridge where
Data/SBV/Provers/Prover.hs view
@@ -10,10 +10,9 @@ ----------------------------------------------------------------------------- {-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverlappingInstances #-}-{-# LANGUAGE PatternGuards #-}-{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE BangPatterns #-} module Data.SBV.Provers.Prover ( SMTSolver(..), SMTConfig(..), Predicate, Provable(..)@@ -36,9 +35,9 @@ import qualified Control.Exception as E import Control.Concurrent (forkIO, newChan, writeChan, getChanContents)-import Control.Monad (when, unless)+import Control.Monad (when, unless, void) import Data.List (intercalate)-import Data.Maybe (fromJust, isJust, catMaybes)+import Data.Maybe (fromJust, isJust, mapMaybe) import System.FilePath (addExtension) import System.Time (getClockTime) @@ -390,7 +389,7 @@ final r = add r >> stop die m = final (ProofError config [m]) -- only fork if non-verbose.. otherwise stdout gets garbled- fork io = if verbose config then io else forkIO io >> return ()+ fork io = if verbose config then io else void (forkIO io) fork $ E.catch (go sbvPgm add stop final (1::Int) []) (\e -> die (show (e::E.SomeException))) results <- getChanContents resChan@@ -454,7 +453,7 @@ let isTiming = timing config in case res of Result boundInfo usorts _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] ->- timeIf isTiming "translation" $ let uiMap = catMaybes (map arrayUIKind arrs) ++ map unintFnUIKind uis+ timeIf isTiming "translation" $ let uiMap = mapMaybe arrayUIKind arrs ++ map unintFnUIKind uis skolemMap = skolemize (if isSat then is else map flipQ is) where flipQ (ALL, x) = (EX, x) flipQ (EX, x) = (ALL, x)
Data/SBV/Provers/Z3.hs view
@@ -9,7 +9,7 @@ -- The connection to the Z3 SMT solver ----------------------------------------------------------------------------- -{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE PatternGuards #-} {-# LANGUAGE ScopedTypeVariables #-} module Data.SBV.Provers.Z3(z3) where
Data/SBV/Tools/Optimize.hs view
@@ -9,7 +9,7 @@ -- SMT based optimization ----------------------------------------------------------------------------- -{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeSynonymInstances #-} module Data.SBV.Tools.Optimize (OptimizeOpts(..), optimize, optimizeWith, minimize, minimizeWith, maximize, maximizeWith) where
Data/SBV/Tools/Polynomial.hs view
@@ -9,10 +9,10 @@ -- Implementation of polynomial arithmetic ----------------------------------------------------------------------------- +{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PatternGuards #-} {-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE PatternGuards #-} module Data.SBV.Tools.Polynomial (Polynomial(..), crc, crcBV) where @@ -34,7 +34,7 @@ -- for all @x@ (including @0@) -- -- Minimal complete definiton: 'pMult', 'pDivMod', 'showPolynomial'-class Bits a => Polynomial a where+class (Num a, Bits a) => Polynomial a where -- | Given bit-positions to be set, create a polynomial -- For instance --@@ -126,7 +126,7 @@ -- | Multiply two polynomials and reduce by the third (concrete) irreducible, given by its coefficients. -- See the remarks for the 'pMult' function for this design choice-polyMult :: (Bits a, SymWord a, FromBits (SBV a)) => (SBV a, SBV a, [Int]) -> SBV a+polyMult :: (Num a, Bits a, SymWord a, FromBits (SBV a)) => (SBV a, SBV a, [Int]) -> SBV a polyMult (x, y, red) | isReal x = error $ "SBV.polyMult: Received a real value: " ++ show x@@ -141,7 +141,7 @@ mul _ [] ps = ps mul as (b:bs) ps = mul (false:as) bs (ites b (as `addPoly` ps) ps) -polyDivMod :: (Bits a, SymWord a, FromBits (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)+polyDivMod :: (Num a, Bits a, SymWord a, FromBits (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a) polyDivMod x y | isReal x = error $ "SBV.polyDivMod: Received a real value: " ++ show x@@ -232,7 +232,7 @@ -- | Compute CRC's over polynomials, i.e., symbolic words. The first -- 'Int' argument plays the same role as the one in the 'crcBV' function.-crc :: (FromBits (SBV a), FromBits (SBV b), Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b+crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b crc n m p | isReal m || isReal p = error $ "SBV.crc: Received a real value: " ++ show (m, p)
RELEASENOTES view
@@ -1,24 +1,10 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub: <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 2.6--======================================================================-Version 2.6, 2012-10-20-- - Workaround issues related hackage compilation, in particular to the- problem with the new containers package release, which does provide- an NFData instance for sequences.--======================================================================-Version 2.5, 2012-10-19-- - Remove dependency on the hackage package strict-concurrency, as- hackage can no longer compile it due to some dependency mismatch.- - Add forgotten Real class instance for the type 'AlgReal'+Latest Hackage released version: 2.7 ======================================================================-Version 2.4, 2012-10-19+Version 2.7, 2012-10-21 - Add missing QuickCheck instance for SReal - When dealing with concrete SReal's, make sure to operate@@ -35,6 +21,18 @@ semantics. - Improve test suite, adding many constant-folding tests and start using cabal based tests (--enable-tests option.)++======================================================================+Versions 2.4, 2.5, and 2.6: Around mid October 2012++ - Workaround issues related hackage compilation, in particular to the+ problem with the new containers package release, which does provide+ an NFData instance for sequences.+ - Add explicit Num requirements when necessary, as the Bits class+ no longer does this.+ - Remove dependency on the hackage package strict-concurrency, as+ hackage can no longer compile it due to some dependency mismatch.+ - Add forgotten Real class instance for the type 'AlgReal' - Stop putting bounds on hackage dependencies, as they cause more trouble then they actually help. (See the discussion here: http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html.)
SBVUnitTest/Examples/Basics/BasicTests.hs view
@@ -9,7 +9,7 @@ -- Basic tests of the sbv library ----------------------------------------------------------------------------- -{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} module Examples.Basics.BasicTests where
SBVUnitTest/Examples/Basics/ProofTests.hs view
@@ -9,7 +9,7 @@ -- Basic proofs ----------------------------------------------------------------------------- -{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} module Examples.Basics.ProofTests where
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Fri Oct 19 18:57:09 PDT 2012"+buildTime = "Sat Oct 20 19:41:13 PDT 2012"
SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs view
@@ -54,7 +54,7 @@ ++ genBlasts ++ genCasts -genBinTest :: String -> (forall a. Bits a => a -> a -> a) -> [Test]+genBinTest :: String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [Test] genBinTest nm op = map mkTest $ zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `op` y | x <- sw8s, y <- sw8s] ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `op` y | x <- sw16s, y <- sw16s]@@ -82,7 +82,7 @@ where pair (x, y, a) b = (x, y, Just a == unliteral b) mkTest (x, y, s) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True" -genUnTest :: String -> (forall a. Bits a => a -> a) -> [Test]+genUnTest :: String -> (forall a. (Num a, Bits a) => a -> a) -> [Test] genUnTest nm op = map mkTest $ zipWith pair [(show x, op x) | x <- w8s ] [op x | x <- sw8s ] ++ zipWith pair [(show x, op x) | x <- w16s] [op x | x <- sw16s]@@ -96,7 +96,7 @@ where pair (x, a) b = (x, show (fromIntegral a `asTypeOf` b) == show b) mkTest (x, s) = "arithCF-" ++ nm ++ "." ++ x ~: s `showsAs` "True" -genIntTest :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]+genIntTest :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test] genIntTest nm op = map mkTest $ zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- is] [x `op` y | x <- sw8s, y <- is] ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- is] [x `op` y | x <- sw16s, y <- is]@@ -111,7 +111,7 @@ mkTest (t, x, y, a, b, s) = "arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True" is = [-10 .. 10] -genIntTestS :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]+genIntTestS :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test] genIntTestS nm op = map mkTest $ zipWith pair [("u8", show x, show y, x `op` y) | x <- w8s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw8s, y <- [0 .. (bitSize x - 1)]] ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (bitSize x - 1)]]
SBVUnitTest/TestSuite/Basics/ArithSolver.hs view
@@ -56,7 +56,7 @@ ++ genCasts -genBinTest :: Bool -> String -> (forall a. Bits a => a -> a -> a) -> [Test]+genBinTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a -> a) -> [Test] genBinTest unboundedOK nm op = map mkTest $ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- w8s ] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s] ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s]@@ -88,7 +88,7 @@ constrain $ b .== literal y return $ literal r .== a `opS` b -genUnTest :: Bool -> String -> (forall a. Bits a => a -> a) -> [Test]+genUnTest :: Bool -> String -> (forall a. (Num a, Bits a) => a -> a) -> [Test] genUnTest unboundedOK nm op = map mkTest $ [(show x, mkThm x (op x)) | x <- w8s ] ++ [(show x, mkThm x (op x)) | x <- w16s] ++ [(show x, mkThm x (op x)) | x <- w32s]@@ -103,7 +103,7 @@ constrain $ a .== literal x return $ literal r .== op a -genIntTest :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]+genIntTest :: String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test] genIntTest nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- is] ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- is] ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- is]@@ -120,7 +120,7 @@ return $ literal r .== a `op` y -genIntTestS :: Bool -> String -> (forall a. Bits a => a -> Int -> a) -> [Test]+genIntTestS :: Bool -> String -> (forall a. (Num a, Bits a) => a -> Int -> a) -> [Test] genIntTestS unboundedOK nm op = map mkTest $ [("u8", show x, show y, mkThm2 x y (x `op` y)) | x <- w8s, y <- [0 .. (bitSize x - 1)]] ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- [0 .. (bitSize x - 1)]] ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- [0 .. (bitSize x - 1)]]
SBVUnitTest/TestSuite/CodeGeneration/Uninterpreted.hs view
@@ -8,6 +8,7 @@ -- -- Test suite for Data.SBV.Examples.CodeGeneration.Uninterpreted -----------------------------------------------------------------------------+ module TestSuite.CodeGeneration.Uninterpreted(testSuite) where import Data.SBV
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 2.6+Version: 2.7 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@@ -97,7 +97,6 @@ default-language: Haskell2010 ghc-options : -Wall other-extensions: BangPatterns- CPP -- Currently commented out since Cabal doesn't yet recognize DefaultSignatures extension yet. Uncomment when it does. -- The current list can be seen at: https://github.com/haskell/cabal/blob/master/Cabal/Language/Haskell/Extension.hs -- DefaultSignatures