Cabal-Version: 2.2 Name : sbv Version : 9.1 x-revision: 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: 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.4.4 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 && < 4.18 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 >= 2, 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.Floating , 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.LadyAndTigers , Documentation.SBV.Examples.Puzzles.MagicSquare , Documentation.SBV.Examples.Puzzles.Murder , Documentation.SBV.Examples.Puzzles.NQueens , Documentation.SBV.Examples.Puzzles.SendMoreMoney , Documentation.SBV.Examples.Puzzles.Sudoku , Documentation.SBV.Examples.Puzzles.U2Bridge , 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.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 , 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.Exceptions , TestSuite.Basics.GenBenchmark , TestSuite.Basics.Higher , TestSuite.Basics.Index , TestSuite.Basics.IteTest , 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 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 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 , hlint, 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