Cabal revisions of sbv-0.9.1
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-Name: sbv-Version: 0.9.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.-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- , containers >= 0.2.0- , QuickCheck >= 2.1.0.3- , strict-concurrency >= 0.2.3- , haskell98- , old-time >= 1.0.0.2- , 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+Name: sbv +Version: 0.9.1 +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. +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 + , 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 + , 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