Name:          sbv
Version:       2.5
x-revision: 1
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
               (Satisfiability Modulo Theories) solvers. Automatically generate C programs from
               Haskell functions. The SBV library adds support for symbolic bit vectors and other
               symbolic types, allowing formal models of Haskell 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 SBV library uses Microsoft's Z3 SMT solver (<http://research.microsoft.com/en-us/um/redmond/projects/z3/>) as the default underlying solver. It is also possible to use SRI's Yices SMT solver with SBV as well (<http://yices.csl.sri.com/download-yices2.shtml>), although the Z3 binding is much more richer.
               .
               SBV 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)
               .
                 * 'SReal': Symbolic algebraic reals (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 axioms.
               .
                 * Uninterpreted sorts, and proofs over such sorts, potentially with 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, John
               Erickson, 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.14
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
  default-language: Haskell2010
  ghc-options     : -Wall
  other-extensions: BangPatterns
                    CPP
                    -- 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
                    FlexibleInstances
                    FunctionalDependencies
                    GeneralizedNewtypeDeriving
                    MultiParamTypeClasses
                    OverlappingInstances
                    ParallelListComp
                    PatternGuards
                    Rank2Types
                    RankNTypes
                    ScopedTypeVariables
                    TupleSections
                    TypeOperators
                    TypeSynonymInstances
  Build-Depends   : base >= 4 && < 4.8
                  , array, containers, deepseq, directory, filepath, old-time
                  , pretty, process, mtl, QuickCheck, random, syb
  Exposed-modules : Data.SBV
                  , Data.SBV.Internals
                  , Data.SBV.Examples.BitPrecise.BitTricks
                  , Data.SBV.Examples.BitPrecise.Legato
                  , Data.SBV.Examples.BitPrecise.MergeSort
                  , 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.Existentials.Diophantine
                  , 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.Deduce
                  , Data.SBV.Examples.Uninterpreted.Function
                  , Data.SBV.Examples.Uninterpreted.Sort
  Other-modules   : Data.SBV.BitVectors.AlgReals
                  , 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
  default-language: Haskell2010
  ghc-options     : -Wall
  other-extensions: Rank2Types
                    RankNTypes
                    ScopedTypeVariables
                    TupleSections
  Build-depends   : base  >= 4 && < 5
                  , HUnit, directory, filepath, process, sbv
  Hs-Source-Dirs  : SBVUnitTest
  main-is         : SBVUnitTest.hs
  Other-modules   : SBVUnitTestBuildTime
                  , SBVTest
                  , SBVTestCollection
                  , 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.ArithNoSolver
                  , TestSuite.Basics.ArithSolver
                  , TestSuite.Basics.BasicTests
                  , TestSuite.Basics.Higher
                  , TestSuite.Basics.Index
                  , TestSuite.Basics.ProofTests
                  , TestSuite.Basics.QRem
                  , TestSuite.BitPrecise.BitTricks
                  , TestSuite.BitPrecise.Legato
                  , TestSuite.BitPrecise.MergeSort
                  , 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

Test-Suite SBVBasicTests
  type            : exitcode-stdio-1.0
  default-language: Haskell2010
  ghc-options     : -Wall
  Build-depends   : base >= 4 && < 5
                  , HUnit, directory, filepath, sbv
  Hs-Source-Dirs  : SBVUnitTest
  main-is         : SBVBasicTests.hs
  Other-modules   : SBVBasicTests
                  , SBVTestCollection