Cabal revisions of sbv-9.1
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-Cabal-Version: 2.2--Name : sbv-Version : 9.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: <http://leventerkok.github.io/sbv/>--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 && < 5-- 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, 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+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: <http://leventerkok.github.io/sbv/> + +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