sbv 2.3 → 2.4
raw patch · 28 files changed
+1082/−522 lines, 28 filesdep ~HUnitdep ~QuickCheckdep ~array
Dependency ranges changed: HUnit, QuickCheck, array, base, containers, deepseq, directory, filepath, mtl, old-time, pretty, process, random, strict-concurrency, syb
Files
- Data/SBV.hs +2/−2
- Data/SBV/BitVectors/AlgReals.hs +27/−4
- Data/SBV/BitVectors/Data.hs +23/−2
- Data/SBV/BitVectors/Model.hs +156/−79
- Data/SBV/Compilers/C.hs +2/−0
- Data/SBV/Examples/CodeGeneration/GCD.hs +3/−3
- Data/SBV/Examples/Crypto/AES.hs +1/−1
- Data/SBV/Examples/Puzzles/Counts.hs +2/−2
- Data/SBV/Provers/Prover.hs +12/−2
- Data/SBV/SMT/SMT.hs +10/−9
- Data/SBV/Tools/Optimize.hs +2/−1
- Data/SBV/Tools/Polynomial.hs +1/−1
- LICENSE +1/−1
- README +22/−17
- RELEASENOTES +23/−1
- SBVUnitTest/Examples/Basics/QRem.hs +11/−6
- SBVUnitTest/Examples/Puzzles/Temperature.hs +8/−8
- SBVUnitTest/GoldFiles/temperature.gold +5/−2
- SBVUnitTest/SBVBasicTests.hs +64/−0
- SBVUnitTest/SBVTestCollection.hs +106/−0
- SBVUnitTest/SBVUnitTest.hs +17/−101
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +287/−0
- SBVUnitTest/TestSuite/Basics/ArithSolver.hs +270/−0
- SBVUnitTest/TestSuite/Basics/Arithmetic.hs +0/−248
- SBVUnitTest/TestSuite/Basics/QRem.hs +3/−1
- SBVUnitTest/TestSuite/Puzzles/Temperature.hs +1/−1
- sbv.cabal +22/−29
Data/SBV.hs view
@@ -133,7 +133,7 @@ -- ** Symbolic numbers , SNum -- ** Division- , BVDivisible(..)+ , SDivisible(..) -- ** The Boolean class , Boolean(..) -- *** Generalizations of boolean operations@@ -387,7 +387,7 @@ * Extraction and concatenation: 'split', '#', and 'extend' (see the 'Splittable' class) -Usual arithmetic ('+', '-', '*', 'bvQuotRem') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are+Usual arithmetic ('+', '-', '*', 'sQuotRem', 'sQuot', 'sRem', 'sDivMod', 'sDiv', 'sMod') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are supported for 'SInteger' fully, both in programming and verification modes. -}
Data/SBV/BitVectors/AlgReals.hs view
@@ -13,12 +13,13 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} -module Data.SBV.BitVectors.AlgReals (AlgReal(..), mkPolyReal, algRealToSMTLib2, algRealToHaskell, mergeAlgReals) where+module Data.SBV.BitVectors.AlgReals (AlgReal(..), mkPolyReal, algRealToSMTLib2, algRealToHaskell, mergeAlgReals, isExactRational, algRealStructuralEqual, algRealStructuralCompare) where -import Data.List (sortBy, isPrefixOf, partition)-import Data.Ratio ((%), numerator, denominator)-import Data.Function (on)+import Data.List (sortBy, isPrefixOf, partition)+import Data.Ratio ((%), numerator, denominator)+import Data.Function (on) import System.Random+import Test.QuickCheck (Arbitrary(..)) -- | Algebraic reals. Note that the representation is left abstract. We represent -- rational results explicitly, while the roots-of-polynomials are represented@@ -27,10 +28,16 @@ | AlgPolyRoot (Integer, Polynomial) -- which root (Maybe String) -- approximate decimal representation with given precision, if available +-- | Check wheter a given argument is an exact rational+isExactRational :: AlgReal -> Bool+isExactRational (AlgRational True _) = True+isExactRational _ = False+ -- | A univariate polynomial, represented simply as a -- coefficient list. For instance, "5x^3 + 2x - 5" is -- represented as [(5, 3), (2, 1), (-5, 0)] newtype Polynomial = Polynomial [(Integer, Integer)]+ deriving (Eq, Ord) -- | Construct a poly-root real with a given approximate value (either as a decimal, or polynomial-root) mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal@@ -96,6 +103,18 @@ AlgRational True a `compare` AlgRational True b = a `compare` b a `compare` b = error $ "AlgReal.compare: unsupported arguments: " ++ show (a, b) +-- Structural equality and ord for AlgReal; used when constants are Map keys+algRealStructuralEqual :: AlgReal -> AlgReal -> Bool+AlgRational a b `algRealStructuralEqual` AlgRational c d = (a, b) == (c, d)+AlgPolyRoot a b `algRealStructuralEqual` AlgPolyRoot c d = (a, b) == (c, d)+_ `algRealStructuralEqual` _ = False++algRealStructuralCompare :: AlgReal -> AlgReal -> Ordering+AlgRational a b `algRealStructuralCompare` AlgRational c d = (a, b) `compare` (c, d)+AlgRational _ _ `algRealStructuralCompare` AlgPolyRoot _ _ = LT+AlgPolyRoot _ _ `algRealStructuralCompare` AlgRational _ _ = GT+AlgPolyRoot a b `algRealStructuralCompare` AlgPolyRoot c d = (a, b) `compare` (c, d)+ instance Num AlgReal where (+) = lift2 "+" (+) (*) = lift2 "*" (*)@@ -198,3 +217,7 @@ | e1 = f | e2 = s mergeAlgReals m _ _ = error m++-- Quickcheck instance+instance Arbitrary AlgReal where+ arbitrary = AlgRational True `fmap` arbitrary
Data/SBV/BitVectors/Data.hs view
@@ -64,8 +64,29 @@ data CWVal = CWAlgReal AlgReal -- ^ algebraic real | CWInteger Integer -- ^ bit-vector/unbounded integer | CWUninterpreted String -- ^ value of an uninterpreted kind- deriving (Eq, Ord) +-- We cannot simply derive Eq/Ord for CWVal, since CWAlgReal doesn't have proper+-- instances for these when values are infinitely precise reals. However, we do+-- need a structural eq/ord for Map indexes; so define custom ones here:+instance Eq CWVal where+ CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b+ CWInteger a == CWInteger b = a == b+ CWUninterpreted a == CWUninterpreted b = a == b+ _ == _ = False++instance Ord CWVal where+ CWAlgReal a `compare` CWAlgReal b = a `algRealStructuralCompare` b+ CWAlgReal _ `compare` CWInteger _ = LT+ CWAlgReal _ `compare` CWUninterpreted _ = LT++ CWInteger _ `compare` CWAlgReal _ = GT+ CWInteger a `compare` CWInteger b = a `compare` b+ CWInteger _ `compare` CWUninterpreted _ = LT++ CWUninterpreted _ `compare` CWAlgReal _ = GT+ CWUninterpreted _ `compare` CWInteger _ = GT+ CWUninterpreted a `compare` CWUninterpreted b = a `compare` b+ -- | 'CW' represents a concrete word of a fixed size: -- Endianness is mostly irrelevant (see the 'FromBits' class). -- For signed words, the most significant digit is considered to be the sign.@@ -163,7 +184,7 @@ -- | Symbolic operations data Op = Plus | Times | Minus- | Quot | Rem -- quot and rem are unsigned only+ | Quot | Rem | Equal | NotEqual | LessThan | GreaterThan | LessEq | GreaterEq | Ite
Data/SBV/BitVectors/Model.hs view
@@ -14,6 +14,7 @@ {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE PatternGuards #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -21,7 +22,7 @@ {-# LANGUAGE Rank2Types #-} module Data.SBV.BitVectors.Model (- Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..), SNum+ Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SNum , sbvTestBit, sbvPopCount, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_ , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32@@ -60,16 +61,16 @@ where c st = do swa <- sbvToSW st a opS st k swa -liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b-liftSym2 _ opCR opCI (SBV k (Left a)) (SBV _ (Left b)) = SBV k $ Left $ mapCW2 opCR opCI noUnint2 a b-liftSym2 opS _ _ a@(SBV k _) b = SBV k $ Right $ cache c+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 where c st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b opS st k sw1 sw2 -liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> SBV b -> SBV b -> SBool-liftSym2B _ opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) = literal (liftCW2 opCR opCI noUnint2 a b)-liftSym2B opS _ _ a b = SBV (KBounded False 1) $ Right $ cache c+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@@ -199,6 +200,11 @@ literal = SBV KReal . Left . CW KReal . CWAlgReal fromCW (CW _ (CWAlgReal a)) = a fromCW c = error $ "SymWord.AlgReal: Unexpected non-real value: " ++ show c+ -- AlgReal needs its own definition of isConcretely+ -- to make sure we avoid using unimplementable Haskell functions+ isConcretely (SBV KReal (Left (CW KReal (CWAlgReal v)))) p+ | isExactRational v = p v+ isConcretely _ _ = False mbMaxBound = Nothing mbMinBound = Nothing @@ -343,8 +349,8 @@ -} instance EqSymbolic (SBV a) where- (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW) Equal) (==) (==)- (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) (/=) (/=)+ (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW) Equal) rationalCheck (==) (==)+ (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) rationalCheck (/=) (/=) eqOpt :: SW -> SW -> SW -> Maybe SW eqOpt w x y = if x == y then Just w else Nothing@@ -353,19 +359,19 @@ x .< y | Just mb <- mbMaxBound, x `isConcretely` (== mb) = false | Just mb <- mbMinBound, y `isConcretely` (== mb) = false- | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) (<) (<) x y+ | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) rationalCheck (<) (<) x y x .<= y | Just mb <- mbMinBound, x `isConcretely` (== mb) = true | Just mb <- mbMaxBound, y `isConcretely` (== mb) = true- | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) (<=) (<=) x y+ | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) rationalCheck (<=) (<=) x y x .> y | Just mb <- mbMinBound, x `isConcretely` (== mb) = false | Just mb <- mbMaxBound, y `isConcretely` (== mb) = false- | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) (>) (>) x y+ | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>) (>) x y x .>= y | Just mb <- mbMaxBound, x `isConcretely` (== mb) = true | Just mb <- mbMinBound, y `isConcretely` (== mb) = true- | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) (>=) (>=) x y+ | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) rationalCheck (>=) (>=) x y -- Bool instance EqSymbolic Bool where@@ -536,16 +542,16 @@ x + y | x `isConcretely` (== 0) = y | y `isConcretely` (== 0) = x- | True = liftSym2 (mkSymOp Plus) (+) (+) x y+ | True = liftSym2 (mkSymOp Plus) rationalCheck (+) (+) x y x * y | x `isConcretely` (== 0) = 0 | y `isConcretely` (== 0) = 0 | x `isConcretely` (== 1) = y | y `isConcretely` (== 1) = x- | True = liftSym2 (mkSymOp Times) (*) (*) x y+ | True = liftSym2 (mkSymOp Times) rationalCheck (*) (*) x y x - y | y `isConcretely` (== 0) = x- | True = liftSym2 (mkSymOp Minus) (-) (-) x y+ | True = liftSym2 (mkSymOp Minus) rationalCheck (-) (-) x y abs a | hasSign a = ite (a .< 0) (-a) a | True = a@@ -555,10 +561,21 @@ instance Fractional SReal where fromRational = literal . fromRational- x / y = liftSym2 (mkSymOp Quot) (/) die x y+ x / y = liftSym2 (mkSymOp Quot) rationalCheck (/) die x y where -- should never happen die = error $ "impossible: non-real value found in Fractional.SReal " ++ show (x, y) +-- Most operations on concrete rationals require a compatibility check+rationalCheck :: CW -> CW -> Bool+rationalCheck a b = case (cwVal a, cwVal b) of+ (CWAlgReal x, CWAlgReal y) -> isExactRational x && isExactRational y+ _ -> True++-- same as above, for SBV's+rationalSBVCheck :: SBV a -> SBV a -> Bool+rationalSBVCheck (SBV KReal (Left a)) (SBV KReal (Left b)) = rationalCheck a b+rationalSBVCheck _ _ = True+ -- Some operations will never be used on Reals, but we need fillers: noReal :: String -> AlgReal -> AlgReal -> AlgReal noReal o a b = error $ "SBV.AlgReal." ++ o ++ ": Unexpected arguments: " ++ show (a, b)@@ -574,17 +591,17 @@ | x `isConcretely` (== -1) = y | y `isConcretely` (== 0) = 0 | y `isConcretely` (== -1) = x- | True = liftSym2 (mkSymOp And) (noReal ".&.") (.&.) x y+ | True = liftSym2 (mkSymOp And) (const (const True)) (noReal ".&.") (.&.) x y x .|. y | x `isConcretely` (== 0) = y | x `isConcretely` (== -1) = -1 | y `isConcretely` (== 0) = x | y `isConcretely` (== -1) = -1- | True = liftSym2 (mkSymOp Or) (noReal ".|.") (.|.) x y+ | True = liftSym2 (mkSymOp Or) (const (const True)) (noReal ".|.") (.|.) x y x `xor` y | x `isConcretely` (== 0) = y | y `isConcretely` (== 0) = x- | True = liftSym2 (mkSymOp XOr) (noReal "xor") xor x y+ | True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor x y complement = liftSym1 (mkSymOp1 Not) (noRealUnary "Not") complement bitSize _ = intSizeOf (undefined :: a) isSigned _ = hasSign (undefined :: a)@@ -731,100 +748,160 @@ Nothing -> error $ "Enum." ++ w ++ "{" ++ showType x ++ "}: Called on symbolic value " ++ show x Just v -> fromIntegral v --- | The 'BVDivisible' class captures the essence of division of words.+-- | The 'SDivisible' class captures the essence of division. -- Unfortunately we cannot use Haskell's 'Integral' class since the 'Real' -- and 'Enum' superclasses are not implementable for symbolic bit-vectors.--- However, 'quotRem' makes perfect sense, and the 'BVDivisible' class captures+-- However, 'quotRem' and 'divMod' makes perfect sense, and the 'SDivisible' class captures -- this operation. One issue is how division by 0 behaves. The verification -- technology requires total functions, and there are several design choices -- here. We follow Isabelle/HOL approach of assigning the value 0 for division -- by 0. Therefore, we impose the following law: ----- @ x `bvQuotRem` 0 = (0, x) @+-- @ x `sQuotRem` 0 = (0, x) @+-- @ x `sDivMod` 0 = (0, x) @ -- -- Note that our instances implement this law even when @x@ is @0@ itself. ----- Minimal complete definition: 'bvQuotRem'-class BVDivisible a where- bvQuotRem :: a -> a -> (a, a)+-- NB. 'quot' truncates toward zero, while 'div' truncates toward negative infinity.+--+-- Minimal complete definition: 'sQuotRem', 'sDivMod'+class SDivisible a where+ sQuotRem :: a -> a -> (a, a)+ sDivMod :: a -> a -> (a, a)+ sQuot :: a -> a -> a+ sRem :: a -> a -> a+ sDiv :: a -> a -> a+ sMod :: a -> a -> a -instance BVDivisible Word64 where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+ x `sQuot` y = fst $ x `sQuotRem` y+ x `sRem` y = snd $ x `sQuotRem` y+ x `sDiv` y = fst $ x `sDivMod` y+ x `sMod` y = snd $ x `sDivMod` y -instance BVDivisible Int64 where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+instance SDivisible Word64 where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible Word32 where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+instance SDivisible Int64 where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible Int32 where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+instance SDivisible Word32 where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible Word16 where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+instance SDivisible Int32 where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible Int16 where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+instance SDivisible Word16 where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible Word8 where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+instance SDivisible Int16 where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible Int8 where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+instance SDivisible Word8 where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible Integer where- bvQuotRem x 0 = (0, x)- bvQuotRem x y = x `quotRem` y+instance SDivisible Int8 where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible CW where- bvQuotRem a b- | CWInteger x <- cwVal a, CWInteger y <- cwVal b- = let (r1, r2) = bvQuotRem x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })- bvQuotRem a b = error $ "SBV.liftQRem: impossible, unexpected args received: " ++ show (a, b)+instance SDivisible Integer where+ sQuotRem x 0 = (0, x)+ sQuotRem x y = x `quotRem` y+ sDivMod x 0 = (0, x)+ sDivMod x y = x `divMod` y -instance BVDivisible SWord64 where- bvQuotRem = liftQRem+instance SDivisible CW where+ sQuotRem a b+ | CWInteger x <- cwVal a, CWInteger y <- cwVal b+ = let (r1, r2) = sQuotRem x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })+ sQuotRem a b = error $ "SBV.sQuotRem: impossible, unexpected args received: " ++ show (a, b)+ sDivMod a b+ | CWInteger x <- cwVal a, CWInteger y <- cwVal b+ = let (r1, r2) = sDivMod x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })+ sDivMod a b = error $ "SBV.sDivMod: impossible, unexpected args received: " ++ show (a, b) -instance BVDivisible SInt64 where- bvQuotRem = liftQRem+instance SDivisible SWord64 where+ sQuotRem = liftQRem+ sDivMod = liftDMod -instance BVDivisible SWord32 where- bvQuotRem = liftQRem+instance SDivisible SInt64 where+ sQuotRem = liftQRem+ sDivMod = liftDMod -instance BVDivisible SInt32 where- bvQuotRem = liftQRem+instance SDivisible SWord32 where+ sQuotRem = liftQRem+ sDivMod = liftDMod -instance BVDivisible SWord16 where- bvQuotRem = liftQRem+instance SDivisible SInt32 where+ sQuotRem = liftQRem+ sDivMod = liftDMod -instance BVDivisible SInt16 where- bvQuotRem = liftQRem+instance SDivisible SWord16 where+ sQuotRem = liftQRem+ sDivMod = liftDMod -instance BVDivisible SWord8 where- bvQuotRem = liftQRem+instance SDivisible SInt16 where+ sQuotRem = liftQRem+ sDivMod = liftDMod -instance BVDivisible SInt8 where- bvQuotRem = liftQRem+instance SDivisible SWord8 where+ sQuotRem = liftQRem+ sDivMod = liftDMod -instance BVDivisible SInteger where- bvQuotRem = liftQRem+instance SDivisible SInt8 where+ sQuotRem = liftQRem+ sDivMod = liftDMod -liftQRem :: (SymWord a, Num a, BVDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)+liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a) liftQRem x y = ite (y .== 0) (0, x) (qr x y)- where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = bvQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r))+ where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = sQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r)) qr a@(SBV sgnsz _) b = (SBV sgnsz (Right (cache (mk Quot))), SBV sgnsz (Right (cache (mk Rem)))) where mk o st = do sw1 <- sbvToSW st a sw2 <- sbvToSW st b mkSymOp o st sgnsz sw1 sw2 +-- Conversion from quotRem (truncate to 0) to divMod (truncate towards negative infinity)+liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)+liftDMod x y = ite (y .== 0) (0, x) $ ite (signum r .== negate (signum y)) (q-1, r+y) qr+ where qr@(q, r) = x `sQuotRem` y++-- SInteger instance for quotRem/divMod are tricky!+-- SMT-Lib only has Euclidean operations, but Haskell+-- uses "truncate to 0" for quotRem, and "truncate to negative infinity" for divMod.+-- So, we cannot just use the above liftings directly.+instance SDivisible SInteger where+ sDivMod = liftDMod+ sQuotRem x y+ | not (isSymbolic x || isSymbolic y)+ = liftQRem x y+ | True+ = ite (y .== 0) (0, x) (qE+i, rE-i*y)+ where (qE, rE) = liftQRem x y -- for integers, this is euclidean due to SMTLib semantics+ i = ite (x .>= 0 ||| rE .== 0) 0+ $ ite (y .> 0) 1 (-1)+ -- Quickcheck interface -- The Arbitrary instance for SFunArray returns an array initialized@@ -890,7 +967,7 @@ -- Of course, we do not have a way of enforcing that in the user code, but -- at least our library code respects that invariant. symbolicMerge t a@(SBV{}) b@(SBV{})- | Just av <- unliteral a, Just bv <- unliteral b, av == bv+ | Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv = a | True = SBV k $ Right $ cache c
Data/SBV/Compilers/C.hs view
@@ -507,6 +507,8 @@ Just i -> (True, canOverflow True i) KUninterpreted s -> die $ "Uninterpreted sort: " ++ s -- Div/Rem should be careful on 0, in the SBV world x `div` 0 is 0, x `rem` 0 is x+ -- NB: Quot is supposed to truncate toward 0; Not clear to me if C guarantees this behavior.+ -- Brief googling suggests C99 does indeed truncate toward 0, but other C compilers might differ. p Quot [a, b] = parens (b <+> text "== 0") <+> text "?" <+> text "0" <+> text ":" <+> parens (a <+> text "/" <+> b) p Rem [a, b] = parens (b <+> text "== 0") <+> text "?" <+> a <+> text ":" <+> parens (a <+> text "%" <+> b) p o [a, b]
Data/SBV/Examples/CodeGeneration/GCD.hs view
@@ -35,7 +35,7 @@ go x y c = ite (c .== 0 ||| y .== 0) -- stop if y is 0, or if we reach the recursion depth x (go y y' (c-1))- where (_, y') = x `bvQuotRem` y+ where (_, y') = x `sQuotRem` y ----------------------------------------------------------------------------- -- * Verification@@ -58,8 +58,8 @@ (isCommonDivisor k ==> k' .>= k)) -- if k is a common divisor as well, then k' is at least as large as k where k' = sgcd x y isCommonDivisor a = z1 .== 0 &&& z2 .== 0- where (_, z1) = x `bvQuotRem` a- (_, z2) = y `bvQuotRem` a+ where (_, z1) = x `sQuotRem` a+ (_, z2) = y `sQuotRem` a ----------------------------------------------------------------------------- -- * Code generation
Data/SBV/Examples/Crypto/AES.hs view
@@ -40,7 +40,7 @@ type GF28 = SWord8 -- | Multiplication in GF(2^8). This is simple polynomial multipliation, followed--- by the irreducible polynomial @x^8+x^5+x^3+x^1+1@. We simply use the 'pMult'+-- by the irreducible polynomial @x^8+x^4+x^3+x^1+1@. We simply use the 'pMult' -- function exported by SBV to do the operation. gf28Mult :: GF28 -> GF28 -> GF28 gf28Mult x y = pMult (x, y, [8, 4, 3, 1, 0])
Data/SBV/Examples/Puzzles/Counts.hs view
@@ -39,8 +39,8 @@ (ite (n .< 100) (upd d1 (upd d2 cnts)) -- two digits (upd d1 (upd d2 (upd d3 cnts)))) -- three digits- where (r1, d1) = n `bvQuotRem` 10- (d3, d2) = r1 `bvQuotRem` 10+ where (r1, d1) = n `sQuotRem` 10+ (d3, d2) = r1 `sQuotRem` 10 upd d = zipWith inc [0..] where inc i c = ite (i .== d) (c+1) c
Data/SBV/Provers/Prover.hs view
@@ -53,7 +53,17 @@ import Data.SBV.Utils.Boolean mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig-mkConfig s isSMTLib2 tweaks = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, printRealPrec = 16, smtFile = Nothing, solver = s, solverTweaks = tweaks, useSMTLib2 = isSMTLib2}+mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False+ , timing = False+ , timeOut = Nothing+ , printBase = 10+ , printRealPrec = 16+ , smtFile = Nothing+ , solver = s+ , solverTweaks = tweaks+ , useSMTLib2 = isSMTLib2+ , satCmd = "(check-sat)"+ } -- | Default configuration for the Yices SMT Solver. yices :: SMTConfig@@ -61,7 +71,7 @@ -- | Default configuration for the Z3 SMT solver z3 :: SMTConfig-z3 = mkConfig Z3.z3 True ["(set-option :mbqi true) ; use model based quantification"]+z3 = mkConfig Z3.z3 True ["(set-option :mbqi true) ; use model based quantifier instantiation"] -- | The default solver used by SBV. This is currently set to z3. defaultSMTCfg :: SMTConfig
Data/SBV/SMT/SMT.hs view
@@ -53,6 +53,7 @@ , printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.) , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified)+ , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly) , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1 , solver :: SMTSolver -- ^ The actual SMT solver.@@ -349,13 +350,13 @@ where shC s = " " ++ s -- | Helper function to spin off to an SMT solver.-pipeProcess :: Bool -> String -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])-pipeProcess verb nm execName opts script cleanErrs = do+pipeProcess :: SMTConfig -> String -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])+pipeProcess cfg nm execName opts script cleanErrs = do mbExecPath <- findExecutable execName case mbExecPath of Nothing -> return $ Left $ "Unable to locate executable for " ++ nm ++ "\nExecutable specified: " ++ show execName- Just execPath -> do (ec, contents, allErrors) <- runSolver verb execPath opts script+ Just execPath -> do (ec, contents, allErrors) <- runSolver cfg execPath opts script let errors = dropWhile isSpace (cleanErrs allErrors) case ec of ExitSuccess -> if null errors@@ -393,7 +394,7 @@ Nothing -> return () Just f -> do putStrLn $ "** Saving the generated script in file: " ++ show f writeFile f (scriptBody script)- contents <- timeIf isTiming nmSolver $ pipeProcess (verbose config) nmSolver exec opts script cleanErrs+ contents <- timeIf isTiming nmSolver $ pipeProcess config nmSolver exec opts script cleanErrs msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents case contents of Left e -> return $ failure (lines e)@@ -401,8 +402,8 @@ -- | A variant of 'readProcessWithExitCode'; except it knows about continuation strings -- and can speak SMT-Lib2 (just a little).-runSolver :: Bool -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String)-runSolver verb execPath opts script+runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String)+runSolver cfg execPath opts script | isNothing $ scriptModel script = readProcessWithExitCode execPath opts (scriptBody script) | True@@ -429,11 +430,11 @@ else return (ex, r ++ "\n" ++ out, err) return (send, ask, cleanUp) mapM_ send (lines (scriptBody script))- r <- ask "(check-sat)"+ r <- ask $ satCmd cfg when (any (`isPrefixOf` r) ["sat", "unknown"]) $ do let mls = lines (fromJust (scriptModel script))- when verb $ do putStrLn "** Sending the following model extraction commands:"- mapM_ putStrLn mls+ when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:"+ mapM_ putStrLn mls mapM_ send mls cleanUp r
Data/SBV/Tools/Optimize.hs view
@@ -84,7 +84,8 @@ msg "Trying to find a satisfying solution." m <- satWith cfg $ valid `fmap` mkExistVars n case getModel m of- Left _ -> return Nothing+ Left _ -> do msg "No satisfying solutions found."+ return Nothing Right (True, _) -> error "SBV: Backend solver reported \"unknown\"" Right (False, a) -> do msg $ "First solution found: " ++ show a let c = cost (map literal a)
Data/SBV/Tools/Polynomial.hs view
@@ -27,7 +27,7 @@ import Data.SBV.Utils.Boolean -- | Implements polynomial addition, multiplication, division, and modulus operations--- over GF(2^n). NB. Similar to 'bvQuotRem', division by @0@ is interpreted as follows:+-- over GF(2^n). NB. Similar to 'sQuotRem', division by @0@ is interpreted as follows: -- -- @x `pDivMod` 0 = (0, x)@ --
LICENSE view
@@ -1,4 +1,4 @@-SBV: A library for Symbolic Bitvectors+SBV: SMT Based Verification in Haskell Copyright (c) 2010-2012, Levent Erkok (erkokl@gmail.com) All rights reserved.
README view
@@ -24,9 +24,14 @@ bit-vectors. Functions for checking satisfiability (`sat` and `allSat`) are also provided. In addition, functions using the SBV library can be compiled to C automatically. +Build Status+============+SBV uses Travis-CI's automated build infrastructure, making a build for each commit. Current build status:+[](http://travis-ci.org/LeventErkok/sbv)+ Resources =========-The sbv library is hosted at [http://github.com/LeventErkok/sbv](http://github.com/LeventErkok/sbv).+The SBV library is hosted at [http://github.com/LeventErkok/sbv](http://github.com/LeventErkok/sbv). The hackage site [http://hackage.haskell.org/package/sbv](http://hackage.haskell.org/package/sbv) is the best place@@ -36,7 +41,7 @@ Overview ========-The Haskell sbv library provides support for dealing with Symbolic Bit Vectors+The Haskell SBV library provides support for dealing with Symbolic Bit Vectors in Haskell. It introduces the types: - `SBool`: Symbolic Booleans (bits).@@ -60,9 +65,9 @@ - proven correct via an external SMT solver (the `prove` function) - checked for satisfiability (the `sat`, and `allSat` functions) - used in synthesis (the `sat` function with existentials)- - optimized with respect to cost functions (the 'optimize', 'maximize', and 'minimize' functions)+ - optimized with respect to cost functions (the `optimize`, `maximize`, and `minimize` functions) - quick-checked- - used in concrete test case generation (the 'genTest' function), rendered as values in various+ - used in concrete test case generation (the `genTest` function), rendered as values in various languages, including Haskell and C. If a predicate is not valid, `prove` will return a counterexample: An @@ -75,17 +80,17 @@ Use of SMT solvers ==================-The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: -[http://goedel.cs.uiowa.edu/smtlib/](http://goedel.cs.uiowa.edu/smtlib/)+The SBV library uses third-party SMT solvers via the standard SMT-Lib interface+[http://goedel.cs.uiowa.edu/smtlib/](http://goedel.cs.uiowa.edu/smtlib/). -The SBV library is designed to work with any SMT-Lib compliant SMT-solver, although integration with-individual solvers require some library work.-Currently, we fully support -the [Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) SMT solver from Microsoft,-and -the [Yices](http://yices.csl.sri.com) SMT solver from SRI.-Both solvers are available for Windows, Linux, and Mac OSX.+Currently, we fully support the+[Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) SMT solver from Microsoft,+and the [Yices](http://yices.csl.sri.com) SMT solver from SRI. Both solvers are available+for Windows, Linux, and Mac OSX. +Other SMT solvers can be used with SBV as well, with a relatively easy hook-up mechanism. Please+do get in touch if you plan to use SBV with any other solver.+ Prerequisites ============= You **should** have at least one of @@ -98,7 +103,7 @@ of the yices executable in the environment variable `SBV_YICES` and the options to yices in `SBV_YICES_OPTIONS`. (The default for the latter is `"-m -f"`). Similarly the environment variables `SBV_Z3` and `SBV_Z3_OPTIONS` can be used for choosing executable location and custom options for Z3. (The default for the latter is-`"/in /smt2"` on Windows and `"-in -smt2"` on Mac and Linux. You should use Z3 version 3.2 or later.)+`"/in /smt2"` on Windows and `"-in -smt2"` on Mac and Linux. You should use Z3 version 4.1 or later.) Examples =========@@ -110,7 +115,7 @@ Installation ============-The sbv library is cabalized. Assuming you have cabal/ghc installed, it should merely+The SBV library is cabalized. Assuming you have cabal/ghc installed, it should merely be a matter of running cabal install sbv@@ -118,11 +123,11 @@ Please see [INSTALL](http://github.com/LeventErkok/sbv/tree/master/INSTALL) for installation details. Once the installation is done, you can run the executable `SBVUnitTests` which will-execute the regression test suite for sbv on your machine to ensure all is well.+execute the regression test suite for SBV on your machine to ensure all is well. Copyright, License ==================-The sbv library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for+The SBV library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for details. The [LICENSE](http://github.com/LeventErkok/sbv/tree/master/LICENSE) file contains the [BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.
RELEASENOTES view
@@ -1,7 +1,29 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub: <http://github.com/LeventErkok/sbv> -Latest Hackage released version: 2.3+Latest Hackage released version: 2.4++======================================================================+Version 2.4, 2012-10-19++ - Add missing QuickCheck instance for SReal+ - When dealing with concrete SReal's, make sure to operate+ only on exact algebraic reals on the Haskell side, leaving+ true algebraic reals (i.e., those that are roots of polynomials+ that cannot be expressed as a rational) symbolic. This avoids+ issues with functions that we cannot implement directly on+ the Haskell side, like exact square-roots.+ - Documentation tweaks, typo fixes etc.+ - Rename BVDivisible class to SDivisible; since SInteger+ is also an instance of this class, and SDivisible is a+ more appropriate name to start with. Also add sQuot and sRem+ methods; along with sDivMod, sDiv, and sMod, with usual+ semantics. + - Improve test suite, adding many constant-folding tests+ and start using cabal based tests (--enable-tests option.)+ - 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.) ====================================================================== Version 2.3, 2012-07-20
SBVUnitTest/Examples/Basics/QRem.hs view
@@ -6,7 +6,7 @@ -- Maintainer : erkokl@gmail.com -- Stability : experimental ----- Testing the qrem (quote-rem) function+-- Testing the sQuotRem and sDivMod ----------------------------------------------------------------------------- module Examples.Basics.QRem where@@ -14,12 +14,17 @@ import Data.SBV -- check: if (a, b) = x `quotRem` y then x = y*a + b+-- same is also true for divMod -- being careful about y = 0. When divisor is 0, then quotient is -- defined to be 0 and the remainder is the numerator-qrem :: (Num a, EqSymbolic a, BVDivisible a) => a -> a -> SBool-qrem x y = ite (y .== 0) ((0, x) .== (a, b)) (x .== y * a + b)- where (a, b) = x `bvQuotRem` y+qrem :: (Num a, EqSymbolic a, SDivisible a) => a -> a -> SBool+qrem x y = ite (y .== 0)+ ((0, x) .== (q, r) &&& (0, x) .== (d, m))+ (x .== y * q + r &&& x .== y * d + m)+ where (q, r) = x `sQuotRem` y+ (d, m) = x `sDivMod` y check :: IO ()-check = print =<< prove (qrem :: SWord8 -> SWord8 -> SBool)- -- print =<< prove (qrem :: SWord16 -> SWord16 -> SBool) -- takes too long!+check = do print =<< prove (qrem :: SWord8 -> SWord8 -> SBool)+ print =<< prove (qrem :: SInt8 -> SInt8 -> SBool)+ print =<< prove (qrem :: SInteger -> SInteger -> SBool)
SBVUnitTest/Examples/Puzzles/Temperature.hs view
@@ -15,25 +15,25 @@ import Data.SBV -type Temp = SWord16 -- larger than we need actually+type Temp = SInteger -- convert celcius to fahrenheit, rounding up/down properly -- we have to be careful here to make sure rounding is done properly.. d2f :: Temp -> Temp d2f d = 32 + ite (fr .>= 5) (1+fi) fi- where (fi, fr) = (18 * d) `bvQuotRem` 10+ where (fi, fr) = (18 * d) `sQuotRem` 10 -- puzzle: What 2 digit fahrenheit/celcius values are reverses of each other? revOf :: Temp -> SBool revOf c = swap (digits c) .== digits (d2f c)- where digits x = x `bvQuotRem` 10+ where digits x = x `sQuotRem` 10 swap (a, b) = (b, a) -solve :: IO ()-solve = do res <- allSat $ revOf `fmap` exists_- cnt <- displayModels disp res- putStrLn $ "Found " ++ show cnt ++ " solutions."- where disp :: Int -> (Bool, Word16) -> IO ()+puzzle :: IO ()+puzzle = do res <- allSat $ revOf `fmap` exists_+ cnt <- displayModels disp res+ putStrLn $ "Found " ++ show cnt ++ " solutions."+ where disp :: Int -> (Bool, Integer) -> IO () disp _ (_, x) = putStrLn $ " " ++ show x ++ "C --> " ++ show (round f :: Integer) ++ "F (exact value: " ++ show f ++ "F)" where f :: Double f = 32 + (9 * fromIntegral x) / 5
SBVUnitTest/GoldFiles/temperature.gold view
@@ -1,2 +1,5 @@-Satisfiable. Model:- s0 = 28 :: SWord16+Solution #1:+ s0 = 16 :: SInteger+Solution #2:+ s0 = 28 :: SInteger+Found 2 different solutions.
+ SBVUnitTest/SBVBasicTests.hs view
@@ -0,0 +1,64 @@+-----------------------------------------------------------------------------+-- |+-- Module : Main+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- SBV library basic test suite; i.e., those tests that do not+-- require the use of an external SMT solver.+-----------------------------------------------------------------------------++-- Nothing needs to be changed in this file, add test cases+-- appropriately to SBVUnitTest.hs file, and they will be+-- picked up here automagically+module Main(main) where++import Control.Monad (unless, when)+import System.Directory (doesDirectoryExist)+import System.Exit (exitWith, exitSuccess, ExitCode(..))+import System.FilePath ((</>))+import System.IO (stderr, hPutStrLn)+import Test.HUnit (Test(..), Counts(..), runTestText, PutText(..), showCounts)++import Data.Version (showVersion)+import SBVTest (SBVTestSuite(..), generateGoldCheck)+import Paths_sbv (getDataDir, version)++import SBVTestCollection (allTestCases)+import SBVUnitTestBuildTime (buildTime)++testCollection :: [(String, SBVTestSuite)]+testCollection = [(n, s) | (n, False, s) <- allTestCases]++main :: IO ()+main = do putStrLn $ "*** SBVBasicTester, version: " ++ showVersion version ++ ", time stamp: " ++ buildTime+ d <- getDataDir + run $ d </> "SBVUnitTest" </> "GoldFiles"++checkGoldDir :: FilePath -> IO ()+checkGoldDir gd = do e <- doesDirectoryExist gd+ unless e $ do putStrLn "*** Cannot locate gold file repository!"+ putStrLn "*** Please call with one argument, the directory name of the gold files."+ putStrLn "*** Cannot run test cases, exiting."+ exitWith $ ExitFailure 1++run :: FilePath -> IO ()+run gd = do putStrLn $ "*** Starting SBV basic tests..\n*** Gold files at: " ++ show gd+ checkGoldDir gd+ (cts, _) <- runTestText (PutText put ()) $ TestList $ map (mkTst . snd) testCollection+ hPutStrLn stderr $ showCounts cts+ decide cts+ where mkTst (SBVTestSuite f) = f $ generateGoldCheck gd False+ put s _ st = length s `seq` return st++decide :: Counts -> IO ()+decide (Counts c t e f) = do+ when (c /= t) $ putStrLn $ "*** Not all test cases were tried. (Only tested " ++ show t ++ " of " ++ show c ++ ")"+ when (e /= 0) $ putStrLn $ "*** " ++ show e ++ " (of " ++ show c ++ ") test cases in error."+ when (f /= 0) $ putStrLn $ "*** " ++ show f ++ " (of " ++ show c ++ ") test cases failed."+ if c == t && e == 0 && f == 0+ then do putStrLn $ "All " ++ show c ++ " test cases successfully passed."+ exitSuccess+ else exitWith $ ExitFailure 2
+ SBVUnitTest/SBVTestCollection.hs view
@@ -0,0 +1,106 @@+-----------------------------------------------------------------------------+-- |+-- Module : Main+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- SBV test collection+-----------------------------------------------------------------------------++module SBVTestCollection(allTestCases) where++import SBVTest++-- To add a new collection of tests, import below and add to allTestCases variable+import qualified TestSuite.Arrays.Memory as T01_01(testSuite)+import qualified TestSuite.Basics.ArithNoSolver as T02_01(testSuite)+import qualified TestSuite.Basics.ArithSolver as T02_02(testSuite)+import qualified TestSuite.Basics.BasicTests as T02_03(testSuite)+import qualified TestSuite.Basics.Higher as T02_04(testSuite)+import qualified TestSuite.Basics.Index as T02_05(testSuite)+import qualified TestSuite.Basics.ProofTests as T02_06(testSuite)+import qualified TestSuite.Basics.QRem as T02_07(testSuite)+import qualified TestSuite.BitPrecise.BitTricks as T03_01(testSuite)+import qualified TestSuite.BitPrecise.Legato as T03_02(testSuite)+import qualified TestSuite.BitPrecise.MergeSort as T03_03(testSuite)+import qualified TestSuite.BitPrecise.PrefixSum as T03_04(testSuite)+import qualified TestSuite.CRC.CCITT as T04_01(testSuite)+import qualified TestSuite.CRC.CCITT_Unidir as T04_02(testSuite)+import qualified TestSuite.CRC.GenPoly as T04_03(testSuite)+import qualified TestSuite.CRC.Parity as T04_04(testSuite)+import qualified TestSuite.CRC.USB5 as T04_05(testSuite)+import qualified TestSuite.CodeGeneration.AddSub as T05_01(testSuite)+import qualified TestSuite.CodeGeneration.CgTests as T05_02(testSuite)+import qualified TestSuite.CodeGeneration.CRC_USB5 as T05_03(testSuite)+import qualified TestSuite.CodeGeneration.Fibonacci as T05_04(testSuite)+import qualified TestSuite.CodeGeneration.GCD as T05_05(testSuite)+import qualified TestSuite.CodeGeneration.PopulationCount as T05_06(testSuite)+import qualified TestSuite.CodeGeneration.Uninterpreted as T05_07(testSuite)+import qualified TestSuite.Crypto.AES as T06_01(testSuite)+import qualified TestSuite.Crypto.RC4 as T06_02(testSuite)+import qualified TestSuite.Existentials.CRCPolynomial as T07_01(testSuite)+import qualified TestSuite.Polynomials.Polynomials as T08_01(testSuite)+import qualified TestSuite.Puzzles.Coins as T09_01(testSuite)+import qualified TestSuite.Puzzles.Counts as T09_02(testSuite)+import qualified TestSuite.Puzzles.DogCatMouse as T09_03(testSuite)+import qualified TestSuite.Puzzles.Euler185 as T09_04(testSuite)+import qualified TestSuite.Puzzles.MagicSquare as T09_05(testSuite)+import qualified TestSuite.Puzzles.NQueens as T09_06(testSuite)+import qualified TestSuite.Puzzles.PowerSet as T09_07(testSuite)+import qualified TestSuite.Puzzles.Sudoku as T09_08(testSuite)+import qualified TestSuite.Puzzles.Temperature as T09_09(testSuite)+import qualified TestSuite.Puzzles.U2Bridge as T09_10(testSuite)+import qualified TestSuite.Uninterpreted.AUF as T10_01(testSuite)+import qualified TestSuite.Uninterpreted.Function as T10_02(testSuite)+import qualified TestSuite.Uninterpreted.Uninterpreted as T10_03(testSuite)++-- Bool says whether we need a real SMT solver to run this test+-- Note that it's ok to say True even if an SMT solver is *not*+-- needed, but we'd like most things to be targeted False so that+-- those tests can be run as part of cabal.+allTestCases :: [(String, Bool, SBVTestSuite)]+allTestCases = [+ ("mem", True, T01_01.testSuite)+ , ("arithCF", False, T02_01.testSuite)+ , ("arith", True, T02_02.testSuite)+ , ("basic", False, T02_03.testSuite)+ , ("higher", True, T02_04.testSuite)+ , ("index", True, T02_05.testSuite)+ , ("proof", True, T02_06.testSuite)+ , ("qrem", True, T02_07.testSuite)+ , ("bitTricks", True, T03_01.testSuite)+ , ("legato", False, T03_02.testSuite)+ , ("mergeSort", False, T03_03.testSuite)+ , ("prefixSum", True, T03_04.testSuite)+ , ("ccitt", False, T04_01.testSuite)+ , ("ccitt2", True, T04_02.testSuite)+ , ("genPoly", True, T04_03.testSuite)+ , ("parity", True, T04_04.testSuite)+ , ("usb5", True, T04_05.testSuite)+ , ("addSub", False, T05_01.testSuite)+ , ("cgtest", False, T05_02.testSuite)+ , ("cgUSB5", False, T05_03.testSuite)+ , ("fib", False, T05_04.testSuite)+ , ("gcd", False, T05_05.testSuite)+ , ("popCount", False, T05_06.testSuite)+ , ("cgUninterp", False, T05_07.testSuite)+ , ("aes", False, T06_01.testSuite)+ , ("rc4", True, T06_02.testSuite)+ , ("existPoly", False, T07_01.testSuite)+ , ("poly", True, T08_01.testSuite)+ , ("coins", False, T09_01.testSuite)+ , ("counts", False, T09_02.testSuite)+ , ("dogCatMouse", True, T09_03.testSuite)+ , ("euler185", True, T09_04.testSuite)+ , ("magicSquare", True, T09_05.testSuite)+ , ("nQueens", True, T09_06.testSuite)+ , ("powerset", True, T09_07.testSuite)+ , ("sudoku", True, T09_08.testSuite)+ , ("temperature", True, T09_09.testSuite)+ , ("u2bridge", True, T09_10.testSuite)+ , ("auf1", True, T10_01.testSuite)+ , ("auf2", True, T10_02.testSuite)+ , ("unint", True, T10_03.testSuite)+ ]
SBVUnitTest/SBVUnitTest.hs view
@@ -23,108 +23,19 @@ import Paths_sbv (getDataDir, version) import SBVUnitTestBuildTime (buildTime)---- To add a new collection of tests, import below and add to testCollection variable-import qualified TestSuite.Arrays.Memory as T01_01(testSuite)-import qualified TestSuite.Basics.Arithmetic as T02_01(testSuite)-import qualified TestSuite.Basics.BasicTests as T02_02(testSuite)-import qualified TestSuite.Basics.Higher as T02_03(testSuite)-import qualified TestSuite.Basics.Index as T02_04(testSuite)-import qualified TestSuite.Basics.ProofTests as T02_05(testSuite)-import qualified TestSuite.Basics.QRem as T02_06(testSuite)-import qualified TestSuite.BitPrecise.BitTricks as T03_01(testSuite)-import qualified TestSuite.BitPrecise.Legato as T03_02(testSuite)-import qualified TestSuite.BitPrecise.MergeSort as T03_03(testSuite)-import qualified TestSuite.BitPrecise.PrefixSum as T03_04(testSuite)-import qualified TestSuite.CRC.CCITT as T04_01(testSuite)-import qualified TestSuite.CRC.CCITT_Unidir as T04_02(testSuite)-import qualified TestSuite.CRC.GenPoly as T04_03(testSuite)-import qualified TestSuite.CRC.Parity as T04_04(testSuite)-import qualified TestSuite.CRC.USB5 as T04_05(testSuite)-import qualified TestSuite.CodeGeneration.AddSub as T05_01(testSuite)-import qualified TestSuite.CodeGeneration.CgTests as T05_02(testSuite)-import qualified TestSuite.CodeGeneration.CRC_USB5 as T05_03(testSuite)-import qualified TestSuite.CodeGeneration.Fibonacci as T05_04(testSuite)-import qualified TestSuite.CodeGeneration.GCD as T05_05(testSuite)-import qualified TestSuite.CodeGeneration.PopulationCount as T05_06(testSuite)-import qualified TestSuite.CodeGeneration.Uninterpreted as T05_07(testSuite)-import qualified TestSuite.Crypto.AES as T06_01(testSuite)-import qualified TestSuite.Crypto.RC4 as T06_02(testSuite)-import qualified TestSuite.Existentials.CRCPolynomial as T07_01(testSuite)-import qualified TestSuite.Polynomials.Polynomials as T08_01(testSuite)-import qualified TestSuite.Puzzles.Coins as T09_01(testSuite)-import qualified TestSuite.Puzzles.Counts as T09_02(testSuite)-import qualified TestSuite.Puzzles.DogCatMouse as T09_03(testSuite)-import qualified TestSuite.Puzzles.Euler185 as T09_04(testSuite)-import qualified TestSuite.Puzzles.MagicSquare as T09_05(testSuite)-import qualified TestSuite.Puzzles.NQueens as T09_06(testSuite)-import qualified TestSuite.Puzzles.PowerSet as T09_07(testSuite)-import qualified TestSuite.Puzzles.Sudoku as T09_08(testSuite)-import qualified TestSuite.Puzzles.Temperature as T09_09(testSuite)-import qualified TestSuite.Puzzles.U2Bridge as T09_10(testSuite)-import qualified TestSuite.Uninterpreted.AUF as T10_01(testSuite)-import qualified TestSuite.Uninterpreted.Function as T10_02(testSuite)-import qualified TestSuite.Uninterpreted.Uninterpreted as T10_03(testSuite)--testCollection :: [(String, SBVTestSuite)]-testCollection = [- ("mem", T01_01.testSuite)- , ("arith", T02_01.testSuite)- , ("basic", T02_02.testSuite)- , ("higher", T02_03.testSuite)- , ("index", T02_04.testSuite)- , ("proof", T02_05.testSuite)- , ("qrem", T02_06.testSuite)- , ("bitTricks", T03_01.testSuite)- , ("legato", T03_02.testSuite)- , ("mergeSort", T03_03.testSuite)- , ("prefixSum", T03_04.testSuite)- , ("ccitt", T04_01.testSuite)- , ("ccitt2", T04_02.testSuite)- , ("genPoly", T04_03.testSuite)- , ("parity", T04_04.testSuite)- , ("usb5", T04_05.testSuite)- , ("addSub", T05_01.testSuite)- , ("cgtest", T05_02.testSuite)- , ("cgUSB5", T05_03.testSuite)- , ("fib", T05_04.testSuite)- , ("gcd", T05_05.testSuite)- , ("popCount", T05_06.testSuite)- , ("cgUninterp", T05_07.testSuite)- , ("aes", T06_01.testSuite)- , ("rc4", T06_02.testSuite)- , ("existPoly", T07_01.testSuite)- , ("poly", T08_01.testSuite)- , ("coins", T09_01.testSuite)- , ("counts", T09_02.testSuite)- , ("dogCatMouse", T09_03.testSuite)- , ("euler185", T09_04.testSuite)- , ("magicSquare", T09_05.testSuite)- , ("nQueens", T09_06.testSuite)- , ("powerset", T09_07.testSuite)- , ("sudoku", T09_08.testSuite)- , ("temperature", T09_09.testSuite)- , ("u2bridge", T09_10.testSuite)- , ("auf1", T10_01.testSuite)- , ("auf2", T10_02.testSuite)- , ("unint", T10_03.testSuite)- ]---- No user serviceable parts below..+import SBVTestCollection (allTestCases) main :: IO () main = do putStrLn $ "*** SBVUnitTester, version: " ++ showVersion version ++ ", time stamp: " ++ buildTime tgts <- getArgs case tgts of [x] | x `elem` ["-h", "--help", "-?"]- -> putStrLn "Usage: SBVUnitTests [-l] [targets]" -- Not quite right, but sufficient+ -> putStrLn "Usage: SBVUnitTests [-l(ist)] [-s(kipCF)] [targets]" -- Not quite right, but sufficient ["-l"] -> showTargets -- undocumented really- ("-c":ts) -> createGolds (unwords ts)- _ -> run tgts False []--createGolds :: String -> IO ()-createGolds tgts = run (words tgts) True ["SBVUnitTest/GoldFiles"]+ ("-c":ts) -> run ts False True ["SBVUnitTest/GoldFiles"]+ ("-s":ts) -> run ts True False []+ _ -> run tgts False False [] checkGoldDir :: FilePath -> IO () checkGoldDir gd = do e <- doesDirectoryExist gd@@ -134,26 +45,31 @@ exitWith $ ExitFailure 1 allTargets :: [String]-allTargets = map fst testCollection+allTargets = [s | (s, _, _) <- allTestCases] showTargets :: IO () showTargets = do putStrLn "Known test targets are:" mapM_ (putStrLn . ("\t" ++)) allTargets -run :: [String] -> Bool -> [String] -> IO ()-run targets shouldCreate [gd] =+run :: [String] -> Bool -> Bool -> [String] -> IO ()+run targets skipCF shouldCreate [gd] = do mapM_ checkTgt targets putStrLn $ "*** Starting SBV unit tests..\n*** Gold files at: " ++ show gd checkGoldDir gd- cts <- runTestTT $ TestList $ map mkTst [c | (tc, c) <- testCollection, select tc]+ cts <- runTestTT $ TestList $ map mkTst [c | (tc, needsSolver, c) <- allTestCases, select needsSolver tc] decide shouldCreate cts where mkTst (SBVTestSuite f) = f $ generateGoldCheck gd shouldCreate- select tc = null targets || tc `elem` targets+ select needsSolver tc+ | not included = False+ | shouldCreate = True+ | needsSolver = True+ | True = not skipCF+ where included = null targets || tc `elem` targets checkTgt t | t `elem` allTargets = return () | True = do putStrLn $ "*** Unknown test target: " ++ show t exitWith $ ExitFailure 1-run targets shouldCreate [] = getDataDir >>= \d -> run targets shouldCreate [d </> "SBVUnitTest" </> "GoldFiles"]-run _ _ _ = error "SBVUnitTests.run: impossible happened!"+run targets skipCF shouldCreate [] = getDataDir >>= \d -> run targets skipCF shouldCreate [d </> "SBVUnitTest" </> "GoldFiles"]+run _ _ _ _ = error "SBVUnitTests.run: impossible happened!" decide :: Bool -> Counts -> IO () decide shouldCreate (Counts c t e f) = do
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Thu Jul 19 22:00:35 PDT 2012"+buildTime = "Thu Oct 18 20:24:21 PDT 2012"
+ SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs view
@@ -0,0 +1,287 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Basics.ArithNoSolver+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test suite for basic concrete arithmetic, i.e., testing all+-- the constant folding based arithmetic implementation in SBV+-----------------------------------------------------------------------------++{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TupleSections #-}++module TestSuite.Basics.ArithNoSolver(testSuite) where++import Data.SBV++import SBVTest++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \_ -> test $+ genReals+ ++ genQRems+ ++ genBinTest "+" (+)+ ++ genBinTest "-" (-)+ ++ genBinTest "*" (*)+ ++ genUnTest "negate" negate+ ++ genUnTest "abs" abs+ ++ genUnTest "signum" signum+ ++ genBinTest ".&." (.&.)+ ++ genBinTest ".|." (.|.)+ ++ genBoolTest "<" (<) (.<)+ ++ genBoolTest "<=" (<=) (.<=)+ ++ genBoolTest ">" (>) (.>)+ ++ genBoolTest ">=" (>=) (.>=)+ ++ genBoolTest "==" (==) (.==)+ ++ genBoolTest "/=" (/=) (./=)+ ++ genBinTest "xor" xor+ ++ genUnTest "complement" complement+ ++ genIntTest "shift" shift+ ++ genIntTest "rotate" rotate+ ++ genIntTestS "setBit" setBit+ ++ genIntTestS "clearBit" clearBit+ ++ genIntTestS "complementBit" complementBit+ ++ genIntTest "shift" shift+ ++ genIntTestS "shiftL" shiftL+ ++ genIntTestS "shiftR" shiftR+ ++ genIntTest "rotate" rotate+ ++ genIntTestS "rotateL" rotateL+ ++ genIntTestS "rotateR" rotateR+ ++ genBlasts+ ++ genCasts++genBinTest :: String -> (forall 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]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `op` y | x <- sw32s, y <- sw32s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `op` y | x <- sw64s, y <- sw64s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `op` y | x <- si8s, y <- si8s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `op` y | x <- si16s, y <- si16s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `op` y | x <- si32s, y <- si32s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `op` y | x <- si64s, y <- si64s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `op` y | x <- siUBs, y <- siUBs]+ where pair (x, y, a) b = (x, y, show (fromIntegral a `asTypeOf` b) == show b)+ mkTest (x, y, s) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"++genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test]+genBoolTest nm op opS = map mkTest $+ zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `opS` y | x <- sw8s, y <- sw8s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `opS` y | x <- sw16s, y <- sw16s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `opS` y | x <- sw32s, y <- sw32s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `opS` y | x <- sw64s, y <- sw64s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `opS` y | x <- si8s, y <- si8s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `opS` y | x <- si16s, y <- si16s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `opS` y | x <- si32s, y <- si32s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `opS` y | x <- si64s, y <- si64s]+ ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `opS` y | x <- siUBs, y <- siUBs]+ 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 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]+ ++ zipWith pair [(show x, op x) | x <- w32s] [op x | x <- sw32s]+ ++ zipWith pair [(show x, op x) | x <- w64s] [op x | x <- sw64s]+ ++ zipWith pair [(show x, op x) | x <- i8s ] [op x | x <- si8s ]+ ++ zipWith pair [(show x, op x) | x <- i16s] [op x | x <- si16s]+ ++ zipWith pair [(show x, op x) | x <- i32s] [op x | x <- si32s]+ ++ zipWith pair [(show x, op x) | x <- i64s] [op x | x <- si64s]+ ++ zipWith pair [(show x, op x) | x <- iUBs] [op x | x <- siUBs]+ 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 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]+ ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- is] [x `op` y | x <- sw32s, y <- is]+ ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- is] [x `op` y | x <- sw64s, y <- is]+ ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- is] [x `op` y | x <- si8s, y <- is]+ ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- is] [x `op` y | x <- si16s, y <- is]+ ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- is] [x `op` y | x <- si32s, y <- is]+ ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- is] [x `op` y | x <- si64s, y <- is]+ ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- is] [x `op` y | x <- siUBs, y <- is]+ where pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)+ 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 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)]]+ ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (bitSize x - 1)]]+ ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (bitSize x - 1)]]+ ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si8s, y <- [0 .. (bitSize x - 1)]]+ ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (bitSize x - 1)]]+ ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (bitSize x - 1)]]+ ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (bitSize x - 1)]]+ ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]] [x `op` y | x <- siUBs, y <- [0 .. 10 ]]+ where pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)+ mkTest (t, x, y, a, b, s) = "arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"++genBlasts :: [Test]+genBlasts = map mkTest $+ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw8s ]+ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw8s ]+ ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si8s ]+ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si8s ]+ ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw16s]+ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw16s]+ ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si16s]+ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si16s]+ ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw32s]+ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw32s]+ ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si32s]+ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si32s]+ ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw64s]+ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw64s]+ ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si64s]+ ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si64s]+ where mkTest (x, r) = "blast-" ++ show x ~: r `showsAs` "True"++genCasts :: [Test]+genCasts = map mkTest $+ [(show x, unsignCast (signCast x) .== x) | x <- sw8s ]+ ++ [(show x, unsignCast (signCast x) .== x) | x <- sw16s]+ ++ [(show x, unsignCast (signCast x) .== x) | x <- sw32s]+ ++ [(show x, unsignCast (signCast x) .== x) | x <- sw64s]+ ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ]+ ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s]+ ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ]+ ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s]+ ++ [(show x, signCast (unsignCast x) .== x) | x <- si32s]+ ++ [(show x, signCast (unsignCast x) .== x) | x <- si64s]+ ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw8s ]+ ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw16s]+ ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw32s]+ ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw64s]+ ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si8s ]+ ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si16s]+ ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si32s]+ ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si64s]+ where mkTest (x, r) = "cast-" ++ show x ~: r `showsAs` "True"++genQRems :: [Test]+genQRems = map mkTest $+ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- w8s, y <- w8s ] [x `sDivMod` y | x <- sw8s, y <- sw8s ]+ ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- w16s, y <- w16s] [x `sDivMod` y | x <- sw16s, y <- sw16s]+ ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- w32s, y <- w32s] [x `sDivMod` y | x <- sw32s, y <- sw32s]+ ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- w64s, y <- w64s] [x `sDivMod` y | x <- sw64s, y <- sw64s]+ ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i8s, y <- i8s , noOverflow x y] [x `sDivMod` y | x <- si8s, y <- si8s , noOverflow x y]+ ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i16s, y <- i16s, noOverflow x y] [x `sDivMod` y | x <- si16s, y <- si16s, noOverflow x y]+ ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i32s, y <- i32s, noOverflow x y] [x `sDivMod` y | x <- si32s, y <- si32s, noOverflow x y]+ ++ (if divModInt64Bug -- see below+ then []+ else zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i64s, y <- i64s, noOverflow x y] [x `sDivMod` y | x <- si64s, y <- si64s, noOverflow x y]+ )+ ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- iUBs, y <- iUBs] [x `sDivMod` y | x <- siUBs, y <- siUBs]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w8s, y <- w8s ] [x `sQuotRem` y | x <- sw8s, y <- sw8s ]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w16s, y <- w16s] [x `sQuotRem` y | x <- sw16s, y <- sw16s]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w32s, y <- w32s] [x `sQuotRem` y | x <- sw32s, y <- sw32s]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w64s, y <- w64s] [x `sQuotRem` y | x <- sw64s, y <- sw64s]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- i8s, y <- i8s , noOverflow x y] [x `sQuotRem` y | x <- si8s, y <- si8s , noOverflow x y]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- i16s, y <- i16s, noOverflow x y] [x `sQuotRem` y | x <- si16s, y <- si16s, noOverflow x y]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- i32s, y <- i32s, noOverflow x y] [x `sQuotRem` y | x <- si32s, y <- si32s, noOverflow x y]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- i64s, y <- i64s, noOverflow x y] [x `sQuotRem` y | x <- si64s, y <- si64s, noOverflow x y]+ ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- iUBs, y <- iUBs] [x `sQuotRem` y | x <- siUBs, y <- siUBs]+ where divMod' x y = if y == 0 then (0, x) else x `divMod` y+ quotRem' x y = if y == 0 then (0, x) else x `quotRem` y+ pair (nm, x, y, (r1, r2)) (e1, e2) = (nm, x, y, show (fromIntegral r1 `asTypeOf` e1, fromIntegral r2 `asTypeOf` e2) == show (e1, e2))+ mkTest (nm, x, y, s) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"+ -- Haskell's divMod and quotRem overflows if x == minBound and y == -1 for bounded signed types; so avoid that case+ noOverflow x y = not (x == minBound && y == -1)++genReals :: [Test]+genReals = map mkTest $+ map ("+",) (zipWith pair [(show x, show y, x + y) | x <- rs, y <- rs ] [x + y | x <- srs, y <- srs ])+ ++ map ("-",) (zipWith pair [(show x, show y, x - y) | x <- rs, y <- rs ] [x - y | x <- srs, y <- srs ])+ ++ map ("*",) (zipWith pair [(show x, show y, x * y) | x <- rs, y <- rs ] [x * y | x <- srs, y <- srs ])+ ++ map ("<",) (zipWith pair [(show x, show y, x < y) | x <- rs, y <- rs ] [x .< y | x <- srs, y <- srs ])+ ++ map ("<=",) (zipWith pair [(show x, show y, x <= y) | x <- rs, y <- rs ] [x .<= y | x <- srs, y <- srs ])+ ++ map (">",) (zipWith pair [(show x, show y, x > y) | x <- rs, y <- rs ] [x .> y | x <- srs, y <- srs ])+ ++ map (">=",) (zipWith pair [(show x, show y, x >= y) | x <- rs, y <- rs ] [x .>= y | x <- srs, y <- srs ])+ ++ map ("==",) (zipWith pair [(show x, show y, x == y) | x <- rs, y <- rs ] [x .== y | x <- srs, y <- srs ])+ ++ map ("/=",) (zipWith pair [(show x, show y, x /= y) | x <- rs, y <- rs ] [x ./= y | x <- srs, y <- srs ])+ ++ map ("/",) (zipWith pair [(show x, show y, x / y) | x <- rs, y <- rs, y /= 0] [x / y | x <- srs, y <- srs, unliteral y /= Just 0])+ where pair (x, y, a) b = (x, y, Just a == unliteral b)+ mkTest (nm, (x, y, s)) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"++-- Concrete test data+xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a]+xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound)+xsSigned = xsUnsigned ++ [-5 .. 5]++w8s :: [Word8]+w8s = xsUnsigned++sw8s :: [SWord8]+sw8s = xsUnsigned++w16s :: [Word16]+w16s = xsUnsigned++sw16s :: [SWord16]+sw16s = xsUnsigned++w32s :: [Word32]+w32s = xsUnsigned++sw32s :: [SWord32]+sw32s = xsUnsigned++w64s :: [Word64]+w64s = xsUnsigned++sw64s :: [SWord64]+sw64s = xsUnsigned++i8s :: [Int8]+i8s = xsSigned++si8s :: [SInt8]+si8s = xsSigned++i16s :: [Int16]+i16s = xsSigned++si16s :: [SInt16]+si16s = xsSigned++i32s :: [Int32]+i32s = xsSigned++si32s :: [SInt32]+si32s = xsSigned++i64s :: [Int64]+i64s = xsSigned++si64s :: [SInt64]+si64s = xsSigned++iUBs :: [Integer]+iUBs = [-1000000 .. -999995] ++ [-5 .. 5] ++ [999995 .. 1000000]++siUBs :: [SInteger]+siUBs = map literal iUBs++rs :: [AlgReal]+rs = [fromRational (i % d) | i <- is, d <- ds]+ where is = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 .. 1000001]+ ds = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000]++srs :: [SReal]+srs = map literal rs+++-- On 32 bit installations of GHC, divMod is buggy for Int64+-- Thus causing our tests to fail. See ticket: http://hackage.haskell.org/trac/ghc/ticket/7233+-- Luckily, it's easy to detect it and sidestep it until GHC is appropriately patched+divModInt64Bug :: Bool+divModInt64Bug = (1 `div` (minBound::Int64)) /= -1 -- Bug causes this expression to evaluate to 1
+ SBVUnitTest/TestSuite/Basics/ArithSolver.hs view
@@ -0,0 +1,270 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Basics.ArithSolver+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test suite for basic non-concrete arithmetic, i.e., testing all+-- basic arithmetic reasoning using an SMT solver without any+-- constant folding.+-----------------------------------------------------------------------------++{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TupleSections #-}++module TestSuite.Basics.ArithSolver(testSuite) where++import Data.SBV++import SBVTest++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \_ -> test $+ genReals+ ++ genQRems+ ++ genBinTest True "+" (+)+ ++ genBinTest True "-" (-)+ ++ genBinTest True "*" (*)+ ++ genUnTest True "negate" negate+ ++ genUnTest True "abs" abs+ ++ genUnTest True "signum" signum+ ++ genBinTest False ".&." (.&.)+ ++ genBinTest False ".|." (.|.)+ ++ genBoolTest "<" (<) (.<)+ ++ genBoolTest "<=" (<=) (.<=)+ ++ genBoolTest ">" (>) (.>)+ ++ genBoolTest ">=" (>=) (.>=)+ ++ genBoolTest "==" (==) (.==)+ ++ genBoolTest "/=" (/=) (./=)+ ++ genBinTest False "xor" xor+ ++ genUnTest False "complement" complement+ ++ genIntTest "shift" shift+ ++ genIntTest "rotate" rotate+ ++ genIntTestS False "setBit" setBit+ ++ genIntTestS False "clearBit" clearBit+ ++ genIntTestS False "complementBit" complementBit+ ++ genIntTest "shift" shift+ ++ genIntTestS True "shiftL" shiftL+ ++ genIntTestS True "shiftR" shiftR+ ++ genIntTest "rotate" rotate+ ++ genIntTestS True "rotateL" rotateL+ ++ genIntTestS True "rotateR" rotateR+ ++ genBlasts+ ++ genCasts+++genBinTest :: Bool -> String -> (forall 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]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- i8s ]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs]+ where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]+ constrain $ a .== literal x+ constrain $ b .== literal y+ return $ literal r .== a `op` b++genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test]+genBoolTest nm op opS = 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]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- i8s ]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s]+ ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- iUBs]+ where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]+ constrain $ a .== literal x+ constrain $ b .== literal y+ return $ literal r .== a `opS` b++genUnTest :: Bool -> String -> (forall 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]+ ++ [(show x, mkThm x (op x)) | x <- w64s]+ ++ [(show x, mkThm x (op x)) | x <- i8s ]+ ++ [(show x, mkThm x (op x)) | x <- i16s]+ ++ [(show x, mkThm x (op x)) | x <- i32s]+ ++ [(show x, mkThm x (op x)) | x <- i64s]+ ++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs]+ where mkTest (x, t) = "arithmetic-" ++ nm ++ "." ++ x ~: assert t+ mkThm x r = isTheorem $ do a <- free "x"+ constrain $ a .== literal x+ return $ literal r .== op a++genIntTest :: String -> (forall 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]+ ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- is]+ ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- is]+ ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- is]+ ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- is]+ ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- is]+ ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- is]+ where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t+ is = [-10 .. 10]+ mkThm2 x y r = isTheorem $ do a <- free "x"+ constrain $ a .== literal x+ return $ literal r .== a `op` y+++genIntTestS :: Bool -> String -> (forall 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)]]+ ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- [0 .. (bitSize x - 1)]]+ ++ [("s8", show x, show y, mkThm2 x y (x `op` y)) | x <- i8s, y <- [0 .. (bitSize x - 1)]]+ ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- [0 .. (bitSize x - 1)]]+ ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- [0 .. (bitSize x - 1)]]+ ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (bitSize x - 1)]]+ ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- [0 .. 10]]+ where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t+ mkThm2 x y r = isTheorem $ do a <- free "x"+ constrain $ a .== literal x+ return $ literal r .== a `op` y++genBlasts :: [Test]+genBlasts = map mkTest $ [(show x, mkThm fromBitsLE blastLE x) | x <- w8s ]+ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w8s ]+ ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i8s ]+ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i8s ]+ ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w16s]+ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w16s]+ ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i16s]+ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i16s]+ ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w32s]+ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w32s]+ ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i32s]+ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i32s]+ ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w64s]+ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w64s]+ ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i64s]+ ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i64s]+ where mkTest (x, t) = "blast-" ++ show x ~: assert t+ mkThm from to v = isTheorem $ do a <- free "x"+ constrain $ a .== literal v+ return $ a .== from (to a)++genCasts :: [Test]+genCasts = map mkTest $ [(show x, mkThm unsignCast signCast x) | x <- w8s ]+ ++ [(show x, mkThm unsignCast signCast x) | x <- w16s]+ ++ [(show x, mkThm unsignCast signCast x) | x <- w32s]+ ++ [(show x, mkThm unsignCast signCast x) | x <- w64s]+ ++ [(show x, mkThm signCast unsignCast x) | x <- i8s ]+ ++ [(show x, mkThm signCast unsignCast x) | x <- i16s]+ ++ [(show x, mkThm signCast unsignCast x) | x <- i8s ]+ ++ [(show x, mkThm signCast unsignCast x) | x <- i16s]+ ++ [(show x, mkThm signCast unsignCast x) | x <- i32s]+ ++ [(show x, mkThm signCast unsignCast x) | x <- i64s]+ ++ [(show x, mkFEq signCast (fromBitsLE . blastLE) x) | x <- w8s ]+ ++ [(show x, mkFEq signCast (fromBitsLE . blastLE) x) | x <- w16s]+ ++ [(show x, mkFEq signCast (fromBitsLE . blastLE) x) | x <- w32s]+ ++ [(show x, mkFEq signCast (fromBitsLE . blastLE) x) | x <- w64s]+ ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i8s ]+ ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i16s]+ ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i32s]+ ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i64s]+ where mkTest (x, t) = "cast-" ++ show x ~: assert t+ mkThm from to v = isTheorem $ do a <- free "x"+ constrain $ a .== literal v+ return $ a .== from (to a)+ mkFEq f g v = isTheorem $ do a <- free "x"+ constrain $ a .== literal v+ return $ f a .== g a++genReals :: [Test]+genReals = map mkTest $ [("+", show x, show y, mkThm2 (+) x y (x + y)) | x <- rs, y <- rs ]+ ++ [("-", show x, show y, mkThm2 (-) x y (x - y)) | x <- rs, y <- rs ]+ ++ [("*", show x, show y, mkThm2 (*) x y (x * y)) | x <- rs, y <- rs ]+ ++ [("/", show x, show y, mkThm2 (/) x y (x / y)) | x <- rs, y <- rs, y /= 0]+ ++ [("<", show x, show y, mkThm2 (.<) x y (x < y)) | x <- rs, y <- rs ]+ ++ [("<=", show x, show y, mkThm2 (.<=) x y (x <= y)) | x <- rs, y <- rs ]+ ++ [(">", show x, show y, mkThm2 (.>) x y (x > y)) | x <- rs, y <- rs ]+ ++ [(">=", show x, show y, mkThm2 (.>=) x y (x >= y)) | x <- rs, y <- rs ]+ ++ [("==", show x, show y, mkThm2 (.==) x y (x == y)) | x <- rs, y <- rs ]+ ++ [("/=", show x, show y, mkThm2 (./=) x y (x /= y)) | x <- rs, y <- rs ]+ where mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ mkThm2 op x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]+ constrain $ a .== literal x+ constrain $ b .== literal y+ return $ literal r .== a `op` b++genQRems :: [Test]+genQRems = map mkTest $ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w8s, y <- w8s ]+ ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w16s, y <- w16s]+ ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w32s, y <- w32s]+ ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- w64s, y <- w64s]+ ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- i8s, y <- i8s , noOverflow x y]+ ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- i16s, y <- i16s, noOverflow x y]+ ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- i32s, y <- i32s, noOverflow x y]+ ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- i64s, y <- i64s, noOverflow x y]+ ++ [("divMod", show x, show y, mkThm2 sDivMod x y (x `divMod'` y)) | x <- iUBs, y <- iUBs]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w8s, y <- w8s ]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w16s, y <- w16s]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w32s, y <- w32s]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w64s, y <- w64s]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i8s, y <- i8s , noOverflow x y]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i16s, y <- i16s, noOverflow x y]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i32s, y <- i32s, noOverflow x y]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i64s, y <- i64s, noOverflow x y]+ ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- iUBs, y <- iUBs]+ where divMod' x y = if y == 0 then (0, x) else x `divMod` y+ quotRem' x y = if y == 0 then (0, x) else x `quotRem` y+ mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: assert t+ mkThm2 op x y (e1, e2) = isTheorem $ do [a, b] <- mapM free ["x", "y"]+ constrain $ a .== literal x+ constrain $ b .== literal y+ return $ (literal e1, literal e2) .== a `op` b+ -- Haskell's divMod and quotRem overflows if x == minBound and y == -1 for signed types; so avoid that case+ noOverflow x y = not (x == minBound && y == -1)++-- Concrete test data+xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a]+xsUnsigned = [minBound, 0, maxBound]+xsSigned = xsUnsigned ++ [-1, 1]++w8s :: [Word8]+w8s = xsUnsigned++w16s :: [Word16]+w16s = xsUnsigned++w32s :: [Word32]+w32s = xsUnsigned++w64s :: [Word64]+w64s = xsUnsigned++i8s :: [Int8]+i8s = xsSigned++i16s :: [Int16]+i16s = xsSigned++i32s :: [Int32]+i32s = xsSigned++i64s :: [Int64]+i64s = xsSigned++iUBs :: [Integer]+iUBs = [-1000000] ++ [-1 .. 1] ++ [1000000]++rs :: [AlgReal]+rs = [fromRational (i % d) | i <- is, d <- ds]+ where is = [-1000000] ++ [-1 .. 1] ++ [10000001]+ ds = [5,100,1000000]++{-# ANN module "HLint: ignore Reduce duplication" #-}
− SBVUnitTest/TestSuite/Basics/Arithmetic.hs
@@ -1,248 +0,0 @@--------------------------------------------------------------------------------- |--- Module : TestSuite.Basics.Arithmetic--- Copyright : (c) Levent Erkok--- License : BSD3--- Maintainer : erkokl@gmail.com--- Stability : experimental------ Test suite for basic concrete arithmetic--------------------------------------------------------------------------------{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE TupleSections #-}--module TestSuite.Basics.Arithmetic(testSuite) where--import Data.SBV--import SBVTest---- Test suite-testSuite :: SBVTestSuite-testSuite = mkTestSuite $ \_ -> test $- genReals- ++ genBinTest "+" (+)- ++ genBinTest "-" (-)- ++ genBinTest "*" (*)- ++ genUnTest "negate" negate- ++ genUnTest "abs" abs- ++ genUnTest "signum" signum- ++ genBinTest ".&." (.&.)- ++ genBinTest ".|." (.|.)- ++ genBoolTest "<" (<) (.<)- ++ genBoolTest "<=" (<=) (.<=)- ++ genBoolTest ">" (>) (.>)- ++ genBoolTest ">=" (>=) (.>=)- ++ genBoolTest "==" (==) (.==)- ++ genBoolTest "/=" (/=) (./=)- ++ genBinTest "xor" xor- ++ genUnTest "complement" complement- ++ genIntTest "shift" shift- ++ genIntTest "rotate" rotate- ++ genIntTestS "setBit" setBit- ++ genIntTestS "clearBit" clearBit- ++ genIntTestS "complementBit" complementBit- ++ genIntTest "shift" shift- ++ genIntTestS "shiftL" shiftL- ++ genIntTestS "shiftR" shiftR- ++ genIntTest "rotate" rotate- ++ genIntTestS "rotateL" rotateL- ++ genIntTestS "rotateR" rotateR- ++ genBlasts- ++ genCasts--genBinTest :: String -> (forall 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]- ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `op` y | x <- sw32s, y <- sw32s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `op` y | x <- sw64s, y <- sw64s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `op` y | x <- si8s, y <- si8s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `op` y | x <- si16s, y <- si16s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `op` y | x <- si32s, y <- si32s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `op` y | x <- si64s, y <- si64s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `op` y | x <- siUBs, y <- siUBs]- where pair (x, y, a) b = (x, y, show (fromIntegral a `asTypeOf` b) == show b)- mkTest (x, y, s) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"--genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test]-genBoolTest nm op opS = map mkTest $- zipWith pair [(show x, show y, x `op` y) | x <- w8s, y <- w8s ] [x `opS` y | x <- sw8s, y <- sw8s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `opS` y | x <- sw16s, y <- sw16s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `opS` y | x <- sw32s, y <- sw32s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `opS` y | x <- sw64s, y <- sw64s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s, y <- i8s ] [x `opS` y | x <- si8s, y <- si8s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `opS` y | x <- si16s, y <- si16s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `opS` y | x <- si32s, y <- si32s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `opS` y | x <- si64s, y <- si64s]- ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `opS` y | x <- siUBs, y <- siUBs]- where pair (x, y, a) b = (x, y, Just a == unliteral b)- mkTest (x, y, s) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"--genUnTest :: String -> (forall 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]- ++ zipWith pair [(show x, op x) | x <- w32s] [op x | x <- sw32s]- ++ zipWith pair [(show x, op x) | x <- w64s] [op x | x <- sw64s]- ++ zipWith pair [(show x, op x) | x <- i8s ] [op x | x <- si8s ]- ++ zipWith pair [(show x, op x) | x <- i16s] [op x | x <- si16s]- ++ zipWith pair [(show x, op x) | x <- i32s] [op x | x <- si32s]- ++ zipWith pair [(show x, op x) | x <- i64s] [op x | x <- si64s]- ++ zipWith pair [(show x, op x) | x <- iUBs] [op x | x <- siUBs]- where pair (x, a) b = (x, show (fromIntegral a `asTypeOf` b) == show b)- mkTest (x, s) = "arithmetic-" ++ nm ++ "." ++ x ~: s `showsAs` "True"--genIntTest :: String -> (forall 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]- ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- is] [x `op` y | x <- sw32s, y <- is]- ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- is] [x `op` y | x <- sw64s, y <- is]- ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- is] [x `op` y | x <- si8s, y <- is]- ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- is] [x `op` y | x <- si16s, y <- is]- ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- is] [x `op` y | x <- si32s, y <- is]- ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- is] [x `op` y | x <- si64s, y <- is]- ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- is] [x `op` y | x <- siUBs, y <- is]- where pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)- mkTest (t, x, y, a, b, s) = "arithmetic-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"- is = [-10 .. 10]--genIntTestS :: String -> (forall 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)]]- ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("s8", show x, show y, x `op` y) | x <- i8s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si8s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (bitSize x - 1)]]- ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]] [x `op` y | x <- siUBs, y <- [0 .. 10 ]]- where pair (t, x, y, a) b = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)- mkTest (t, x, y, a, b, s) = "arithmetic-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"--genBlasts :: [Test]-genBlasts = map mkTest $- [(show x, fromBitsLE (blastLE x) .== x) | x <- sw8s ]- ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw8s ]- ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si8s ]- ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si8s ]- ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw16s]- ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw16s]- ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si16s]- ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si16s]- ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw32s]- ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw32s]- ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si32s]- ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si32s]- ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw64s]- ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw64s]- ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si64s]- ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si64s]- where mkTest (x, r) = "blast-" ++ show x ~: r `showsAs` "True"--genCasts :: [Test]-genCasts = map mkTest $- [(show x, unsignCast (signCast x) .== x) | x <- sw8s ]- ++ [(show x, unsignCast (signCast x) .== x) | x <- sw16s]- ++ [(show x, unsignCast (signCast x) .== x) | x <- sw32s]- ++ [(show x, unsignCast (signCast x) .== x) | x <- sw64s]- ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ]- ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s]- ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ]- ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s]- ++ [(show x, signCast (unsignCast x) .== x) | x <- si32s]- ++ [(show x, signCast (unsignCast x) .== x) | x <- si64s]- ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw8s ]- ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw16s]- ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw32s]- ++ [(show x, signCast x .== fromBitsLE (blastLE x)) | x <- sw64s]- ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si8s ]- ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si16s]- ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si32s]- ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si64s]- where mkTest (x, r) = "cast-" ++ show x ~: r `showsAs` "True"--genReals :: [Test]-genReals = map mkTest $- map ("+",) (zipWith pair [(show x, show y, x + y) | x <- rs, y <- rs ] [x + y | x <- srs, y <- srs ])- ++ map ("-",) (zipWith pair [(show x, show y, x - y) | x <- rs, y <- rs ] [x - y | x <- srs, y <- srs ])- ++ map ("*",) (zipWith pair [(show x, show y, x * y) | x <- rs, y <- rs ] [x * y | x <- srs, y <- srs ])- ++ map ("<",) (zipWith pair [(show x, show y, x < y) | x <- rs, y <- rs ] [x .< y | x <- srs, y <- srs ])- ++ map ("<=",) (zipWith pair [(show x, show y, x <= y) | x <- rs, y <- rs ] [x .<= y | x <- srs, y <- srs ])- ++ map (">",) (zipWith pair [(show x, show y, x > y) | x <- rs, y <- rs ] [x .> y | x <- srs, y <- srs ])- ++ map (">=",) (zipWith pair [(show x, show y, x >= y) | x <- rs, y <- rs ] [x .>= y | x <- srs, y <- srs ])- ++ map ("==",) (zipWith pair [(show x, show y, x == y) | x <- rs, y <- rs ] [x .== y | x <- srs, y <- srs ])- ++ map ("/=",) (zipWith pair [(show x, show y, x /= y) | x <- rs, y <- rs ] [x ./= y | x <- srs, y <- srs ])- ++ map ("/",) (zipWith pair [(show x, show y, x / y) | x <- rs, y <- rs, y /= 0] [x / y | x <- srs, y <- srs, unliteral y /= Just 0])- where pair (x, y, a) b = (x, y, Just a == unliteral b)- mkTest (nm, (x, y, s)) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True"---- Concrete test data-xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a]-xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound)-xsSigned = xsUnsigned ++ [-5 .. 5]--w8s :: [Word8]-w8s = xsUnsigned--sw8s :: [SWord8]-sw8s = xsUnsigned--w16s :: [Word16]-w16s = xsUnsigned--sw16s :: [SWord16]-sw16s = xsUnsigned--w32s :: [Word32]-w32s = xsUnsigned--sw32s :: [SWord32]-sw32s = xsUnsigned--w64s :: [Word64]-w64s = xsUnsigned--sw64s :: [SWord64]-sw64s = xsUnsigned--i8s :: [Int8]-i8s = xsSigned--si8s :: [SInt8]-si8s = xsSigned--i16s :: [Int16]-i16s = xsSigned--si16s :: [SInt16]-si16s = xsSigned--i32s :: [Int32]-i32s = xsSigned--si32s :: [SInt32]-si32s = xsSigned--i64s :: [Int64]-i64s = xsSigned--si64s :: [SInt64]-si64s = xsSigned--iUBs :: [Integer]-iUBs = [-1000000 .. -999995] ++ [-5 .. 5] ++ [999995 .. 1000000]--siUBs :: [SInteger]-siUBs = map literal iUBs--rs :: [AlgReal]-rs = [fromRational (i % d) | i <- is, d <- ds]- where is = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 .. 1000001]- ds = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000]--srs :: [SReal]-srs = map literal rs
SBVUnitTest/TestSuite/Basics/QRem.hs view
@@ -19,5 +19,7 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test [- "qrem" ~: assert =<< isTheorem (qrem :: SWord8 -> SWord8 -> SBool)+ "qremW8" ~: assert =<< isTheorem (qrem :: SWord8 -> SWord8 -> SBool)+ , "qremI8" ~: assert =<< isTheorem (qrem :: SInt8 -> SInt8 -> SBool)+ , "qremI" ~: assert =<< isTheorem (qrem :: SInteger -> SInteger -> SBool) ]
SBVUnitTest/TestSuite/Puzzles/Temperature.hs view
@@ -19,5 +19,5 @@ -- Test suite testSuite :: SBVTestSuite testSuite = mkTestSuite $ \goldCheck -> test [- "temperature" ~: sat (revOf `fmap` exists_) `goldCheck` "temperature.gold"+ "temperature" ~: allSat (revOf `fmap` exists_) `goldCheck` "temperature.gold" ]
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 2.3+Version: 2.4 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@@ -15,8 +15,10 @@ > Falsifiable. Counter-example: > x = 128 :: SWord8 .- The library introduces the following types and concepts:+ The SBV library uses Microsoft's Z3 SMT solver (<http://research.microsoft.com/en-us/um/redmond/projects/z3/>) as the default underlying solver. It is also possible to use SRI's Yices SMT solver with SBV as well (<http://yices.csl.sri.com/download-yices2.shtml>), although the Z3 binding is much more richer. .+ SBV introduces the following types and concepts:+ . * 'SBool': Symbolic Booleans (bits) . * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned)@@ -115,22 +117,8 @@ TypeOperators TypeSynonymInstances Build-Depends : base >= 4 && < 5- -- Be careful with versions of packages that come with "latest" GHC,- -- need to update this as new GHC releases incorporate new packages- , array == 0.4.0.0- , containers == 0.4.2.1- , deepseq == 1.3.0.0- , directory == 1.1.0.2- , filepath == 1.3.0.0- , old-time == 1.1.0.0- , pretty == 1.1.1.0- , process == 1.1.0.1- -- following are pure hackage packages, thus we can be more relaxed- , mtl >= 2.1.2- , QuickCheck >= 2.5- , random >= 1.0.1.1- , strict-concurrency >= 0.2.4.1- , syb >= 0.3.7+ , array, containers, deepseq, directory, filepath, old-time+ , pretty, process, mtl, QuickCheck, random, strict-concurrency, syb Exposed-modules : Data.SBV , Data.SBV.Internals , Data.SBV.Examples.BitPrecise.BitTricks@@ -192,20 +180,13 @@ RankNTypes ScopedTypeVariables TupleSections- Build-depends : base >= 4 && < 5- -- Be careful with versions of packages that come with "latest" GHC,- -- need to update this as new GHC releases incorporate new packages- , directory == 1.1.0.2- , filepath == 1.3.0.0- , process == 1.1.0.1- -- apparently HUnit 1.2.5.0 has some cabal issues..- , HUnit == 1.2.4.3- -- self dependence on sbv- , sbv+ Build-depends : base >= 4 && < 5+ , HUnit, directory, filepath, process, sbv Hs-Source-Dirs : SBVUnitTest main-is : SBVUnitTest.hs Other-modules : SBVUnitTestBuildTime , SBVTest+ , SBVTestCollection , Examples.Arrays.Memory , Examples.Basics.BasicTests , Examples.Basics.Higher@@ -221,7 +202,8 @@ , Examples.Puzzles.Temperature , Examples.Uninterpreted.Uninterpreted , TestSuite.Arrays.Memory- , TestSuite.Basics.Arithmetic+ , TestSuite.Basics.ArithNoSolver+ , TestSuite.Basics.ArithSolver , TestSuite.Basics.BasicTests , TestSuite.Basics.Higher , TestSuite.Basics.Index@@ -260,3 +242,14 @@ , TestSuite.Uninterpreted.AUF , TestSuite.Uninterpreted.Function , TestSuite.Uninterpreted.Uninterpreted++Test-Suite SBVBasicTests+ type : exitcode-stdio-1.0+ default-language: Haskell2010+ ghc-options : -Wall+ Build-depends : base >= 4 && < 5+ , HUnit, directory, filepath, sbv+ Hs-Source-Dirs : SBVUnitTest+ main-is : SBVBasicTests.hs+ Other-modules : SBVBasicTests+ , SBVTestCollection