sbv 5.13 → 5.14

raw patch · 13 files changed

+40/−23 lines, 13 filesdep ~QuickCheck

Dependency ranges changed: QuickCheck

Files

• CHANGES.md +12/−1
• COPYRIGHT +1/−1
• Data/SBV/BitVectors/Concrete.hs +1/−1
• Data/SBV/BitVectors/Data.hs +1/−1
• Data/SBV/BitVectors/Symbolic.hs +3/−3
• Data/SBV/Examples/Uninterpreted/Deduce.hs +1/−1
• Data/SBV/Examples/Uninterpreted/Sort.hs +1/−1
• Data/SBV/SMT/SMTLib2.hs +12/−6
• LICENSE +1/−1
• SBVUnitTest/SBVTest.hs +1/−1
• SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
• SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs +1/−1
• sbv.cabal +4/−4

@@ -1,7 +1,18 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub:  <http://leventerkok.github.com/sbv/> -* Latest Hackage released version: 5.13, 2016-10-29+* Latest Hackage released version: 5.14, 2017-01-12++### Version 5.14, 2017-01-12+  +  * Bump up QuickCheck dependency to >= 2.9.2 to avoid the following quick-check+    bug http://github.com/nick8325/quickcheck/issues/113, which transitively impacted+    the quick-check as implemented by SBV.++  * Generalize casts between integral-floats, using the rounding mode round-nearest-ties-to-even.+    Previously calls to sFromIntegral did not support conversion to floats since it needed+    a rounding mode. But it does make sense to support them with the default mode. If a different+    mode is needed, use the function 'toSFloat' as before, which takes an explicit rounding mode.  ### Version 5.13, 2016-10-29 

@@ -1,4 +1,4 @@-Copyright (c) 2010-2016, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2017, Levent Erkok (erkokl@gmail.com) All rights reserved.  The sbv library is distributed with the BSD3 license. See the LICENSE file

@@ -112,7 +112,7 @@ trueCW :: CW trueCW  = CW KBool (CWInteger 1) --- | Lift a unary function thruough a CW+-- | Lift a unary function through a CW liftCW :: (AlgReal -> b) -> (Integer -> b) -> (Float -> b) -> (Double -> b) -> ((Maybe Int, String) -> b) -> CW -> b liftCW f _ _ _ _ (CW _ (CWAlgReal v))  = f v liftCW _ f _ _ _ (CW _ (CWInteger v))  = f v

@@ -428,7 +428,7 @@ -- --    * Typically faster as it gets compiled away during translation ---data SFunArray a b = SFunArray (SBV a -> SBV b)+newtype SFunArray a b = SFunArray (SBV a -> SBV b)  instance (HasKind a, HasKind b) => Show (SFunArray a b) where   show (SFunArray _) = "SFunArray<" ++ showType (undefined :: a) ++ ":" ++ showType (undefined :: b) ++ ">"

@@ -103,11 +103,11 @@ forceSWArg :: SW -> IO () forceSWArg (SW k n) = k `seq` n `seq` return () --- | Constant False as a SW. Note that this value always occupies slot -2.+-- | Constant False as an SW. Note that this value always occupies slot -2. falseSW :: SW falseSW = SW KBool $ NodeId (-2) --- | Constant False as a SW. Note that this value always occupies slot -1.+-- | Constant True as an SW. Note that this value always occupies slot -1. trueSW :: SW trueSW  = SW KBool $ NodeId (-1) @@ -1072,7 +1072,7 @@   show = show . solver  -- | A model, as returned by a solver-data SMTModel = SMTModel {+newtype SMTModel = SMTModel {         modelAssocs    :: [(String, CW)]        -- ^ Mapping of symbolic values to constants.      }      deriving Show

@@ -29,7 +29,7 @@  -- | The uninterpreted sort 'B', corresponding to the carrier. -- To prevent SBV from translating it to an enumerated type, we simply attach an unused field-data B = B () deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind)+newtype B = B () deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind)  -- | Handy shortcut for the type of symbolic values over 'B' type SB = SBV B

