Cabal-Version: 2.2 Name : sbv Version : 10.9 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.8.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.16 && < 5 other-extensions: BangPatterns CPP ConstrainedClassMethods ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFunctor DeriveGeneric DeriveTraversable 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 UndecidableInstances ViewPatterns if impl(ghc >= 8.10.1) ghc-options : -Wunused-packages Library import : common-settings default-language: Haskell2010 build-depends : QuickCheck , containers , array , deepseq , template-haskell , pretty , random , mtl , transformers , async , filepath , text , directory , time , libBF >= 0.6.7 , process , syb , 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.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.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.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.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.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 : 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.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 : base, sbv, process, QuickCheck, filepath, mtl, bytestring, directory , tasty, tasty-quickcheck, tasty-golden, tasty-hunit, deepseq 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 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 : 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.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