Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Update from Hackage at 2019-03-09T23:55:27Z
- Loading branch information
1 parent
e114afe
commit 9939986
Showing
2 changed files
with
382 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,381 @@ | ||
| Name: sbv | ||
| Version: 8.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. | ||
| . | ||
| For details, please see: <http://leventerkok.github.com/sbv/> | ||
|
|
||
| Copyright: Levent Erkok, 2010-2019 | ||
| License: BSD3 | ||
| License-file: LICENSE | ||
| Stability: Experimental | ||
| Author: Levent Erkok | ||
| Homepage: http://leventerkok.github.com/sbv/ | ||
| Bug-reports: http://github.com/LeventErkok/sbv/issues | ||
| Maintainer: Levent Erkok (erkokl@gmail.com) | ||
| Build-Type: Simple | ||
| Cabal-Version: 1.14 | ||
| Data-Files: SBVTestSuite/GoldFiles/*.gold | ||
| Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md | ||
|
|
||
| source-repository head | ||
| type: git | ||
| location: git://github.com/LeventErkok/sbv.git | ||
|
|
||
| Library | ||
| default-language: Haskell2010 | ||
| ghc-options : -Wall -O2 | ||
| other-extensions: BangPatterns | ||
| CPP | ||
| ConstraintKinds | ||
| DataKinds | ||
| DefaultSignatures | ||
| DeriveAnyClass | ||
| DeriveDataTypeable | ||
| DeriveFunctor | ||
| DeriveGeneric | ||
| FlexibleContexts | ||
| FlexibleInstances | ||
| FunctionalDependencies | ||
| GADTs | ||
| GeneralizedNewtypeDeriving | ||
| ImplicitParams | ||
| InstanceSigs | ||
| KindSignatures | ||
| LambdaCase | ||
| MultiParamTypeClasses | ||
| NamedFieldPuns | ||
| OverloadedLists | ||
| OverloadedStrings | ||
| PatternGuards | ||
| QuasiQuotes | ||
| Rank2Types | ||
| RankNTypes | ||
| ScopedTypeVariables | ||
| StandaloneDeriving | ||
| TemplateHaskell | ||
| TupleSections | ||
| TypeApplications | ||
| TypeFamilies | ||
| TypeOperators | ||
| TypeSynonymInstances | ||
| UndecidableInstances | ||
| ViewPatterns | ||
| Build-Depends : base >= 4.9 && < 5 | ||
| , crackNum >= 2.3 | ||
| , ghc, QuickCheck, template-haskell | ||
| , array, async, containers, deepseq, directory, filepath, time | ||
| , pretty, process, mtl, random, syb, transformers | ||
| , generic-deriving | ||
| Exposed-modules : Data.SBV | ||
| , Data.SBV.Control | ||
| , Data.SBV.Dynamic | ||
| , Data.SBV.Either | ||
| , Data.SBV.Internals | ||
| , Data.SBV.List | ||
| , Data.SBV.Maybe | ||
| , Data.SBV.Set | ||
| , Data.SBV.String | ||
| , Data.SBV.Tuple | ||
| , Data.SBV.Char | ||
| , Data.SBV.RegExp | ||
| , Data.SBV.Tools.BMC | ||
| , Data.SBV.Tools.BoundedList | ||
| , Data.SBV.Tools.Induction | ||
| , Data.SBV.Tools.BoundedFix | ||
| , Data.SBV.Tools.CodeGen | ||
| , Data.SBV.Tools.GenTest | ||
| , Data.SBV.Tools.Overflow | ||
| , Data.SBV.Tools.Polynomial | ||
| , Data.SBV.Tools.Range | ||
| , Data.SBV.Tools.STree | ||
| , Data.SBV.Tools.WeakestPreconditions | ||
| , Data.SBV.Trans | ||
| , Data.SBV.Trans.Control | ||
| , Documentation.SBV.Examples.BitPrecise.BitTricks | ||
| , Documentation.SBV.Examples.BitPrecise.BrokenSearch | ||
| , Documentation.SBV.Examples.BitPrecise.Legato | ||
| , Documentation.SBV.Examples.BitPrecise.MergeSort | ||
| , Documentation.SBV.Examples.BitPrecise.MultMask | ||
| , Documentation.SBV.Examples.BitPrecise.PrefixSum | ||
| , Documentation.SBV.Examples.CodeGeneration.AddSub | ||
| , Documentation.SBV.Examples.CodeGeneration.CRC_USB5 | ||
| , Documentation.SBV.Examples.CodeGeneration.Fibonacci | ||
| , Documentation.SBV.Examples.CodeGeneration.GCD | ||
| , Documentation.SBV.Examples.CodeGeneration.PopulationCount | ||
| , Documentation.SBV.Examples.CodeGeneration.Uninterpreted | ||
| , Documentation.SBV.Examples.Crypto.AES | ||
| , Documentation.SBV.Examples.Crypto.RC4 | ||
| , Documentation.SBV.Examples.Existentials.CRCPolynomial | ||
| , Documentation.SBV.Examples.Existentials.Diophantine | ||
| , Documentation.SBV.Examples.Lists.Fibonacci | ||
| , Documentation.SBV.Examples.Lists.Nested | ||
| , Documentation.SBV.Examples.Lists.BoundedMutex | ||
| , Documentation.SBV.Examples.Misc.Enumerate | ||
| , Documentation.SBV.Examples.Misc.Floating | ||
| , Documentation.SBV.Examples.Misc.ModelExtract | ||
| , Documentation.SBV.Examples.Misc.Auxiliary | ||
| , Documentation.SBV.Examples.Misc.NoDiv0 | ||
| , Documentation.SBV.Examples.Misc.Polynomials | ||
| , Documentation.SBV.Examples.Misc.SetAlgebra | ||
| , Documentation.SBV.Examples.Misc.SoftConstrain | ||
| , Documentation.SBV.Examples.Misc.Tuple | ||
| , Documentation.SBV.Examples.Misc.Word4 | ||
| , Documentation.SBV.Examples.Optimization.Enumerate | ||
| , Documentation.SBV.Examples.Optimization.ExtField | ||
| , Documentation.SBV.Examples.Optimization.LinearOpt | ||
| , Documentation.SBV.Examples.Optimization.Production | ||
| , Documentation.SBV.Examples.Optimization.VM | ||
| , Documentation.SBV.Examples.ProofTools.BMC | ||
| , Documentation.SBV.Examples.ProofTools.Fibonacci | ||
| , Documentation.SBV.Examples.ProofTools.Strengthen | ||
| , Documentation.SBV.Examples.ProofTools.Sum | ||
| , Documentation.SBV.Examples.WeakestPreconditions.Append | ||
| , Documentation.SBV.Examples.WeakestPreconditions.Fib | ||
| , Documentation.SBV.Examples.WeakestPreconditions.GCD | ||
| , Documentation.SBV.Examples.WeakestPreconditions.IntDiv | ||
| , Documentation.SBV.Examples.WeakestPreconditions.IntSqrt | ||
| , Documentation.SBV.Examples.WeakestPreconditions.Length | ||
| , Documentation.SBV.Examples.WeakestPreconditions.Sum | ||
| , Documentation.SBV.Examples.Puzzles.Birthday | ||
| , Documentation.SBV.Examples.Puzzles.Coins | ||
| , Documentation.SBV.Examples.Puzzles.Counts | ||
| , Documentation.SBV.Examples.Puzzles.DogCatMouse | ||
| , Documentation.SBV.Examples.Puzzles.Euler185 | ||
| , Documentation.SBV.Examples.Puzzles.Fish | ||
| , Documentation.SBV.Examples.Puzzles.Garden | ||
| , Documentation.SBV.Examples.Puzzles.HexPuzzle | ||
| , Documentation.SBV.Examples.Puzzles.LadyAndTigers | ||
| , Documentation.SBV.Examples.Puzzles.MagicSquare | ||
| , Documentation.SBV.Examples.Puzzles.NQueens | ||
| , Documentation.SBV.Examples.Puzzles.SendMoreMoney | ||
| , Documentation.SBV.Examples.Puzzles.Sudoku | ||
| , Documentation.SBV.Examples.Puzzles.U2Bridge | ||
| , Documentation.SBV.Examples.Queries.AllSat | ||
| , Documentation.SBV.Examples.Queries.UnsatCore | ||
| , Documentation.SBV.Examples.Queries.FourFours | ||
| , Documentation.SBV.Examples.Queries.GuessNumber | ||
| , Documentation.SBV.Examples.Queries.CaseSplit | ||
| , Documentation.SBV.Examples.Queries.Enums | ||
| , Documentation.SBV.Examples.Queries.Interpolants | ||
| , Documentation.SBV.Examples.Strings.RegexCrossword | ||
| , Documentation.SBV.Examples.Strings.SQLInjection | ||
| , Documentation.SBV.Examples.Transformers.SymbolicEval | ||
| , Documentation.SBV.Examples.Uninterpreted.AUF | ||
| , Documentation.SBV.Examples.Uninterpreted.Deduce | ||
| , Documentation.SBV.Examples.Uninterpreted.Function | ||
| , Documentation.SBV.Examples.Uninterpreted.Multiply | ||
| , Documentation.SBV.Examples.Uninterpreted.Shannon | ||
| , Documentation.SBV.Examples.Uninterpreted.Sort | ||
| , Documentation.SBV.Examples.Uninterpreted.UISortAllSat | ||
| Other-modules : Data.SBV.Client | ||
| , Data.SBV.Client.BaseIO | ||
| , Data.SBV.Core.AlgReals | ||
| , Data.SBV.Core.Concrete | ||
| , Data.SBV.Core.Data | ||
| , Data.SBV.Core.Kind | ||
| , Data.SBV.Core.Model | ||
| , Data.SBV.Core.Operations | ||
| , Data.SBV.Core.Floating | ||
| , Data.SBV.Core.Splittable | ||
| , Data.SBV.Core.Symbolic | ||
| , Data.SBV.Control.BaseIO | ||
| , Data.SBV.Control.Query | ||
| , Data.SBV.Control.Types | ||
| , Data.SBV.Control.Utils | ||
| , Data.SBV.Compilers.C | ||
| , Data.SBV.Compilers.CodeGen | ||
| , Data.SBV.SMT.SMT | ||
| , Data.SBV.SMT.SMTLib | ||
| , Data.SBV.SMT.SMTLib2 | ||
| , Data.SBV.SMT.SMTLibNames | ||
| , Data.SBV.SMT.Utils | ||
| , Data.SBV.Provers.Prover | ||
| , Data.SBV.Provers.Boolector | ||
| , Data.SBV.Provers.CVC4 | ||
| , Data.SBV.Provers.Yices | ||
| , Data.SBV.Provers.Z3 | ||
| , Data.SBV.Provers.MathSAT | ||
| , Data.SBV.Provers.ABC | ||
| , Data.SBV.Utils.ExtractIO | ||
| , Data.SBV.Utils.Numeric | ||
| , Data.SBV.Utils.TDiff | ||
| , Data.SBV.Utils.Lib | ||
| , Data.SBV.Utils.PrettyNum | ||
| , Data.SBV.Utils.SExpr | ||
|
|
||
| Test-Suite SBVTest | ||
| type : exitcode-stdio-1.0 | ||
| default-language: Haskell2010 | ||
| ghc-options : -Wall -with-rtsopts=-K64m -O2 | ||
| other-extensions: DataKinds | ||
| DeriveAnyClass | ||
| DeriveDataTypeable | ||
| FlexibleContexts | ||
| GeneralizedNewtypeDeriving | ||
| OverloadedLists | ||
| OverloadedStrings | ||
| Rank2Types | ||
| RankNTypes | ||
| ScopedTypeVariables | ||
| StandaloneDeriving | ||
| TemplateHaskell | ||
| TupleSections | ||
| TypeApplications | ||
| Build-depends : base >= 4.9, filepath, syb, crackNum >= 2.3 | ||
| , sbv, directory, random, mtl, containers | ||
| , template-haskell, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, QuickCheck | ||
| Hs-Source-Dirs : SBVTestSuite | ||
| main-is : SBVTest.hs | ||
| Other-modules : Utils.SBVTestFramework | ||
| , TestSuite.Arrays.InitVals | ||
| , TestSuite.Arrays.Memory | ||
| , TestSuite.Arrays.Query | ||
| , TestSuite.Basics.AllSat | ||
| , TestSuite.Basics.ArithNoSolver | ||
| , TestSuite.Basics.ArithSolver | ||
| , TestSuite.Basics.Assert | ||
| , TestSuite.Basics.BarrelRotate | ||
| , TestSuite.Basics.BasicTests | ||
| , TestSuite.Basics.BoundedList | ||
| , TestSuite.Basics.DynSign | ||
| , TestSuite.Basics.Exceptions | ||
| , TestSuite.Basics.GenBenchmark | ||
| , TestSuite.Basics.Higher | ||
| , TestSuite.Basics.Index | ||
| , TestSuite.Basics.IteTest | ||
| , TestSuite.Basics.List | ||
| , TestSuite.Basics.ModelValidate | ||
| , TestSuite.Basics.ProofTests | ||
| , TestSuite.Basics.PseudoBoolean | ||
| , TestSuite.Basics.QRem | ||
| , TestSuite.Basics.Quantifiers | ||
| , TestSuite.Basics.Recursive | ||
| , TestSuite.Basics.Set | ||
| , TestSuite.Basics.SmallShifts | ||
| , TestSuite.Basics.SquashReals | ||
| , TestSuite.Basics.String | ||
| , TestSuite.Basics.Sum | ||
| , TestSuite.Basics.TOut | ||
| , TestSuite.Basics.Tuple | ||
| , TestSuite.Basics.UISat | ||
| , 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.Floats | ||
| , TestSuite.CodeGeneration.GCD | ||
| , TestSuite.CodeGeneration.PopulationCount | ||
| , TestSuite.CodeGeneration.Uninterpreted | ||
| , TestSuite.CRC.CCITT | ||
| , TestSuite.CRC.CCITT_Unidir | ||
| , TestSuite.CRC.GenPoly | ||
| , TestSuite.CRC.Parity | ||
| , TestSuite.CRC.USB5 | ||
| , TestSuite.Crypto.AES | ||
| , TestSuite.Crypto.RC4 | ||
| , TestSuite.Existentials.CRCPolynomial | ||
| , TestSuite.GenTest.GenTests | ||
| , TestSuite.Optimization.AssertWithPenalty | ||
| , TestSuite.Optimization.Basics | ||
| , TestSuite.Optimization.Combined | ||
| , TestSuite.Optimization.ExtensionField | ||
| , TestSuite.Optimization.Floats | ||
| , TestSuite.Optimization.NoOpt | ||
| , TestSuite.Optimization.Quantified | ||
| , TestSuite.Optimization.Reals | ||
| , TestSuite.Optimization.Tuples | ||
| , TestSuite.Overflows.Arithmetic | ||
| , TestSuite.Overflows.Casts | ||
| , TestSuite.Polynomials.Polynomials | ||
| , TestSuite.Puzzles.Coins | ||
| , TestSuite.Puzzles.Counts | ||
| , TestSuite.Puzzles.DogCatMouse | ||
| , TestSuite.Puzzles.Euler185 | ||
| , TestSuite.Puzzles.MagicSquare | ||
| , TestSuite.Puzzles.NQueens | ||
| , TestSuite.Puzzles.PowerSet | ||
| , TestSuite.Puzzles.Sudoku | ||
| , TestSuite.Puzzles.Temperature | ||
| , TestSuite.Puzzles.U2Bridge | ||
| , TestSuite.Queries.BasicQuery | ||
| , TestSuite.Queries.BadOption | ||
| , TestSuite.Queries.Enums | ||
| , TestSuite.Queries.FreshVars | ||
| , TestSuite.Queries.Int_ABC | ||
| , TestSuite.Queries.Int_Boolector | ||
| , TestSuite.Queries.Int_CVC4 | ||
| , TestSuite.Queries.Int_Mathsat | ||
| , TestSuite.Queries.Int_Yices | ||
| , TestSuite.Queries.Int_Z3 | ||
| , TestSuite.Queries.Interpolants | ||
| , TestSuite.Queries.Lists | ||
| , TestSuite.Queries.Strings | ||
| , TestSuite.Queries.Sums | ||
| , TestSuite.Queries.Tuples | ||
| , TestSuite.Queries.Uninterpreted | ||
| , TestSuite.Queries.UISat | ||
| , TestSuite.Queries.UISatEx | ||
| , TestSuite.QuickCheck.QC | ||
| , TestSuite.Transformers.SymbolicEval | ||
| , TestSuite.Uninterpreted.AUF | ||
| , TestSuite.Uninterpreted.Axioms | ||
| , TestSuite.Uninterpreted.Function | ||
| , TestSuite.Uninterpreted.Sort | ||
| , TestSuite.Uninterpreted.Uninterpreted | ||
|
|
||
| Test-Suite SBVDocTest | ||
| Build-Depends: base, directory, filepath, random | ||
| , doctest, Glob, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck, random | ||
| , sbv | ||
| ghc-options : -Wall -O2 | ||
| other-extensions: DataKinds | ||
| DeriveAnyClass | ||
| DeriveDataTypeable | ||
| FlexibleContexts | ||
| GeneralizedNewtypeDeriving | ||
| OverloadedLists | ||
| OverloadedStrings | ||
| Rank2Types | ||
| RankNTypes | ||
| ScopedTypeVariables | ||
| StandaloneDeriving | ||
| TemplateHaskell | ||
| TupleSections | ||
| TypeApplications | ||
| default-language: Haskell2010 | ||
| Hs-Source-Dirs : SBVTestSuite | ||
| main-is: SBVDocTest.hs | ||
| Other-modules : Utils.SBVTestFramework | ||
| type: exitcode-stdio-1.0 | ||
|
|
||
| Test-Suite SBVHLint | ||
| build-depends: base, directory, filepath, random | ||
| , hlint, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck | ||
| , sbv | ||
| ghc-options : -Wall -O2 | ||
| other-extensions: DataKinds | ||
| DeriveAnyClass | ||
| DeriveDataTypeable | ||
| FlexibleContexts | ||
| GeneralizedNewtypeDeriving | ||
| OverloadedLists | ||
| OverloadedStrings | ||
| Rank2Types | ||
| RankNTypes | ||
| ScopedTypeVariables | ||
| StandaloneDeriving | ||
| TemplateHaskell | ||
| TupleSections | ||
| TypeApplications | ||
| default-language: Haskell2010 | ||
| hs-source-dirs: SBVTestSuite | ||
| Other-modules : Utils.SBVTestFramework | ||
| main-is: SBVHLint.hs | ||
| type: exitcode-stdio-1.0 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1 @@ | ||
| {"package-hashes":{"MD5":"8c548a90c8227c88c8b0514e9c993030","Skein512_512":"4745eaaa5de4443c1caa31cfcb19f930d78d97a761d5f460d05229b29444e7924702b6f03960835255c805459ec4befbb536b45d1088c6570be608f93e86d641","SHA1":"a9d1ac0ceca513feeb193834675a5aab7542e68f","SHA512":"fe1225bc74b64c33e0bd9205cbdbf3b957b9b29725b8bbbc4a31653795cb85992d203c11fc9bc6983cb8e10437e48f8dfa581f04372b8830f46657bf3deab50f","SHA256":"3e699e02960c1f08b900544e6168fa3a5fad5f5da3819948191ca6b884248dd3"},"package-locations":["https://hackage.haskell.org/package/sbv-8.1/sbv-8.1.tar.gz","https://s3.amazonaws.com/hackage.fpcomplete.com/package/sbv-8.1.tar.gz"],"package-size":826425} |