@@ -21,7 +21,7 @@ -- in the backend SMT solver. Note the custom @deriving@ clause, which -- takes care of most of the boilerplate. The () field is needed so -- SBV will not translate it to an enumerated data-type-data Q = Q () deriving (Eq, Ord, Data, Read, Show, SymWord, HasKind)+newtype Q = Q () deriving (Eq, Ord, Data, Read, Show, SymWord, HasKind)  -- | Declare an uninterpreted function that works over Q's f :: SBV Q -> SBV Q

@@ -531,7 +531,7 @@ -----------------------------------------------------------------------------------------------  handleFPCast :: Kind -> Kind -> String -> String -> String-handleFPCast kFrom kTo rm  input+handleFPCast kFrom kTo rm input   | kFrom == kTo   = input   | True@@ -592,20 +592,26 @@       KBounded s m -> case kTo of                         KBounded _ n -> fromBV (if s then signExtend else zeroExtend) m n                         KUnbounded   -> b2i s m-                        _            -> noCast+                        _            -> tryFPCast        KUnbounded   -> case kTo of                         KReal        -> "(to_real " ++ a ++ ")"                         KBounded _ n -> i2b n-                        _            -> noCast+                        _            -> tryFPCast        KReal        -> case kTo of                         KUnbounded   -> "(to_int " ++ a ++ ")"-                        _            -> noCast+                        _            -> tryFPCast -      _            -> noCast+      _            -> tryFPCast -  where noCast  = error $ "SBV.SMTLib2: Unexpected cast from: " ++ show kFrom ++ " to " ++ show kTo+  where -- See if we can push this down to a float-cast, using sRNE. This happens if one of the kinds is a float/double.+        -- Otherwise complain+        tryFPCast+          | any (\k -> isFloat k || isDouble k) [kFrom, kTo]+          = handleFPCast kFrom kTo (smtRoundingMode RoundNearestTiesToEven) a+          | True+          = error $ "SBV.SMTLib2: Unexpected cast from: " ++ show kFrom ++ " to " ++ show kTo          fromBV upConv m n          | n > m  = upConv  (n - m)

@@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2016, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2017, Levent Erkok (erkokl@gmail.com) All rights reserved.  Redistribution and use in source and binary forms, with or without

@@ -25,7 +25,7 @@ import Test.HUnit              (Test(..), Assertion, assert, (~:), test)  -- | A Test-suite, parameterized by the gold-check generator/checker-data SBVTestSuite = SBVTestSuite ((forall a. Show a => (IO a -> FilePath -> IO ())) -> Test)+newtype SBVTestSuite = SBVTestSuite ((forall a. Show a => (IO a -> FilePath -> IO ())) -> Test)  -- | Wrap over 'SBVTestSuite', avoids exporting the constructor mkTestSuite :: ((forall a. (Show a) => IO a -> FilePath -> IO ()) -> Test) -> SBVTestSuite

@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where  buildTime :: String-buildTime = "Sat Oct 29 10:15:43 PDT 2016"+buildTime = "Thu Jan 12 09:52:42 PST 2017"

@@ -25,7 +25,7 @@  ]  -- Example provided by Thomas DuBuisson:-data Bitstring = Bitstring () deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind)+newtype Bitstring = Bitstring () deriving (Eq, Ord, Show, Read, Data, SymWord, HasKind) type SBitstring = SBV Bitstring  a :: SBitstring -> SBool

@@ -1,5 +1,5 @@ Name:          sbv-Version:       5.13+Version:       5.14 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@@ -7,7 +7,7 @@                .                For details, please see: <http://leventerkok.github.com/sbv/> -Copyright:     Levent Erkok, 2010-2016+Copyright:     Levent Erkok, 2010-2017 License:       BSD3 License-file:  LICENSE Stability:     Experimental@@ -48,9 +48,9 @@   Build-Depends   : base >= 4.8 && < 5                   , base-compat >= 0.6                   , ghc+                  , QuickCheck >= 2.9.2                   , array, async, containers, deepseq, directory, filepath, old-time-                  , pretty, process, mtl, QuickCheck, random, syb, data-binary-ieee754-                  , crackNum+                  , pretty, process, mtl, random, syb, data-binary-ieee754, crackNum   Exposed-modules : Data.SBV                   , Data.SBV.Bridge.Boolector                   , Data.SBV.Bridge.CVC4