sbv-0.9.4: sbv.cabal

Name:          sbv
Version:       0.9.4
Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math
Synopsis:      Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.
Description:   Adds support for symbolic bit vectors, allowing formal models of bit-precise
               programs to be created. Supports symbolic arrays and polynomials over GF(2^n).
               Supports uninterpreted constants and functions. Aims to provide seamless integration
               with SMT solvers to produce formal property proofs of theoremhood and
               satisfiability, with counter-examples.
Copyright:     Levent Erkok, 2011
License:       BSD3
License-file:  LICENSE
Stability:     Experimental
Author:        Levent Erkok
Homepage:      http://github.com/LeventErkok/sbv
Maintainer:    Levent Erkok (erkokl@gmail.com)
Build-Type:    Custom
Cabal-Version: >= 1.6
Data-Files: SBVUnitTest/GoldFiles/*.gold
Extra-Source-Files: INSTALL, README, COPYRIGHT

Flag test
  Description: Run the unit-test suite after build
  Default    : False

Library
  ghc-options     : -Wall
  ghc-prof-options: -auto-all -caf-all
  Build-Depends   : base                >= 3 && < 5
                  , deepseq             >= 1.1.0.2
                  , process             >= 1.0.1.3
                  , containers          >= 0.3.0.0
                  , QuickCheck          >= 2.4.0.1
                  , strict-concurrency  >= 0.2.4.1
                  , old-time            >= 1.0.0.5
                  , mtl                 >= 2.0.1.0
                  , array               >= 0.3.0.1
                  , HUnit               >= 1.2.2.3
                  , directory           >= 1.0.1.1
                  , filepath            >= 1.1.0.4
  Exposed-modules : Data.SBV
                  , Data.SBV.Internals
                  , Data.SBV.Examples.BitPrecise.BitTricks
                  , Data.SBV.Examples.BitPrecise.Legato
                  , Data.SBV.Examples.Polynomials.Polynomials
                  , Data.SBV.Examples.Puzzles.DogCatMouse
                  , 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
  Other-modules   : Data.SBV.BitVectors.Data
                  , Data.SBV.BitVectors.Bit
                  , Data.SBV.BitVectors.Model
                  , Data.SBV.BitVectors.Splittable
                  , Data.SBV.BitVectors.Polynomial
                  , Data.SBV.BitVectors.PrettyNum
                  , Data.SBV.SMT.SMT
                  , Data.SBV.SMT.SMTLib
                  , Data.SBV.Provers.Prover
                  , Data.SBV.Provers.SExpr
                  , Data.SBV.Provers.Yices
                  , Data.SBV.Utils.Boolean
                  , Data.SBV.Utils.TDiff
                  , Data.SBV.Utils.SBVTest
                  , Data.SBV.Examples.Arrays.Memory
                  , Data.SBV.Examples.Basics.BasicTests
                  , Data.SBV.Examples.Basics.Higher
                  , Data.SBV.Examples.Basics.Index
                  , Data.SBV.Examples.Basics.ProofTests
                  , Data.SBV.Examples.Basics.QRem
                  , Data.SBV.Examples.Basics.UnsafeFunctionEquality
                  , Data.SBV.Examples.CRC.CCITT
                  , Data.SBV.Examples.CRC.CCITT_Unidir
                  , Data.SBV.Examples.CRC.GenPoly
                  , Data.SBV.Examples.CRC.Parity
                  , Data.SBV.Examples.CRC.USB5
                  , Data.SBV.Examples.PrefixSum.PrefixSum
                  , Data.SBV.Examples.Puzzles.PowerSet
                  , Data.SBV.Examples.Puzzles.Temperature
                  , Data.SBV.Examples.Uninterpreted.Uninterpreted
                  , Data.SBV.TestSuite.Arrays.Memory
                  , Data.SBV.TestSuite.Basics.BasicTests
                  , Data.SBV.TestSuite.Basics.Higher
                  , Data.SBV.TestSuite.Basics.Index
                  , Data.SBV.TestSuite.Basics.ProofTests
                  , Data.SBV.TestSuite.Basics.QRem
                  , Data.SBV.TestSuite.Basics.UnsafeFunctionEquality
                  , Data.SBV.TestSuite.BitPrecise.BitTricks
                  , Data.SBV.TestSuite.BitPrecise.Legato
                  , Data.SBV.TestSuite.CRC.CCITT
                  , Data.SBV.TestSuite.CRC.CCITT_Unidir
                  , Data.SBV.TestSuite.CRC.GenPoly
                  , Data.SBV.TestSuite.CRC.Parity
                  , Data.SBV.TestSuite.CRC.USB5
                  , Data.SBV.TestSuite.PrefixSum.PrefixSum
                  , Data.SBV.TestSuite.Polynomials.Polynomials
                  , Data.SBV.TestSuite.Puzzles.DogCatMouse
                  , Data.SBV.TestSuite.Puzzles.MagicSquare
                  , Data.SBV.TestSuite.Puzzles.NQueens
                  , Data.SBV.TestSuite.Puzzles.PowerSet
                  , Data.SBV.TestSuite.Puzzles.Sudoku
                  , Data.SBV.TestSuite.Puzzles.U2Bridge
                  , Data.SBV.TestSuite.Puzzles.Temperature
                  , Data.SBV.TestSuite.Uninterpreted.AUF
                  , Data.SBV.TestSuite.Uninterpreted.Uninterpreted

Executable SBVUnitTests
  main-is         : SBVUnitTest/SBVUnitTest.hs
  if flag(test)
    x-run-unittests: True
  else
    x-run-unittests: False