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 @@ -1111,8 +1111,8 @@ instance NFData Kind instance NFData ArrayContext -instance NFData Pgm instance NFData SW +instance NFData SBVExpr instance NFData Quantifier instance NFData SBVType instance NFData UnintKind diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -516,21 +516,21 @@ | y == falseSW = Just x | True = Nothing --- | Returns (symbolic) true if all the elements of the given list are different +-- | Returns (symbolic) true if all the elements of the given list are different. allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBool allDifferent (x:xs@(_:_)) = bAll ((./=) x) xs &&& allDifferent xs allDifferent _ = true --- | Returns (symbolic) true if all the elements of the given list are the same +-- | Returns (symbolic) true if all the elements of the given list are the same. allEqual :: (Eq a, SymWord a) => [SBV a] -> SBool allEqual (x:xs@(_:_)) = bAll ((.==) x) xs allEqual _ = true --- | Returns 1 if the boolean is true, otherwise 0 +-- | Returns 1 if the boolean is true, otherwise 0. oneIf :: (Num a, SymWord a) => SBool -> SBV a oneIf t = ite t 1 0 --- Num instance for symbolic words +-- Num instance for symbolic words. instance (Ord a, Num a, SymWord a) => Num (SBV a) where fromInteger = literal . fromIntegral x + y @@ -641,7 +641,7 @@ -- number is 2^256-1, which is a pretty darn big number to worry about for practical -- purposes. In any case, we do not support 'sbvPopCount' for unbounded symbolic integers, -- as the only possible implementation wouldn't symbolically terminate. So the only overflow --- issue is with really-really large concrete 'SInteger' values +-- issue is with really-really large concrete 'SInteger' values. sbvPopCount :: (Bits a, SymWord a) => SBV a -> SWord8 sbvPopCount x | isReal x = error "SBV.sbvPopCount: Called on a real value" @@ -658,22 +658,22 @@ setBitTo :: (Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a setBitTo x i b = ite b (setBit x i) (clearBit x i) --- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class +-- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class. blastLE :: (Bits a, SymWord a) => SBV a -> [SBool] blastLE x | isReal x = error "SBV.blastLE: Called on a real value" | not (isBounded x) = error "SBV.blastLE: Called on an infinite precision value" | True = map (sbvTestBit x) [0 .. (intSizeOf x)-1] --- | Big-endian blasting of a word into its bits. Also see the 'FromBits' class +-- | Big-endian blasting of a word into its bits. Also see the 'FromBits' class. blastBE :: (Bits a, SymWord a) => SBV a -> [SBool] blastBE = reverse . blastLE --- | Least significant bit of a word, always stored at index 0 +-- | Least significant bit of a word, always stored at index 0. lsb :: (Bits a, SymWord a) => SBV a -> SBool lsb x = sbvTestBit x 0 --- | Most significant bit of a word, always stored at the last position +-- | Most significant bit of a word, always stored at the last position. msb :: (Bits a, SymWord a) => SBV a -> SBool msb x | isReal x = error "SBV.msb: Called on a real value" diff --git a/Data/SBV/BitVectors/STree.hs b/Data/SBV/BitVectors/STree.hs --- a/Data/SBV/BitVectors/STree.hs +++ b/Data/SBV/BitVectors/STree.hs @@ -57,7 +57,7 @@ walk (b:bs) (SBin l r) = SBin (ite b l (walk bs l)) (ite b (walk bs r) r) walk _ _ = error $ "SBV.STree.writeSTree: Impossible happened while reading: " ++ show i --- | Construct the fully balanced initial tree using the given values +-- | Construct the fully balanced initial tree using the given values. mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e mkSTree ivals | isReal (undefined :: i) diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -174,7 +174,7 @@ genParse k (x@(CW _ (CWInteger i)):r) | kindOf x == k = Just (fromIntegral i, r) genParse _ _ = Nothing --- | Base case, that comes in handy if there are no real variables +-- Base case, that comes in handy if there are no real variables instance SatModel () where parseCWs xs = return ((), xs) diff --git a/Data/SBV/SMT/SMTLib1.hs b/Data/SBV/SMT/SMTLib1.hs --- a/Data/SBV/SMT/SMTLib1.hs +++ b/Data/SBV/SMT/SMTLib1.hs @@ -102,7 +102,7 @@ ++ [mkFormula isSat out] ++ [")"] asgns = F.toList asgnsSeq - mkCstr s = ":assumption (= " ++ show s ++ " bv1[1])" + mkCstr s = " :assumption (= " ++ show s ++ " bv1[1])" -- TODO: Does this work for SMT-Lib when the index/element types are signed? -- Currently we ignore the signedness of the arguments, as there appears to be no way diff --git a/Data/SBV/Tools/Optimize.hs b/Data/SBV/Tools/Optimize.hs --- a/Data/SBV/Tools/Optimize.hs +++ b/Data/SBV/Tools/Optimize.hs @@ -41,11 +41,11 @@ optimizeWith cfg (Iterative chatty) = iterOptimize chatty cfg optimizeWith cfg Quantified = quantOptimize cfg --- | Variant of 'optimizeWith' using the default solver +-- | Variant of 'optimizeWith' using the default solver. See 'optimizeWith' for parameter descriptions. optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> (SBV c -> SBV c -> SBool) -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) optimize = optimizeWith defaultSMTCfg --- | Variant of 'maximize' allowing the use of a user specified solver. +-- | Variant of 'maximize' allowing the use of a user specified solver. See 'optimizeWith' for parameter descriptions. maximizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) maximizeWith cfg opts = optimizeWith cfg opts (.>=) @@ -56,7 +56,7 @@ maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) maximize = maximizeWith defaultSMTCfg --- | Variant of 'minimize' allowing the use of a user specified solver. +-- | Variant of 'minimize' allowing the use of a user specified solver. See 'optimizeWith' for parameter descriptions. minimizeWith :: (SatModel a, SymWord a, Show a, SymWord c, Show c) => SMTConfig -> OptimizeOpts -> ([SBV a] -> SBV c) -> Int -> ([SBV a] -> SBool) -> IO (Maybe [a]) minimizeWith cfg opts = optimizeWith cfg opts (.<=) diff --git a/Data/SBV/Tools/Polynomial.hs b/Data/SBV/Tools/Polynomial.hs --- a/Data/SBV/Tools/Polynomial.hs +++ b/Data/SBV/Tools/Polynomial.hs @@ -43,7 +43,7 @@ -- will evaluate to @11@, since it sets the bits @0@, @1@, and @3@. Mathematicans would write this polynomial -- as @x^3 + x + 1@. And in fact, 'showPoly' will show it like that. polynomial :: [Int] -> a - -- | Add two polynomials in GF(2^n) + -- | Add two polynomials in GF(2^n). pAdd :: a -> a -> a -- | Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by -- the polynomial as specified by coefficients of the third argument. Note that the third @@ -55,13 +55,13 @@ -- Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't -- fit into the resulting size. pMult :: (a, a, [Int]) -> a - -- | Divide two polynomials in GF(2^n), see above note for division by 0 + -- | Divide two polynomials in GF(2^n), see above note for division by 0. pDiv :: a -> a -> a - -- | Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0 + -- | Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0. pMod :: a -> a -> a - -- | Division and modulus packed together + -- | Division and modulus packed together. pDivMod :: a -> a -> (a, a) - -- | Display a polynomial like a mathematician would (over the monomial @x@), with a type + -- | Display a polynomial like a mathematician would (over the monomial @x@), with a type. showPoly :: a -> String -- | Display a polynomial like a mathematician would (over the monomial @x@), the first argument -- controls if the final type is shown as well. diff --git a/RELEASENOTES b/RELEASENOTES --- a/RELEASENOTES +++ b/RELEASENOTES @@ -1,7 +1,15 @@ Hackage: GitHub: -Latest Hackage released version: 2.1 +Latest Hackage released version: 2.2 + +====================================================================== +Version 2.2, 2012-07-17 + + - Maintanence release, no new features. + - Update cabal dependencies, in particular fix the + regression with respect to latest version of the + containers package. ====================================================================== Version 2.1, 2012-05-24 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 = "Wed May 23 20:53:39 PDT 2012" +buildTime = "Mon Jul 16 22:55:32 PDT 2012" diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,5 +1,5 @@ Name: sbv -Version: 2.1 +Version: 2.2 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 @@ -83,7 +83,7 @@ Bug-reports: http://github.com/LeventErkok/sbv/issues Maintainer: Levent Erkok (erkokl@gmail.com) Build-Type: Simple -Cabal-Version: >= 1.8 +Cabal-Version: >= 1.14 Data-Files: SBVUnitTest/GoldFiles/*.gold Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES @@ -92,10 +92,12 @@ location: git://github.com/LeventErkok/sbv.git Library + default-language: Haskell2010 ghc-options : -Wall other-extensions: BangPatterns CPP - -- DefaultSignatures flag is not present in cabal 1.14.0; so ignore for the time being + -- Currently commented out since Cabal doesn't yet recognize DefaultSignatures extension yet. Uncomment when it does. + -- The current list can be seen at: https://github.com/haskell/cabal/blob/master/Cabal/Language/Haskell/Extension.hs -- DefaultSignatures DeriveDataTypeable FlexibleContexts @@ -112,20 +114,20 @@ TupleSections TypeOperators TypeSynonymInstances - Build-Depends : array >= 0.3.0.1 + Build-Depends : array >= 0.4.0.0 , base >= 3 && < 5 - , containers >= 0.3.0.0 - , deepseq >= 1.1.0.2 - , directory >= 1.0.1.1 - , filepath >= 1.1.0.4 - , mtl >= 2.0.1.0 - , old-time >= 1.0.0.5 - , pretty >= 1.0.1.1 - , process >= 1.0.1.3 - , QuickCheck >= 2.4.0.1 + , containers >= 0.5.0.0 + , deepseq >= 1.3.0.0 + , directory >= 1.1.0.2 + , filepath >= 1.3.0.0 + , mtl >= 2.1.2 + , old-time >= 1.1.0.0 + , pretty >= 1.1.1.0 + , process >= 1.1.0.1 + , QuickCheck >= 2.5 , random >= 1.0.1.1 , strict-concurrency >= 0.2.4.1 - , syb >= 0.3.6 + , syb >= 0.3.7 Exposed-modules : Data.SBV , Data.SBV.Internals , Data.SBV.Examples.BitPrecise.BitTricks @@ -181,6 +183,7 @@ , Data.SBV.Utils.Lib Executable SBVUnitTests + default-language: Haskell2010 ghc-options : -Wall other-extensions: Rank2Types RankNTypes