sbv-14.3: sbv.cabal
Cabal-Version: 2.2
Name : sbv
Version : 14.3
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-2026
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
SBVTestSuite/TestSuite/CompileTests/SCase/*.hs
SBVTestSuite/TestSuite/CompileTests/SCase/*.stderr
SBVTestSuite/TestSuite/CompileTests/PCase/*.hs
SBVTestSuite/TestSuite/CompileTests/PCase/*.stderr
Extra-Doc-Files : INSTALL, README.md, COPYRIGHT, CHANGES.md
flag doctest_is_running
description: Define this flag during doctest run
default : False
manual : True
flag compile_examples
description: Compile examples for documentation.
default : True
manual : True
source-repository head
type : git
location: https://github.com/LeventErkok/sbv.git
common common-settings
default-language: Haskell2010
ghc-options : -Wall
build-depends : base >= 4.19.2 && < 5
other-extensions: AllowAmbiguousTypes
BangPatterns
CPP
ConstraintKinds
DataKinds
DefaultSignatures
DeriveAnyClass
DeriveDataTypeable
DeriveFunctor
DeriveGeneric
DeriveLift
DeriveTraversable
DerivingStrategies
ExistentialQuantification
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GADTs
GeneralizedNewtypeDeriving
ImplicitParams
InstanceSigs
KindSignatures
LambdaCase
MultiParamTypeClasses
NamedFieldPuns
NegativeLiterals
NumericUnderscores
OverloadedLists
OverloadedRecordDot
OverloadedStrings
PackageImports
ParallelListComp
QuantifiedConstraints
QuasiQuotes
RankNTypes
RecordWildCards
ScopedTypeVariables
StandaloneDeriving
TemplateHaskell
TemplateHaskellQuotes
TupleSections
TypeApplications
TypeFamilies
TypeFamilyDependencies
TypeOperators
UndecidableInstances
ViewPatterns
TypeAbstractions
ghc-options : -Wunused-packages
Library
import : common-settings
if flag(doctest_is_running)
CPP-Options: -DDOCTEST
default-language: Haskell2010
build-depends : QuickCheck
, array
, async
, base16-bytestring
, bytestring
, cryptohash-sha512
, containers
, deepseq
, directory
, filepath
, haskell-src-exts
, haskell-src-meta
, libBF
, mtl
, pretty
, process
, random
, syb
, template-haskell
, th-expand-syns
, text
, time
, transformers
, tree-view
, 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.Tuple
, Data.SBV.RegExp
, Data.SBV.TP
, Data.SBV.Tools.BMC
, Data.SBV.Tools.BVOptimize
, Data.SBV.Tools.Induction
, 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
if flag(compile_examples)
Exposed-modules : Documentation.SBV.Examples.ADT.Expr
, Documentation.SBV.Examples.ADT.Param
, Documentation.SBV.Examples.ADT.Types
, 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.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.SquareBirthday
, 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.TP.Ackermann
, Documentation.SBV.Examples.TP.Basics
, Documentation.SBV.Examples.TP.BinarySearch
, Documentation.SBV.Examples.TP.CaseSplit
, Documentation.SBV.Examples.TP.Coins
, Documentation.SBV.Examples.TP.Collatz
, Documentation.SBV.Examples.TP.ConstFold
, Documentation.SBV.Examples.TP.Countdown
, Documentation.SBV.Examples.TP.Fibonacci
, Documentation.SBV.Examples.TP.GCD
, Documentation.SBV.Examples.TP.InsertionSort
, Documentation.SBV.Examples.TP.Kadane
, Documentation.SBV.Examples.TP.Kleene
, Documentation.SBV.Examples.TP.Lists
, Documentation.SBV.Examples.TP.McCarthy91
, Documentation.SBV.Examples.TP.Majority
, Documentation.SBV.Examples.TP.MergeSort
, Documentation.SBV.Examples.TP.MutualCorecursion
, Documentation.SBV.Examples.TP.NatStream
, Documentation.SBV.Examples.TP.Numeric
, Documentation.SBV.Examples.TP.Peano
, Documentation.SBV.Examples.TP.PigeonHole
, Documentation.SBV.Examples.TP.PowerMod
, Documentation.SBV.Examples.TP.Primes
, Documentation.SBV.Examples.TP.Queue
, Documentation.SBV.Examples.TP.QuickSort
, Documentation.SBV.Examples.TP.RevAcc
, Documentation.SBV.Examples.TP.Reverse
, Documentation.SBV.Examples.TP.RunLength
, Documentation.SBV.Examples.TP.ShefferStroke
, Documentation.SBV.Examples.TP.SortHelpers
, Documentation.SBV.Examples.TP.Sqrt2IsIrrational
, Documentation.SBV.Examples.TP.StrongInduction
, Documentation.SBV.Examples.TP.SumReverse
, Documentation.SBV.Examples.TP.Tao
, Documentation.SBV.Examples.TP.TautologyChecker
, Documentation.SBV.Examples.TP.UpDown
, Documentation.SBV.Examples.TP.VM
, Documentation.SBV.Examples.Transformers.SymbolicEval
, Documentation.SBV.Examples.Uninterpreted.AUF
, Documentation.SBV.Examples.Uninterpreted.Deduce
, Documentation.SBV.Examples.Uninterpreted.EUFLogic
, 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.Core.TH
, 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.SCase
, Data.SBV.SEnum
, 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.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
, Data.SBV.TP.Kernel
, Data.SBV.TP.TP
, Data.SBV.TP.Utils
Test-Suite SBVTest
import : common-settings
default-language : Haskell2010
type : exitcode-stdio-1.0
ghc-options : -with-rtsopts=-K64m
build-depends : Glob
, QuickCheck
, bytestring
, containers
, deepseq
, directory
, filepath
, mtl
, process
, random
, sbv
, tasty
, tasty-golden
, tasty-hunit
, tasty-quickcheck
, temporary
hs-source-dirs : SBVTestSuite
main-is : SBVTest.hs
other-modules : Utils.SBVTestFramework
, TestSuite.ADT.ADT
, TestSuite.ADT.Expr
, TestSuite.ADT.MutRec
, TestSuite.ADT.PExpr
, TestSuite.Arrays.InitVals
, TestSuite.Arrays.Memory
, TestSuite.Arrays.Query
, TestSuite.Arrays.Caching
, TestSuite.Basics.AllSat
, TestSuite.Basics.ArbFloats
, TestSuite.Basics.ArithNoSolver
, TestSuite.Basics.ArithNoSolver2
, TestSuite.Basics.ArithSolver
, TestSuite.Basics.Assert
, TestSuite.Basics.BarrelRotate
, TestSuite.Basics.BasicTests
, 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.TPCaching
, TestSuite.Basics.Set
, TestSuite.Basics.SmtFunctionUnique
, TestSuite.Basics.SmallShifts
, TestSuite.Basics.SquashReals
, TestSuite.Basics.String
, TestSuite.Basics.Sum
, TestSuite.Basics.TOut
, TestSuite.Basics.Tuple
, TestSuite.Basics.UISat
, TestSuite.CRC.CCITT
, TestSuite.CRC.CCITT_Unidir
, TestSuite.CRC.GenPoly
, TestSuite.CRC.Parity
, TestSuite.CRC.USB5
, 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.CompileTests.SCase
, TestSuite.CompileTests.PCase
, 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.Uninterpreted.EUFLogic
, 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 : process, sbv
hs-source-dirs : SBVTestSuite
main-is: SBVDocTest.hs
type: exitcode-stdio-1.0
Test-Suite SBVHLint
import : common-settings
default-language: Haskell2010
build-depends : process
hs-source-dirs : SBVTestSuite
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