sbv-8.0: sbv.cabal
Name: sbv
Version: 8.0
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.Internals
, Data.SBV.List
, 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.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.SoftConstrain
, Documentation.SBV.Examples.Misc.Tuple
, Documentation.SBV.Examples.Misc.Word4
, Documentation.SBV.Examples.Optimization.LinearOpt
, Documentation.SBV.Examples.Optimization.Production
, Documentation.SBV.Examples.Optimization.VM
, Documentation.SBV.Examples.Optimization.ExtField
, Documentation.SBV.Examples.ProofTools.BMC
, Documentation.SBV.Examples.ProofTools.Fibonacci
, Documentation.SBV.Examples.ProofTools.Strengthen
, Documentation.SBV.Examples.ProofTools.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.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.BasicTests
, TestSuite.Basics.BoundedList
, TestSuite.Basics.Exceptions
, TestSuite.Basics.GenBenchmark
, TestSuite.Basics.Higher
, TestSuite.Basics.Index
, TestSuite.Basics.IteTest
, TestSuite.Basics.ProofTests
, TestSuite.Basics.PseudoBoolean
, TestSuite.Basics.QRem
, TestSuite.Basics.Quantifiers
, TestSuite.Basics.Recursive
, TestSuite.Basics.SmallShifts
, TestSuite.Basics.SquashReals
, TestSuite.Basics.String
, TestSuite.Basics.List
, TestSuite.Basics.TOut
, TestSuite.Basics.Tuple
, 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.Quantified
, TestSuite.Optimization.Reals
, TestSuite.Optimization.NoOpt
, 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.Tuples
, TestSuite.Queries.Uninterpreted
, 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