Cabal-Version: 2.2 Name : sbv Version : 8.17 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-2021 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.0.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 && < 4.16 if impl(ghc >= 8.10.1) ghc-options : -Wunused-packages Library import : common-settings 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.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.Birthday , Documentation.SBV.Examples.Puzzles.Coins , Documentation.SBV.Examples.Puzzles.Counts , Documentation.SBV.Examples.Puzzles.DogCatMouse , Documentation.SBV.Examples.Puzzles.Euler185 , Documentation.SBV.Examples.Puzzles.Fish , Documentation.SBV.Examples.Puzzles.Garden , Documentation.SBV.Examples.Puzzles.HexPuzzle , 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 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.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 build-depends : sbv hs-source-dirs : SBVTestSuite main-is : SBVConnectionTest.hs type: exitcode-stdio-1.0 Test-Suite SBVDocTest import : common-settings build-depends : base, directory, filepath, random , doctest, Glob, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck, random, sbv 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 build-depends : base, directory, filepath, random , 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 SBVBenchmark import : common-settings 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, syb, text, sbv, directory, random, mtl, containers, time , gauge, process, deepseq, bench-show, silently hs-source-dirs : SBVBenchSuite main-is : SBVBenchmark.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 Benchmark SBVBench import : common-settings 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, syb, text, sbv, directory, random, mtl, containers, time , gauge, process, deepseq, silently, bench-show 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