Cabal-Version: 2.2 Name : sbv Version : 8.8 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-2020 License : BSD-3-Clause License-file : LICENSE Stability : Experimental Author : Levent Erkok Homepage : http://leventerkok.github.com/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==8.10.2, GHC==8.8.4 source-repository head type: git location: git://github.com/LeventErkok/sbv.git -- On build-bots, building HLint takes inordinately long and times out. So -- we use this flag to skip that build. flag skipHLintTester description: Do not build the HLint tester default : False manual : True 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 : crackNum , QuickCheck, template-haskell , array, async, containers, deepseq, directory, filepath, time , pretty, process, mtl, random, syb, transformers Exposed-modules : Data.SBV , Data.SBV.Control , Data.SBV.Dynamic , Data.SBV.Either , Data.SBV.Internals , Data.SBV.List , Data.SBV.Maybe , Data.SBV.Set , Data.SBV.String , Data.SBV.Tuple , Data.SBV.Char , 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.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.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.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.Boolector , Data.SBV.Provers.CVC4 , Data.SBV.Provers.Yices , Data.SBV.Provers.DReal , Data.SBV.Provers.Z3 , Data.SBV.Provers.MathSAT , Data.SBV.Provers.ABC , 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, crackNum , 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.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.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 if flag(skipHLintTester) buildable: False 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, crackNum , 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, crackNum , 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