Cabal revisions of sbv-1.2
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-Name: sbv-Version: 1.2-Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT-Synopsis: Symbolic bit vectors: Bit-precise verification and automatic C-code generation.-Description: Express properties about bit-precise Haskell programs and automatically prove- them using SMT solvers. Automatically generate C programs from Haskell functions.- The SBV library adds support for symbolic bit vectors, allowing formal models of- bit-precise programs to be created.- .- > $ ghci -XScopedTypeVariables- > Prelude> :m Data.SBV- > Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x- > Q.E.D.- > Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x- > Falsifiable. Counter-example:- > x = 128 :: SWord8- .- The library introduces the following types and concepts:- .- * 'SBool': Symbolic Booleans (bits)- .- * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned)- .- * 'SInt8', 'SInt16', 'SInt32', 'SInt64': Symbolic Ints (signed)- .- * 'SInteger': Symbolic unbounded integers (signed)- .- * 'SArray', 'SFunArray': Flat arrays of symbolic values- .- * 'STree': Full binary trees of symbolic values (for fast symbolic access)- .- * Symbolic polynomials over GF(2^n), and polynomial arithmetic- .- * Uninterpreted constants and functions over symbolic values, with user- defined SMT-Lib axioms- .- Functions built out of these types can be:- .- * 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 existential variables)- .- * 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- languages, including Haskell and C.- .- Predicates can have both existential and universal variables. Use of- alternating quantifiers provides considerable expressive power.- Furthermore, existential variables allow synthesis via model generation.- .- The SBV library can also compile Haskell functions that manipulate symbolic- values directly to C, rendering them as straight-line C programs.- .- In addition to the library, the installation will create the- executable @SBVUnitTests@. You should run it once the installation is complete,- to make sure the unit tests are run and all is well.- .- SBV is hosted at GitHub: <http://github.com/LeventErkok/sbv>. Comments,- bug reports, and patches are always welcome.- .- The following people reported bugs, provided comments/feedback, or contributed to the- development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki,- Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann.- .- Release notes can be seen at: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>.--Copyright: Levent Erkok, 2010-2012-License: BSD3-License-file: LICENSE-Stability: Experimental-Author: Levent Erkok-Homepage: http://github.com/LeventErkok/sbv-Bug-reports: http://github.com/LeventErkok/sbv/issues-Maintainer: Levent Erkok (erkokl@gmail.com)-Build-Type: Simple-Cabal-Version: >= 1.6-Data-Files: SBVUnitTest/GoldFiles/*.gold-Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES--source-repository head- type: git- location: git://github.com/LeventErkok/sbv.git--Library- ghc-options : -Wall- Build-Depends : array >= 0.3.0.1- , 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- , random >= 1.0.1.1- , strict-concurrency >= 0.2.4.1- Exposed-modules : Data.SBV- , Data.SBV.Internals- , Data.SBV.Examples.BitPrecise.BitTricks- , Data.SBV.Examples.BitPrecise.Legato- , Data.SBV.Examples.BitPrecise.PrefixSum- , Data.SBV.Examples.CodeGeneration.AddSub- , Data.SBV.Examples.CodeGeneration.CRC_USB5- , Data.SBV.Examples.CodeGeneration.Fibonacci- , Data.SBV.Examples.CodeGeneration.GCD- , Data.SBV.Examples.CodeGeneration.PopulationCount- , Data.SBV.Examples.CodeGeneration.Uninterpreted- , Data.SBV.Examples.Crypto.AES- , Data.SBV.Examples.Crypto.RC4- , Data.SBV.Examples.Existentials.CRCPolynomial- , Data.SBV.Examples.Polynomials.Polynomials- , Data.SBV.Examples.Puzzles.Coins- , Data.SBV.Examples.Puzzles.Counts- , Data.SBV.Examples.Puzzles.DogCatMouse- , Data.SBV.Examples.Puzzles.Euler185- , Data.SBV.Examples.Puzzles.MagicSquare- , Data.SBV.Examples.Puzzles.NQueens- , Data.SBV.Examples.Puzzles.Sudoku- , Data.SBV.Examples.Puzzles.U2Bridge- , Data.SBV.Examples.Uninterpreted.AUF- , Data.SBV.Examples.Uninterpreted.Function- Other-modules : Data.SBV.BitVectors.Data- , Data.SBV.BitVectors.Model- , Data.SBV.BitVectors.PrettyNum- , Data.SBV.BitVectors.SignCast- , Data.SBV.BitVectors.Splittable- , Data.SBV.BitVectors.STree- , Data.SBV.Compilers.C- , Data.SBV.Compilers.CodeGen- , Data.SBV.SMT.SMT- , Data.SBV.SMT.SMTLib- , Data.SBV.SMT.SMTLib1- , Data.SBV.SMT.SMTLib2- , Data.SBV.Provers.Prover- , Data.SBV.Provers.SExpr- , Data.SBV.Provers.Yices- , Data.SBV.Provers.Z3- , Data.SBV.Tools.ExpectedValue- , Data.SBV.Tools.GenTest- , Data.SBV.Tools.Optimize- , Data.SBV.Tools.Polynomial- , Data.SBV.Utils.Boolean- , Data.SBV.Utils.TDiff- , Data.SBV.Utils.Lib--Executable SBVUnitTests- ghc-options : -Wall- Build-depends : base >= 3 && < 5- , directory >= 1.0.1.1- , HUnit >= 1.2.4.2- , filepath >= 1.1.0.4- , process >= 1.0.1.3- Hs-Source-Dirs : SBVUnitTest, .- main-is : SBVUnitTest.hs- Other-modules : SBVUnitTestBuildTime- , SBVTest- , Examples.Arrays.Memory- , Examples.Basics.BasicTests- , Examples.Basics.Higher- , Examples.Basics.Index- , Examples.Basics.ProofTests- , Examples.Basics.QRem- , Examples.CRC.CCITT- , Examples.CRC.CCITT_Unidir- , Examples.CRC.GenPoly- , Examples.CRC.Parity- , Examples.CRC.USB5- , Examples.Puzzles.PowerSet- , Examples.Puzzles.Temperature- , Examples.Uninterpreted.Uninterpreted- , TestSuite.Arrays.Memory- , TestSuite.Basics.Arithmetic- , TestSuite.Basics.BasicTests- , TestSuite.Basics.Higher- , TestSuite.Basics.Index- , TestSuite.Basics.ProofTests- , TestSuite.Basics.QRem- , TestSuite.BitPrecise.BitTricks- , TestSuite.BitPrecise.Legato- , TestSuite.BitPrecise.PrefixSum- , TestSuite.CodeGeneration.AddSub- , TestSuite.CodeGeneration.CgTests- , TestSuite.CodeGeneration.CRC_USB5- , TestSuite.CodeGeneration.Fibonacci- , TestSuite.CodeGeneration.GCD- , TestSuite.CodeGeneration.PopulationCount- , TestSuite.CodeGeneration.Uninterpreted- , TestSuite.Crypto.AES- , TestSuite.Crypto.RC4- , TestSuite.Existentials.CRCPolynomial- , TestSuite.CRC.CCITT- , TestSuite.CRC.CCITT_Unidir- , TestSuite.CRC.GenPoly- , TestSuite.CRC.Parity- , TestSuite.CRC.USB5- , TestSuite.Puzzles.Coins- , TestSuite.Polynomials.Polynomials- , TestSuite.Puzzles.Counts- , TestSuite.Puzzles.DogCatMouse- , TestSuite.Puzzles.Euler185- , TestSuite.Puzzles.MagicSquare- , TestSuite.Puzzles.NQueens- , TestSuite.Puzzles.PowerSet- , TestSuite.Puzzles.Sudoku- , TestSuite.Puzzles.U2Bridge- , TestSuite.Puzzles.Temperature- , TestSuite.Uninterpreted.AUF- , TestSuite.Uninterpreted.Function- , TestSuite.Uninterpreted.Uninterpreted+Name: sbv +Version: 1.2 +x-revision: 1 +Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT +Synopsis: Symbolic bit vectors: Bit-precise verification and automatic C-code generation. +Description: Express properties about bit-precise Haskell programs and automatically prove + them using SMT solvers. Automatically generate C programs from Haskell functions. + The SBV library adds support for symbolic bit vectors, allowing formal models of + bit-precise programs to be created. + . + > $ ghci -XScopedTypeVariables + > Prelude> :m Data.SBV + > Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x + > Q.E.D. + > Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x + > Falsifiable. Counter-example: + > x = 128 :: SWord8 + . + The library introduces the following types and concepts: + . + * 'SBool': Symbolic Booleans (bits) + . + * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned) + . + * 'SInt8', 'SInt16', 'SInt32', 'SInt64': Symbolic Ints (signed) + . + * 'SInteger': Symbolic unbounded integers (signed) + . + * 'SArray', 'SFunArray': Flat arrays of symbolic values + . + * 'STree': Full binary trees of symbolic values (for fast symbolic access) + . + * Symbolic polynomials over GF(2^n), and polynomial arithmetic + . + * Uninterpreted constants and functions over symbolic values, with user + defined SMT-Lib axioms + . + Functions built out of these types can be: + . + * 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 existential variables) + . + * 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 + languages, including Haskell and C. + . + Predicates can have both existential and universal variables. Use of + alternating quantifiers provides considerable expressive power. + Furthermore, existential variables allow synthesis via model generation. + . + The SBV library can also compile Haskell functions that manipulate symbolic + values directly to C, rendering them as straight-line C programs. + . + In addition to the library, the installation will create the + executable @SBVUnitTests@. You should run it once the installation is complete, + to make sure the unit tests are run and all is well. + . + SBV is hosted at GitHub: <http://github.com/LeventErkok/sbv>. Comments, + bug reports, and patches are always welcome. + . + The following people reported bugs, provided comments/feedback, or contributed to the + development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, + Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and Nis Wegmann. + . + Release notes can be seen at: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>. + +Copyright: Levent Erkok, 2010-2012 +License: BSD3 +License-file: LICENSE +Stability: Experimental +Author: Levent Erkok +Homepage: http://github.com/LeventErkok/sbv +Bug-reports: http://github.com/LeventErkok/sbv/issues +Maintainer: Levent Erkok (erkokl@gmail.com) +Build-Type: Simple +Cabal-Version: >= 1.6 +Data-Files: SBVUnitTest/GoldFiles/*.gold +Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES + +source-repository head + type: git + location: git://github.com/LeventErkok/sbv.git + +Library + ghc-options : -Wall + Build-Depends : array >= 0.3.0.1 + , base >= 3 && < 4.8 + , 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 + , random >= 1.0.1.1 + , strict-concurrency >= 0.2.4.1 + Exposed-modules : Data.SBV + , Data.SBV.Internals + , Data.SBV.Examples.BitPrecise.BitTricks + , Data.SBV.Examples.BitPrecise.Legato + , Data.SBV.Examples.BitPrecise.PrefixSum + , Data.SBV.Examples.CodeGeneration.AddSub + , Data.SBV.Examples.CodeGeneration.CRC_USB5 + , Data.SBV.Examples.CodeGeneration.Fibonacci + , Data.SBV.Examples.CodeGeneration.GCD + , Data.SBV.Examples.CodeGeneration.PopulationCount + , Data.SBV.Examples.CodeGeneration.Uninterpreted + , Data.SBV.Examples.Crypto.AES + , Data.SBV.Examples.Crypto.RC4 + , Data.SBV.Examples.Existentials.CRCPolynomial + , Data.SBV.Examples.Polynomials.Polynomials + , Data.SBV.Examples.Puzzles.Coins + , Data.SBV.Examples.Puzzles.Counts + , Data.SBV.Examples.Puzzles.DogCatMouse + , Data.SBV.Examples.Puzzles.Euler185 + , Data.SBV.Examples.Puzzles.MagicSquare + , Data.SBV.Examples.Puzzles.NQueens + , Data.SBV.Examples.Puzzles.Sudoku + , Data.SBV.Examples.Puzzles.U2Bridge + , Data.SBV.Examples.Uninterpreted.AUF + , Data.SBV.Examples.Uninterpreted.Function + Other-modules : Data.SBV.BitVectors.Data + , Data.SBV.BitVectors.Model + , Data.SBV.BitVectors.PrettyNum + , Data.SBV.BitVectors.SignCast + , Data.SBV.BitVectors.Splittable + , Data.SBV.BitVectors.STree + , Data.SBV.Compilers.C + , Data.SBV.Compilers.CodeGen + , Data.SBV.SMT.SMT + , Data.SBV.SMT.SMTLib + , Data.SBV.SMT.SMTLib1 + , Data.SBV.SMT.SMTLib2 + , Data.SBV.Provers.Prover + , Data.SBV.Provers.SExpr + , Data.SBV.Provers.Yices + , Data.SBV.Provers.Z3 + , Data.SBV.Tools.ExpectedValue + , Data.SBV.Tools.GenTest + , Data.SBV.Tools.Optimize + , Data.SBV.Tools.Polynomial + , Data.SBV.Utils.Boolean + , Data.SBV.Utils.TDiff + , Data.SBV.Utils.Lib + +Executable SBVUnitTests + ghc-options : -Wall + Build-depends : base >= 3 && < 5 + , directory >= 1.0.1.1 + , HUnit >= 1.2.4.2 + , filepath >= 1.1.0.4 + , process >= 1.0.1.3 + Hs-Source-Dirs : SBVUnitTest, . + main-is : SBVUnitTest.hs + Other-modules : SBVUnitTestBuildTime + , SBVTest + , Examples.Arrays.Memory + , Examples.Basics.BasicTests + , Examples.Basics.Higher + , Examples.Basics.Index + , Examples.Basics.ProofTests + , Examples.Basics.QRem + , Examples.CRC.CCITT + , Examples.CRC.CCITT_Unidir + , Examples.CRC.GenPoly + , Examples.CRC.Parity + , Examples.CRC.USB5 + , Examples.Puzzles.PowerSet + , Examples.Puzzles.Temperature + , Examples.Uninterpreted.Uninterpreted + , TestSuite.Arrays.Memory + , TestSuite.Basics.Arithmetic + , TestSuite.Basics.BasicTests + , TestSuite.Basics.Higher + , TestSuite.Basics.Index + , TestSuite.Basics.ProofTests + , TestSuite.Basics.QRem + , TestSuite.BitPrecise.BitTricks + , TestSuite.BitPrecise.Legato + , TestSuite.BitPrecise.PrefixSum + , TestSuite.CodeGeneration.AddSub + , TestSuite.CodeGeneration.CgTests + , TestSuite.CodeGeneration.CRC_USB5 + , TestSuite.CodeGeneration.Fibonacci + , TestSuite.CodeGeneration.GCD + , TestSuite.CodeGeneration.PopulationCount + , TestSuite.CodeGeneration.Uninterpreted + , TestSuite.Crypto.AES + , TestSuite.Crypto.RC4 + , TestSuite.Existentials.CRCPolynomial + , TestSuite.CRC.CCITT + , TestSuite.CRC.CCITT_Unidir + , TestSuite.CRC.GenPoly + , TestSuite.CRC.Parity + , TestSuite.CRC.USB5 + , TestSuite.Puzzles.Coins + , TestSuite.Polynomials.Polynomials + , TestSuite.Puzzles.Counts + , TestSuite.Puzzles.DogCatMouse + , TestSuite.Puzzles.Euler185 + , TestSuite.Puzzles.MagicSquare + , TestSuite.Puzzles.NQueens + , TestSuite.Puzzles.PowerSet + , TestSuite.Puzzles.Sudoku + , TestSuite.Puzzles.U2Bridge + , TestSuite.Puzzles.Temperature + , TestSuite.Uninterpreted.AUF + , TestSuite.Uninterpreted.Function + , TestSuite.Uninterpreted.Uninterpreted