sbv 2.1 → 2.2

raw patch · 10 files changed

+48/−37 lines, 10 filesdep ~QuickCheckdep ~arraydep ~containers

Dependency ranges changed: QuickCheck, array, containers, deepseq, directory, filepath, mtl, old-time, pretty, process, syb

Files

• Data/SBV/BitVectors/Data.hs +1/−1
• Data/SBV/BitVectors/Model.hs +9/−9
• Data/SBV/BitVectors/STree.hs +1/−1
• Data/SBV/SMT/SMT.hs +1/−1
• Data/SBV/SMT/SMTLib1.hs +1/−1
• Data/SBV/Tools/Optimize.hs +3/−3
• Data/SBV/Tools/Polynomial.hs +5/−5
• RELEASENOTES +9/−1
• SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
• sbv.cabal +17/−14

@@ -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

@@ -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"

@@ -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)

@@ -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) 

@@ -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

@@ -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 (.<=) 

@@ -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.

@@ -1,7 +1,15 @@ Hackage: <http://hackage.haskell.org/package/sbv> GitHub:  <http://github.com/LeventErkok/sbv> -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

@@ -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"

@@ -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