Name: sbv Version: 0.9 x-revision: 1 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). Aims to provide seamless integration with SMT solvers to produce formal property proofs of theoremhood and satisfiability, with counter-examples. 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 , process >= 1.0.1 , containers >= 0.2.0 , QuickCheck >= 2.1.0.3 && < 2.3 , strict-concurrency >= 0.2.3 , haskell98 < 1.2 , old-time >= 1.0.0.2 , parallel >= 2.2.0.1 , mtl >= 1.1.0.2 , array >= 0.2.0.0 , 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.Puzzles.DogCatMouse , Data.SBV.Examples.Puzzles.MagicSquare , Data.SBV.Examples.Puzzles.NQueens , Data.SBV.Examples.Puzzles.Sudoku , Data.SBV.Examples.Puzzles.U2Bridge 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.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.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 Executable SBVUnitTests main-is : SBVUnitTest/SBVUnitTest.hs if flag(test) x-run-unittests: True else x-run-unittests: False