sbv-11.0: sbv.cabal
Cabal-Version: 2.2
Name : sbv
Version : 11.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.
Copyright : Levent Erkok, 2010-2024
License : BSD-3-Clause
License-file : LICENSE
Stability : Experimental
Author : Levent Erkok
Homepage : http://github.com/LeventErkok/sbv
Bug-reports : http://github.com/LeventErkok/sbv/issues
Maintainer : Levent Erkok (erkokl@gmail.com)
Build-Type : Simple
Data-Files : SBVTestSuite/GoldFiles/*.gold
Extra-Doc-Files : INSTALL, README.md, COPYRIGHT, CHANGES.md
Tested-With : GHC==9.10.1
source-repository head
type: git
location: git://github.com/LeventErkok/sbv.git
common common-settings
default-language: Haskell2010
ghc-options : -Wall
build-depends : base >= 4.19 && < 5
other-extensions: BangPatterns
CPP
ConstrainedClassMethods
ConstraintKinds
DataKinds
DefaultSignatures
DeriveAnyClass
DeriveDataTypeable
DeriveFunctor
DeriveGeneric
DeriveTraversable
DerivingStrategies
ExistentialQuantification
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GADTs
GeneralizedNewtypeDeriving
ImplicitParams
InstanceSigs
KindSignatures
LambdaCase
MultiParamTypeClasses
NamedFieldPuns
NegativeLiterals
OverloadedLists
OverloadedRecordDot
OverloadedStrings
PackageImports
ParallelListComp
PatternGuards
QuantifiedConstraints
QuasiQuotes
Rank2Types
RankNTypes
RecordWildCards
ScopedTypeVariables
StandaloneDeriving
TemplateHaskell
TupleSections
TypeApplications
TypeFamilies
TypeOperators
TypeSynonymInstances
UndecidableInstances
ViewPatterns
if impl(ghc >= 9.8.1)
other-extensions: TypeAbstractions
if impl(ghc >= 8.10.1)
ghc-options : -Wunused-packages
Library
import : common-settings
default-language: Haskell2010
build-depends : QuickCheck
, array
, async >= 2.2.5
, containers
, deepseq
, directory
, filepath
, libBF >= 0.6.8
, mtl
, pretty
, process
, random
, syb
, template-haskell
, text
, time
, transformers
, uniplate
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.BVOptimize
, Data.SBV.Tools.Induction
, Data.SBV.Tools.BoundedFix
, Data.SBV.Tools.CodeGen
, Data.SBV.Tools.GenTest
, Data.SBV.Tools.KnuckleDragger
, Data.SBV.Tools.NaturalInduction
, 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.PEXT_PDEP
, 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.Prince
, Documentation.SBV.Examples.Crypto.SHA
, Documentation.SBV.Examples.DeltaSat.DeltaSat
, Documentation.SBV.Examples.Existentials.Diophantine
, Documentation.SBV.Examples.Lists.Fibonacci
, Documentation.SBV.Examples.Lists.BoundedMutex
, Documentation.SBV.Examples.Lists.CountOutAndTransfer
, Documentation.SBV.Examples.KnuckleDragger.AppendRev
, Documentation.SBV.Examples.KnuckleDragger.Basics
, Documentation.SBV.Examples.KnuckleDragger.CaseSplit
, Documentation.SBV.Examples.KnuckleDragger.Kleene
, Documentation.SBV.Examples.KnuckleDragger.Induction
, Documentation.SBV.Examples.KnuckleDragger.ListLen
, Documentation.SBV.Examples.KnuckleDragger.RevLen
, Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational
, Documentation.SBV.Examples.KnuckleDragger.Tao
, 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.ProgramPaths
, 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.AddHorn
, 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.DieHard
, 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.Newspaper
, 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.Tower
, 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.OpenSMT
, Data.SBV.Provers.Yices
, Data.SBV.Provers.Z3
, Data.SBV.Tools.KDKernel
, Data.SBV.Tools.KDUtils
, 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
build-depends : QuickCheck
, bytestring
, containers
, deepseq
, directory
, filepath
, mtl
, random
, sbv
, tasty
, tasty-golden
, tasty-hunit
, tasty-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.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.ArrayGetVal
, 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 : QuickCheck
, bytestring
, deepseq
, directory
, filepath
, mtl
, process
, sbv
, tasty
, tasty-golden
, tasty-hunit
, tasty-quickcheck
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 : QuickCheck
, bytestring
, deepseq
, directory
, filepath
, mtl
, process
, sbv
, tasty
, tasty-golden
, tasty-hunit
, tasty-quickcheck
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
build-depends : deepseq
, filepath
, process
, random
, sbv
, tasty
, tasty-bench
, time
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.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.Strings.RegexCrossword
, BenchSuite.Strings.SQLInjection
, BenchSuite.Existentials.Diophantine
, BenchSuite.Transformers.SymbolicEval