Name: sbv Version: 7.12 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-2018 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 other-extensions: BangPatterns DefaultSignatures DeriveAnyClass DeriveDataTypeable FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving MultiParamTypeClasses OverlappingInstances ParallelListComp PatternGuards Rank2Types RankNTypes ScopedTypeVariables StandaloneDeriving TemplateHaskell TupleSections TypeOperators TypeSynonymInstances Build-Depends : base >= 4.9 && < 4.13 , crackNum >= 2.2 , ghc, QuickCheck, template-haskell , array, async, containers, deepseq, directory, filepath, time , pretty, process, mtl, random, syb, reinterpret-cast , generic-deriving Exposed-modules : Data.SBV , Data.SBV.Control , Data.SBV.Dynamic , Data.SBV.Internals , Data.SBV.List , Data.SBV.List.Bounded , Data.SBV.String , Data.SBV.Char , Data.SBV.RegExp , Data.SBV.Tools.CodeGen , Data.SBV.Tools.GenTest , Data.SBV.Tools.Overflow , Data.SBV.Tools.Polynomial , Data.SBV.Tools.STree , 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.SoftConstrain , Documentation.SBV.Examples.Misc.Word4 , Documentation.SBV.Examples.Optimization.LinearOpt , Documentation.SBV.Examples.Optimization.Production , Documentation.SBV.Examples.Optimization.VM , Documentation.SBV.Examples.Optimization.ExtField , 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.HexPuzzle , 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.Uninterpreted.AUF , Documentation.SBV.Examples.Uninterpreted.Deduce , Documentation.SBV.Examples.Uninterpreted.Function , Documentation.SBV.Examples.Uninterpreted.Shannon , Documentation.SBV.Examples.Uninterpreted.Sort , Documentation.SBV.Examples.Uninterpreted.UISortAllSat Other-modules : 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.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.Boolean , 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 other-extensions: DeriveAnyClass , DeriveDataTypeable , Rank2Types , ScopedTypeVariables Build-depends : base >= 4.9, reinterpret-cast, filepath, syb , 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.BasicTests , TestSuite.Basics.Exceptions , TestSuite.Basics.GenBenchmark , TestSuite.Basics.Higher , TestSuite.Basics.Index , TestSuite.Basics.IteTest , TestSuite.Basics.ProofTests , TestSuite.Basics.PseudoBoolean , TestSuite.Basics.QRem , TestSuite.Basics.Quantifiers , TestSuite.Basics.Recursive , TestSuite.Basics.SmallShifts , TestSuite.Basics.SquashReals , TestSuite.Basics.String , TestSuite.Basics.List , TestSuite.Basics.TOut , 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.Quantified , TestSuite.Optimization.Reals , TestSuite.Optimization.NoOpt , 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.Uninterpreted , TestSuite.QuickCheck.QC , 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 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 default-language: Haskell2010 hs-source-dirs: SBVTestSuite Other-modules : Utils.SBVTestFramework main-is: SBVHLint.hs type: exitcode-stdio-1.0