Name: sbv Version: 8.2 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-2019 License: BSD3 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 Cabal-Version: 1.14 Data-Files: SBVTestSuite/GoldFiles/*.gold Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md source-repository head type: git location: git://github.com/LeventErkok/sbv.git Library default-language: Haskell2010 ghc-options : -Wall -O2 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 : base >= 4.9 && < 5 , crackNum >= 2.3 , ghc, QuickCheck, template-haskell , array, async, containers, deepseq, directory, filepath, time , pretty, process, mtl, random, syb, transformers , generic-deriving 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.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.Polynomials , Documentation.SBV.Examples.Misc.SetAlgebra , Documentation.SBV.Examples.Misc.SoftConstrain , Documentation.SBV.Examples.Misc.Tuple , Documentation.SBV.Examples.Misc.Word4 , 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.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.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.Splittable , 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.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 type : exitcode-stdio-1.0 default-language: Haskell2010 ghc-options : -Wall -with-rtsopts=-K64m -O2 other-extensions: DataKinds DeriveAnyClass DeriveDataTypeable FlexibleContexts GeneralizedNewtypeDeriving OverloadedLists OverloadedStrings Rank2Types RankNTypes ScopedTypeVariables StandaloneDeriving TemplateHaskell TupleSections TypeApplications Build-depends : base >= 4.9, filepath, syb, crackNum >= 2.3 , sbv, directory, random, mtl, containers , template-haskell, 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.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.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.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.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 SBVDocTest Build-Depends: base, directory, filepath, random , doctest, Glob, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck, random , sbv ghc-options : -Wall -O2 other-extensions: DataKinds DeriveAnyClass DeriveDataTypeable FlexibleContexts GeneralizedNewtypeDeriving OverloadedLists OverloadedStrings Rank2Types RankNTypes ScopedTypeVariables StandaloneDeriving TemplateHaskell TupleSections TypeApplications default-language: Haskell2010 Hs-Source-Dirs : SBVTestSuite main-is: SBVDocTest.hs Other-modules : Utils.SBVTestFramework type: exitcode-stdio-1.0 Test-Suite SBVHLint build-depends: base, directory, filepath, random , hlint, bytestring, tasty, tasty-golden, tasty-hunit, tasty-quickcheck, mtl, QuickCheck , sbv ghc-options : -Wall -O2 other-extensions: DataKinds DeriveAnyClass DeriveDataTypeable FlexibleContexts GeneralizedNewtypeDeriving OverloadedLists OverloadedStrings Rank2Types RankNTypes ScopedTypeVariables StandaloneDeriving TemplateHaskell TupleSections TypeApplications default-language: Haskell2010 hs-source-dirs: SBVTestSuite Other-modules : Utils.SBVTestFramework main-is: SBVHLint.hs type: exitcode-stdio-1.0