sbv-7.5: sbv.cabal
Name: sbv
Version: 7.5
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-2018
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
other-extensions: BangPatterns
DefaultSignatures
DeriveAnyClass
DeriveDataTypeable
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GeneralizedNewtypeDeriving
MultiParamTypeClasses
OverlappingInstances
ParallelListComp
PatternGuards
Rank2Types
RankNTypes
ScopedTypeVariables
StandaloneDeriving
TemplateHaskell
TupleSections
TypeOperators
TypeSynonymInstances
Build-Depends : base >= 4.9 && < 5
, ghc, QuickCheck, crackNum, template-haskell
, array, async, containers, deepseq, directory, filepath, time
, pretty, process, mtl, random, syb, data-binary-ieee754
, generic-deriving
Exposed-modules : Data.SBV
, Data.SBV.Control
, Data.SBV.Dynamic
, Data.SBV.Internals
, Data.SBV.Tools.CodeGen
, Data.SBV.Tools.GenTest
, Data.SBV.Tools.Polynomial
, Data.SBV.Tools.STree
, Data.SBV.Examples.BitPrecise.BitTricks
, Data.SBV.Examples.BitPrecise.Legato
, Data.SBV.Examples.BitPrecise.MergeSort
, Data.SBV.Examples.BitPrecise.MultMask
, Data.SBV.Examples.BitPrecise.PrefixSum
, Data.SBV.Examples.CodeGeneration.AddSub
, Data.SBV.Examples.CodeGeneration.CRC_USB5
, Data.SBV.Examples.CodeGeneration.Fibonacci
, Data.SBV.Examples.CodeGeneration.GCD
, Data.SBV.Examples.CodeGeneration.PopulationCount
, Data.SBV.Examples.CodeGeneration.Uninterpreted
, Data.SBV.Examples.Crypto.AES
, Data.SBV.Examples.Crypto.RC4
, Data.SBV.Examples.Existentials.CRCPolynomial
, Data.SBV.Examples.Existentials.Diophantine
, Data.SBV.Examples.Misc.Enumerate
, Data.SBV.Examples.Misc.Floating
, Data.SBV.Examples.Misc.ModelExtract
, Data.SBV.Examples.Misc.Auxiliary
, Data.SBV.Examples.Misc.NoDiv0
, Data.SBV.Examples.Misc.Word4
, Data.SBV.Examples.Polynomials.Polynomials
, Data.SBV.Examples.Optimization.LinearOpt
, Data.SBV.Examples.Optimization.Production
, Data.SBV.Examples.Optimization.VM
, Data.SBV.Examples.Optimization.ExtField
, Data.SBV.Examples.Puzzles.Birthday
, Data.SBV.Examples.Puzzles.Coins
, Data.SBV.Examples.Puzzles.Counts
, Data.SBV.Examples.Puzzles.DogCatMouse
, Data.SBV.Examples.Puzzles.Euler185
, Data.SBV.Examples.Puzzles.Fish
, Data.SBV.Examples.Puzzles.MagicSquare
, Data.SBV.Examples.Puzzles.NQueens
, Data.SBV.Examples.Puzzles.SendMoreMoney
, Data.SBV.Examples.Puzzles.Sudoku
, Data.SBV.Examples.Puzzles.U2Bridge
, Data.SBV.Examples.Queries.AllSat
, Data.SBV.Examples.Queries.UnsatCore
, Data.SBV.Examples.Queries.FourFours
, Data.SBV.Examples.Queries.GuessNumber
, Data.SBV.Examples.Queries.CaseSplit
, Data.SBV.Examples.Queries.Enums
, Data.SBV.Examples.Queries.Interpolants
, Data.SBV.Examples.Uninterpreted.AUF
, Data.SBV.Examples.Uninterpreted.Deduce
, Data.SBV.Examples.Uninterpreted.Function
, Data.SBV.Examples.Uninterpreted.Shannon
, Data.SBV.Examples.Uninterpreted.Sort
, Data.SBV.Examples.Uninterpreted.UISortAllSat
Other-modules : 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.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.Boolean
, 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
other-extensions: DeriveAnyClass
, DeriveDataTypeable
, Rank2Types
, ScopedTypeVariables
Build-depends : base >= 4.9, data-binary-ieee754, filepath, syb
, sbv, directory, random, mtl, containers
, template-haskell, bytestring, tasty, tasty-golden, tasty-hunit
Hs-Source-Dirs : SBVTestSuite
main-is : SBVTest.hs
Other-modules : Utils.SBVTestFramework
, TestSuite.Arrays.Memory
, TestSuite.Arrays.Query
, TestSuite.Basics.AllSat
, TestSuite.Basics.ArithNoSolver
, TestSuite.Basics.ArithSolver
, TestSuite.Basics.BasicTests
, 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.TOut
, 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.AssertSoft
, TestSuite.Optimization.Basics
, TestSuite.Optimization.Combined
, TestSuite.Optimization.ExtensionField
, TestSuite.Optimization.Quantified
, TestSuite.Optimization.Reals
, 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.Uninterpreted
, 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
, sbv
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
, sbv
default-language: Haskell2010
hs-source-dirs: SBVTestSuite
Other-modules : Utils.SBVTestFramework
main-is: SBVHLint.hs
type: exitcode-stdio-1.0