sbv-10.1: sbv.cabal
Cabal-Version: 2.2
Name : sbv
Version : 10.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.io/sbv/>
Copyright : Levent Erkok, 2010-2023
License : BSD-3-Clause
License-file : LICENSE
Stability : Experimental
Author : Levent Erkok
Homepage : http://leventerkok.github.io/sbv/
Bug-reports : http://github.com/LeventErkok/sbv/issues
Maintainer : Levent Erkok (erkokl@gmail.com)
Build-Type : Simple
Data-Files : SBVTestSuite/GoldFiles/*.gold
Extra-Source-Files : INSTALL, README.md, COPYRIGHT, CHANGES.md
Tested-With : GHC==9.6.1
source-repository head
type: git
location: git://github.com/LeventErkok/sbv.git
common common-settings
default-language: Haskell2010
ghc-options : -Wall -O2
build-depends : base >= 4.11 && < 5
if impl(ghc >= 8.10.1)
ghc-options : -Wunused-packages
Library
import : common-settings
default-language: Haskell2010
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 : QuickCheck, template-haskell
, array, async, containers, deepseq, directory, filepath, time
, pretty, process, mtl, random, syb, text, transformers, uniplate
, libBF
Exposed-modules : Data.SBV
, Data.SBV.Control
, Data.SBV.Dynamic
, Data.SBV.Either
, Data.SBV.Float
, Data.SBV.Internals
, Data.SBV.List
, Data.SBV.Maybe
, Data.SBV.Rational
, Data.SBV.Set
, Data.SBV.Char
, Data.SBV.String
, Data.SBV.Tuple
, 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.Crypto.SHA
, Documentation.SBV.Examples.DeltaSat.DeltaSat
, 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.Lists.CountOutAndTransfer
, Documentation.SBV.Examples.Misc.Definitions
, Documentation.SBV.Examples.Misc.Enumerate
, Documentation.SBV.Examples.Misc.FirstOrderLogic
, Documentation.SBV.Examples.Misc.Floating
, Documentation.SBV.Examples.Misc.LambdaArray
, Documentation.SBV.Examples.Misc.ModelExtract
, Documentation.SBV.Examples.Misc.NestedArray
, Documentation.SBV.Examples.Misc.Auxiliary
, Documentation.SBV.Examples.Misc.NoDiv0
, Documentation.SBV.Examples.Misc.Newtypes
, Documentation.SBV.Examples.Misc.Polynomials
, Documentation.SBV.Examples.Misc.SetAlgebra
, Documentation.SBV.Examples.Misc.SoftConstrain
, Documentation.SBV.Examples.Misc.Tuple
, 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.Basics
, 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.AOC_2021_24
, Documentation.SBV.Examples.Puzzles.Birthday
, Documentation.SBV.Examples.Puzzles.Coins
, Documentation.SBV.Examples.Puzzles.Counts
, Documentation.SBV.Examples.Puzzles.DogCatMouse
, Documentation.SBV.Examples.Puzzles.Drinker
, Documentation.SBV.Examples.Puzzles.Euler185
, Documentation.SBV.Examples.Puzzles.Fish
, Documentation.SBV.Examples.Puzzles.Garden
, Documentation.SBV.Examples.Puzzles.HexPuzzle
, Documentation.SBV.Examples.Puzzles.Jugs
, Documentation.SBV.Examples.Puzzles.KnightsAndKnaves
, Documentation.SBV.Examples.Puzzles.LadyAndTigers
, Documentation.SBV.Examples.Puzzles.MagicSquare
, Documentation.SBV.Examples.Puzzles.Murder
, Documentation.SBV.Examples.Puzzles.NQueens
, Documentation.SBV.Examples.Puzzles.Orangutans
, Documentation.SBV.Examples.Puzzles.Rabbits
, Documentation.SBV.Examples.Puzzles.SendMoreMoney
, Documentation.SBV.Examples.Puzzles.Sudoku
, Documentation.SBV.Examples.Puzzles.U2Bridge
, Documentation.SBV.Examples.Queries.Abducts
, 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.Queries.Concurrency
, 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.Sized
, Data.SBV.Core.SizedFloats
, 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.Lambda
, 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.ABC
, Data.SBV.Provers.Boolector
, Data.SBV.Provers.Bitwuzla
, Data.SBV.Provers.CVC4
, Data.SBV.Provers.CVC5
, Data.SBV.Provers.DReal
, Data.SBV.Provers.MathSAT
, Data.SBV.Provers.Yices
, Data.SBV.Provers.Z3
, Data.SBV.Utils.CrackNum
, 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
import : common-settings
default-language : Haskell2010
type : exitcode-stdio-1.0
ghc-options : -with-rtsopts=-K64m
other-extensions : DataKinds
DeriveAnyClass
DeriveDataTypeable
FlexibleContexts
GeneralizedNewtypeDeriving
OverloadedLists
OverloadedStrings
Rank2Types
RankNTypes
ScopedTypeVariables
StandaloneDeriving
TemplateHaskell
TupleSections
TypeApplications
build-depends : filepath, sbv, directory, random, mtl, containers, deepseq
, 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.Arrays.Caching
, TestSuite.Basics.AllSat
, TestSuite.Basics.ArbFloats
, TestSuite.Basics.ArithNoSolver
, TestSuite.Basics.ArithSolver
, TestSuite.Basics.Assert
, TestSuite.Basics.BarrelRotate
, TestSuite.Basics.BasicTests
, TestSuite.Basics.BoundedList
, TestSuite.Basics.DynSign
, TestSuite.Basics.EqSym
, TestSuite.Basics.Exceptions
, TestSuite.Basics.GenBenchmark
, TestSuite.Basics.Higher
, TestSuite.Basics.Index
, TestSuite.Basics.IteTest
, TestSuite.Basics.Lambda
, TestSuite.Basics.List
, TestSuite.Basics.ModelValidate
, TestSuite.Basics.Nonlinear
, 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.Char.Char
, 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.Crypto.SHA
, 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.DSat
, 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.Tables
, 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
, TestSuite.CantTypeCheck.Misc
Test-Suite SBVConnections
import : common-settings
default-language: Haskell2010
build-depends : sbv
hs-source-dirs : SBVTestSuite
main-is : SBVConnectionTest.hs
type: exitcode-stdio-1.0
Test-Suite SBVDocTest
import : common-settings
default-language: Haskell2010
build-depends : base, sbv, process, QuickCheck, filepath, mtl, bytestring, directory
, tasty, tasty-quickcheck, tasty-golden, tasty-hunit, deepseq
other-extensions: DataKinds
DeriveAnyClass
DeriveDataTypeable
FlexibleContexts
GeneralizedNewtypeDeriving
OverloadedLists
OverloadedStrings
Rank2Types
RankNTypes
ScopedTypeVariables
StandaloneDeriving
TemplateHaskell
TupleSections
TypeApplications
hs-source-dirs : SBVTestSuite
main-is: SBVDocTest.hs
other-modules : Utils.SBVTestFramework
type: exitcode-stdio-1.0
Test-Suite SBVHLint
import : common-settings
default-language: Haskell2010
build-depends : base, directory, filepath, process, deepseq
, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck, sbv
other-extensions: DataKinds
DeriveAnyClass
DeriveDataTypeable
FlexibleContexts
GeneralizedNewtypeDeriving
OverloadedLists
OverloadedStrings
Rank2Types
RankNTypes
ScopedTypeVariables
StandaloneDeriving
TemplateHaskell
TupleSections
TypeApplications
hs-source-dirs : SBVTestSuite
other-modules : Utils.SBVTestFramework
main-is : SBVHLint.hs
type : exitcode-stdio-1.0
Benchmark SBVBench
import : common-settings
default-language: Haskell2010
type : exitcode-stdio-1.0
ghc-options : -with-rtsopts=-K64m
other-extensions: DataKinds
DeriveAnyClass
DeriveDataTypeable
FlexibleContexts
GeneralizedNewtypeDeriving
OverloadedLists
OverloadedStrings
Rank2Types
RankNTypes
ScopedTypeVariables
StandaloneDeriving
TemplateHaskell
TupleSections
TypeApplications
build-depends : filepath, sbv, random, time , process, deepseq, tasty, tasty-bench
hs-source-dirs : SBVBenchSuite
main-is : SBVBench.hs
other-modules : Utils.SBVBenchFramework
, BenchSuite.Bench.Bench
, BenchSuite.Puzzles.Birthday
, BenchSuite.Puzzles.Coins
, BenchSuite.Puzzles.Counts
, BenchSuite.Puzzles.DogCatMouse
, BenchSuite.Puzzles.Euler185
, BenchSuite.Puzzles.Garden
, BenchSuite.Puzzles.LadyAndTigers
, BenchSuite.Puzzles.MagicSquare
, BenchSuite.Puzzles.NQueens
, BenchSuite.Puzzles.SendMoreMoney
, BenchSuite.Puzzles.Sudoku
, BenchSuite.Puzzles.U2Bridge
, BenchSuite.BitPrecise.BitTricks
, BenchSuite.BitPrecise.BrokenSearch
, BenchSuite.BitPrecise.Legato
, BenchSuite.BitPrecise.MergeSort
, BenchSuite.BitPrecise.MultMask
, BenchSuite.BitPrecise.PrefixSum
, BenchSuite.Queries.AllSat
, BenchSuite.Queries.CaseSplit
, BenchSuite.Queries.Concurrency
, BenchSuite.Queries.Enums
, BenchSuite.Queries.FourFours
, BenchSuite.Queries.GuessNumber
, BenchSuite.Queries.Interpolants
, BenchSuite.Queries.UnsatCore
, BenchSuite.WeakestPreconditions.Instances
, BenchSuite.WeakestPreconditions.Append
, BenchSuite.WeakestPreconditions.Basics
, BenchSuite.WeakestPreconditions.Fib
, BenchSuite.WeakestPreconditions.GCD
, BenchSuite.WeakestPreconditions.IntDiv
, BenchSuite.WeakestPreconditions.IntSqrt
, BenchSuite.WeakestPreconditions.Length
, BenchSuite.WeakestPreconditions.Sum
, BenchSuite.Optimization.Instances
, BenchSuite.Optimization.Enumerate
, BenchSuite.Optimization.ExtField
, BenchSuite.Optimization.LinearOpt
, BenchSuite.Optimization.Production
, BenchSuite.Optimization.VM
, BenchSuite.Uninterpreted.AUF
, BenchSuite.Uninterpreted.Deduce
, BenchSuite.Uninterpreted.Function
, BenchSuite.Uninterpreted.Multiply
, BenchSuite.Uninterpreted.Shannon
, BenchSuite.Uninterpreted.Sort
, BenchSuite.Uninterpreted.UISortAllSat
, BenchSuite.ProofTools.BMC
, BenchSuite.ProofTools.Fibonacci
, BenchSuite.ProofTools.Strengthen
, BenchSuite.ProofTools.Sum
, BenchSuite.CodeGeneration.AddSub
, BenchSuite.CodeGeneration.CRC_USB5
, BenchSuite.CodeGeneration.Fibonacci
, BenchSuite.CodeGeneration.GCD
, BenchSuite.CodeGeneration.PopulationCount
, BenchSuite.CodeGeneration.Uninterpreted
, BenchSuite.Crypto.AES
, BenchSuite.Crypto.RC4
, BenchSuite.Crypto.SHA
, BenchSuite.Misc.Auxiliary
, BenchSuite.Misc.Enumerate
, BenchSuite.Misc.Floating
, BenchSuite.Misc.ModelExtract
, BenchSuite.Misc.Newtypes
, BenchSuite.Misc.NoDiv0
, BenchSuite.Misc.Polynomials
, BenchSuite.Misc.SetAlgebra
, BenchSuite.Misc.SoftConstrain
, BenchSuite.Misc.Tuple
, BenchSuite.Lists.BoundedMutex
, BenchSuite.Lists.Fibonacci
, BenchSuite.Lists.Nested
, BenchSuite.Strings.RegexCrossword
, BenchSuite.Strings.SQLInjection
, BenchSuite.Existentials.CRCPolynomial
, BenchSuite.Existentials.Diophantine
, BenchSuite.Transformers.SymbolicEval