diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,18 @@ * Hackage: * GitHub: -* 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 diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -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 diff --git a/Data/SBV/BitVectors/Concrete.hs b/Data/SBV/BitVectors/Concrete.hs --- a/Data/SBV/BitVectors/Concrete.hs +++ b/Data/SBV/BitVectors/Concrete.hs @@ -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 diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -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) ++ ">" diff --git a/Data/SBV/BitVectors/Symbolic.hs b/Data/SBV/BitVectors/Symbolic.hs --- a/Data/SBV/BitVectors/Symbolic.hs +++ b/Data/SBV/BitVectors/Symbolic.hs @@ -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 diff --git a/Data/SBV/Examples/Uninterpreted/Deduce.hs b/Data/SBV/Examples/Uninterpreted/Deduce.hs --- a/Data/SBV/Examples/Uninterpreted/Deduce.hs +++ b/Data/SBV/Examples/Uninterpreted/Deduce.hs @@ -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 diff --git a/Data/SBV/Examples/Uninterpreted/Sort.hs b/Data/SBV/Examples/Uninterpreted/Sort.hs --- a/Data/SBV/Examples/Uninterpreted/Sort.hs +++ b/Data/SBV/Examples/Uninterpreted/Sort.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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) diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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 diff --git a/SBVUnitTest/SBVTest.hs b/SBVUnitTest/SBVTest.hs --- a/SBVUnitTest/SBVTest.hs +++ b/SBVUnitTest/SBVTest.hs @@ -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 diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Sat Oct 29 10:15:43 PDT 2016" +buildTime = "Thu Jan 12 09:52:42 PST 2017" diff --git a/SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs b/SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs --- a/SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs +++ b/SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs @@ -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 diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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: -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