Cabal revisions of what4-1.0
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-Name: what4-Version: 1.0-Author: Galois Inc.-Maintainer: jhendrix@galois.com, rdockins@galois.com-Copyright: (c) Galois, Inc 2014-2020-License: BSD3-License-file: LICENSE-Build-type: Simple-Cabal-version: 1.18-Homepage: https://github.com/GaloisInc/what4-Bug-reports: https://github.com/GaloisInc/what4/issues-Tested-with: GHC==8.6.5, GHC==8.8.3, GHC==8.10.1-Category: Formal Methods, Theorem Provers, Symbolic Computation, SMT-Synopsis: Solver-agnostic symbolic values support for issuing queries-Description:- What4 is a generic library for representing values as symbolic formulae which may- contain references to symbolic values, representing unknown variables.- It provides support for communicating with a variety of SAT and SMT solvers,- including Z3, CVC4, Yices, Boolector, STP, and dReal.-- The data representation types make heavy use of GADT-style type indices- to ensure type-correct manipulation of symbolic values.-Extra-doc-files:- README.md- CHANGES.md- doc/README.md- doc/bvdomain.cry- doc/arithdomain.cry- doc/bitsdomain.cry- doc/xordomain.cry--source-repository head- type: git- location: https://github.com/GaloisInc/what4--flag solverTests- description: extra tests that require all the solvers to be installed- manual: True- default: False--flag dRealTestDisable- description: when running solver tests, disable testing using dReal (ignored unless -fsolverTests)- manual: True- default: False--flag STPTestDisable- description: when running solver tests, disable testing using STP (ignored unless -fsolverTests)- manual: True- default: False--library- build-depends:- base >= 4.8 && < 5,- attoparsec >= 0.13,- ansi-wl-pprint >= 0.6.8,- bimap >= 0.2,- bifunctors >= 5,- bv-sized >= 1.0.0,- bytestring >= 0.10,- deriving-compat >= 0.5,- containers >= 0.5.0.0,- data-binary-ieee754,- deepseq >= 1.3,- directory >= 1.2.2,- exceptions >= 0.10,- extra >= 1.6,- filepath >= 1.3,- fingertree >= 0.1.4,- hashable >= 1.3,- hashtables >= 1.2.3,- io-streams >= 1.5,- lens >= 4.18,- mtl >= 2.2.1,- panic >= 0.3,- parameterized-utils >= 2.1 && < 2.2,- process >= 1.2,- scientific >= 0.3.6,- temporary >= 1.2,- template-haskell,- text >= 1.1,- th-abstraction >=0.1 && <0.4,- transformers >= 0.4,- unordered-containers >= 0.2.10,- utf8-string >= 1.0.1,- vector >= 0.12.1,- versions >= 3.5.2,- zenc >= 0.1.0 && < 0.2.0,- ghc-prim >= 0.5.3-- default-language: Haskell2010- default-extensions:- NondecreasingIndentation-- hs-source-dirs: src-- exposed-modules:- What4.BaseTypes- What4.Concrete- What4.Config- What4.FunctionName- What4.IndexLit- What4.Interface- What4.InterpretedFloatingPoint- What4.LabeledPred- What4.Panic- What4.Partial- What4.ProblemFeatures- What4.ProgramLoc- What4.SatResult- What4.SemiRing- What4.Symbol- What4.SWord- What4.WordMap-- What4.Expr- What4.Expr.ArrayUpdateMap- What4.Expr.AppTheory- What4.Expr.BoolMap- What4.Expr.Builder- What4.Expr.GroundEval- What4.Expr.MATLAB- What4.Expr.Simplify- What4.Expr.StringSeq- What4.Expr.VarIdentification- What4.Expr.WeightedSum- What4.Expr.UnaryBV-- What4.Solver- What4.Solver.Adapter- What4.Solver.Boolector- What4.Solver.CVC4- What4.Solver.DReal- What4.Solver.STP- What4.Solver.Yices- What4.Solver.Z3-- What4.Protocol.Online- What4.Protocol.SMTLib2- What4.Protocol.SMTLib2.Parse- What4.Protocol.SMTLib2.Syntax- What4.Protocol.SMTWriter- What4.Protocol.ReadDecimal- What4.Protocol.SExp- What4.Protocol.PolyRoot-- What4.Utils.AbstractDomains- What4.Utils.AnnotatedMap- What4.Utils.Arithmetic- What4.Utils.BVDomain- What4.Utils.BVDomain.Arith- What4.Utils.BVDomain.Bitwise- What4.Utils.BVDomain.XOR- What4.Utils.Complex- What4.Utils.Endian- What4.Utils.Environment- What4.Utils.HandleReader- What4.Utils.IncrHash- What4.Utils.LeqMap- What4.Utils.MonadST- What4.Utils.OnlyNatRepr- What4.Utils.Process- What4.Utils.Streams- What4.Utils.StringLiteral- What4.Utils.Word16String-- Test.Verification-- other-modules:- What4.Expr.App-- ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns- ghc-prof-options: -fprof-auto-top- if impl(ghc >= 8.6)- default-extensions: NoStarIsType--executable quickstart- main-is: doc/QuickStart.hs- default-language: Haskell2010-- build-depends:- base,- parameterized-utils,- what4--test-suite adapter-test- type: exitcode-stdio-1.0- default-language: Haskell2010-- hs-source-dirs: test- main-is: AdapterTest.hs-- if flag(solverTests)- buildable: True- if ! flag(dRealTestDisable)- cpp-options: -DTEST_DREAL- if ! flag(STPTestDisable)- cpp-options: -DTEST_STP- else- buildable: False-- build-depends:- base,- bv-sized,- bytestring,- containers,- data-binary-ieee754,- lens,- parameterized-utils,- process,- tasty >= 0.10,- tasty-hunit >= 0.9,- text,- versions,- what4-- ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns--test-suite online-solver-test- type: exitcode-stdio-1.0- default-language: Haskell2010-- hs-source-dirs: test- main-is: OnlineSolverTest.hs-- if flag(solverTests)- buildable: True- if ! flag(STPTestDisable)- cpp-options: -DTEST_STP- else- buildable: False-- build-depends:- base,- bv-sized,- bytestring,- containers,- data-binary-ieee754,- lens,- parameterized-utils,- process,- tasty >= 0.10,- tasty-hunit >= 0.9,- text,- versions,- what4-- ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns--test-suite expr-builder-smtlib2- type: exitcode-stdio-1.0- default-language: Haskell2010-- hs-source-dirs: test- main-is: ExprBuilderSMTLib2.hs-- build-depends:- base,- bv-sized,- bytestring,- containers,- data-binary-ieee754,- parameterized-utils,- tasty >= 0.10,- tasty-hunit >= 0.9,- text,- versions,- what4-- ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns--test-suite exprs_tests- type: exitcode-stdio-1.0- default-language: Haskell2010-- hs-source-dirs: test- main-is: ExprsTest.hs-- other-modules:- GenWhat4Expr-- build-depends: base- , bv-sized- , hedgehog >= 1.0.2- , parameterized-utils- , tasty >= 0.10- , tasty-hunit >= 0.9- , tasty-hedgehog- , what4-- ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns--test-suite iteexprs_tests- type: exitcode-stdio-1.0- default-language: Haskell2010-- hs-source-dirs: test- main-is: IteExprs.hs-- other-modules:- GenWhat4Expr-- build-depends: base- , bv-sized- , hedgehog >= 1.0.2- , parameterized-utils- , tasty >= 0.10- , tasty-hunit >= 0.9- , tasty-hedgehog- , what4-- ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns--test-suite bvdomain_tests- type: exitcode-stdio-1.0- default-language: Haskell2010-- hs-source-dirs: test, test/QC- main-is: BVDomTests.hs-- other-modules: VerifyBindings-- build-depends: base- , parameterized-utils- , tasty >= 0.10- , tasty-quickcheck >= 0.10- , QuickCheck >= 2.12- , transformers- , what4-- ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns--test-suite bvdomain_tests_hh- type: exitcode-stdio-1.0- default-language: Haskell2010-- hs-source-dirs: test, test/HH- main-is: BVDomTests.hs-- other-modules: VerifyBindings-- build-depends: base- , parameterized-utils- , tasty >= 0.10- , tasty-hedgehog- , hedgehog >= 1.0.2- , transformers- , what4-- ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns+Name: what4 +Version: 1.0 +x-revision: 1 +Author: Galois Inc. +Maintainer: jhendrix@galois.com, rdockins@galois.com +Copyright: (c) Galois, Inc 2014-2020 +License: BSD3 +License-file: LICENSE +Build-type: Simple +Cabal-version: 1.18 +Homepage: https://github.com/GaloisInc/what4 +Bug-reports: https://github.com/GaloisInc/what4/issues +Tested-with: GHC==8.6.5, GHC==8.8.3, GHC==8.10.1 +Category: Formal Methods, Theorem Provers, Symbolic Computation, SMT +Synopsis: Solver-agnostic symbolic values support for issuing queries +Description: + What4 is a generic library for representing values as symbolic formulae which may + contain references to symbolic values, representing unknown variables. + It provides support for communicating with a variety of SAT and SMT solvers, + including Z3, CVC4, Yices, Boolector, STP, and dReal. + + The data representation types make heavy use of GADT-style type indices + to ensure type-correct manipulation of symbolic values. +Extra-doc-files: + README.md + CHANGES.md + doc/README.md + doc/bvdomain.cry + doc/arithdomain.cry + doc/bitsdomain.cry + doc/xordomain.cry + +source-repository head + type: git + location: https://github.com/GaloisInc/what4 + +flag solverTests + description: extra tests that require all the solvers to be installed + manual: True + default: False + +flag dRealTestDisable + description: when running solver tests, disable testing using dReal (ignored unless -fsolverTests) + manual: True + default: False + +flag STPTestDisable + description: when running solver tests, disable testing using STP (ignored unless -fsolverTests) + manual: True + default: False + +library + build-depends: + base >= 4.8 && < 5, + attoparsec >= 0.13, + ansi-wl-pprint >= 0.6.8, + bimap >= 0.2, + bifunctors >= 5, + bv-sized >= 1.0.0, + bytestring >= 0.10, + deriving-compat >= 0.5, + containers >= 0.5.0.0, + data-binary-ieee754, + deepseq >= 1.3, + directory >= 1.2.2, + exceptions >= 0.10, + extra >= 1.6, + filepath >= 1.3, + fingertree >= 0.1.4, + hashable >= 1.3, + hashtables >= 1.2.3, + io-streams >= 1.5, + lens >= 4.18, + mtl >= 2.2.1, + panic >= 0.3, + parameterized-utils >= 2.1 && < 2.2, + process >= 1.2, + scientific >= 0.3.6, + temporary >= 1.2, + template-haskell, + text >= 1.1, + th-abstraction >=0.1 && <0.4, + transformers >= 0.4, + unordered-containers >= 0.2.10, + utf8-string >= 1.0.1, + vector >= 0.12.1, + versions >= 3.5.2 && < 4.0, + zenc >= 0.1.0 && < 0.2.0, + ghc-prim >= 0.5.3 + + default-language: Haskell2010 + default-extensions: + NondecreasingIndentation + + hs-source-dirs: src + + exposed-modules: + What4.BaseTypes + What4.Concrete + What4.Config + What4.FunctionName + What4.IndexLit + What4.Interface + What4.InterpretedFloatingPoint + What4.LabeledPred + What4.Panic + What4.Partial + What4.ProblemFeatures + What4.ProgramLoc + What4.SatResult + What4.SemiRing + What4.Symbol + What4.SWord + What4.WordMap + + What4.Expr + What4.Expr.ArrayUpdateMap + What4.Expr.AppTheory + What4.Expr.BoolMap + What4.Expr.Builder + What4.Expr.GroundEval + What4.Expr.MATLAB + What4.Expr.Simplify + What4.Expr.StringSeq + What4.Expr.VarIdentification + What4.Expr.WeightedSum + What4.Expr.UnaryBV + + What4.Solver + What4.Solver.Adapter + What4.Solver.Boolector + What4.Solver.CVC4 + What4.Solver.DReal + What4.Solver.STP + What4.Solver.Yices + What4.Solver.Z3 + + What4.Protocol.Online + What4.Protocol.SMTLib2 + What4.Protocol.SMTLib2.Parse + What4.Protocol.SMTLib2.Syntax + What4.Protocol.SMTWriter + What4.Protocol.ReadDecimal + What4.Protocol.SExp + What4.Protocol.PolyRoot + + What4.Utils.AbstractDomains + What4.Utils.AnnotatedMap + What4.Utils.Arithmetic + What4.Utils.BVDomain + What4.Utils.BVDomain.Arith + What4.Utils.BVDomain.Bitwise + What4.Utils.BVDomain.XOR + What4.Utils.Complex + What4.Utils.Endian + What4.Utils.Environment + What4.Utils.HandleReader + What4.Utils.IncrHash + What4.Utils.LeqMap + What4.Utils.MonadST + What4.Utils.OnlyNatRepr + What4.Utils.Process + What4.Utils.Streams + What4.Utils.StringLiteral + What4.Utils.Word16String + + Test.Verification + + other-modules: + What4.Expr.App + + ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns + ghc-prof-options: -fprof-auto-top + if impl(ghc >= 8.6) + default-extensions: NoStarIsType + +executable quickstart + main-is: doc/QuickStart.hs + default-language: Haskell2010 + + build-depends: + base, + parameterized-utils, + what4 + +test-suite adapter-test + type: exitcode-stdio-1.0 + default-language: Haskell2010 + + hs-source-dirs: test + main-is: AdapterTest.hs + + if flag(solverTests) + buildable: True + if ! flag(dRealTestDisable) + cpp-options: -DTEST_DREAL + if ! flag(STPTestDisable) + cpp-options: -DTEST_STP + else + buildable: False + + build-depends: + base, + bv-sized, + bytestring, + containers, + data-binary-ieee754, + lens, + parameterized-utils, + process, + tasty >= 0.10, + tasty-hunit >= 0.9, + text, + versions, + what4 + + ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns + +test-suite online-solver-test + type: exitcode-stdio-1.0 + default-language: Haskell2010 + + hs-source-dirs: test + main-is: OnlineSolverTest.hs + + if flag(solverTests) + buildable: True + if ! flag(STPTestDisable) + cpp-options: -DTEST_STP + else + buildable: False + + build-depends: + base, + bv-sized, + bytestring, + containers, + data-binary-ieee754, + lens, + parameterized-utils, + process, + tasty >= 0.10, + tasty-hunit >= 0.9, + text, + versions, + what4 + + ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns + +test-suite expr-builder-smtlib2 + type: exitcode-stdio-1.0 + default-language: Haskell2010 + + hs-source-dirs: test + main-is: ExprBuilderSMTLib2.hs + + build-depends: + base, + bv-sized, + bytestring, + containers, + data-binary-ieee754, + parameterized-utils, + tasty >= 0.10, + tasty-hunit >= 0.9, + text, + versions, + what4 + + ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns + +test-suite exprs_tests + type: exitcode-stdio-1.0 + default-language: Haskell2010 + + hs-source-dirs: test + main-is: ExprsTest.hs + + other-modules: + GenWhat4Expr + + build-depends: base + , bv-sized + , hedgehog >= 1.0.2 + , parameterized-utils + , tasty >= 0.10 + , tasty-hunit >= 0.9 + , tasty-hedgehog + , what4 + + ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns + +test-suite iteexprs_tests + type: exitcode-stdio-1.0 + default-language: Haskell2010 + + hs-source-dirs: test + main-is: IteExprs.hs + + other-modules: + GenWhat4Expr + + build-depends: base + , bv-sized + , hedgehog >= 1.0.2 + , parameterized-utils + , tasty >= 0.10 + , tasty-hunit >= 0.9 + , tasty-hedgehog + , what4 + + ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns + +test-suite bvdomain_tests + type: exitcode-stdio-1.0 + default-language: Haskell2010 + + hs-source-dirs: test, test/QC + main-is: BVDomTests.hs + + other-modules: VerifyBindings + + build-depends: base + , parameterized-utils + , tasty >= 0.10 + , tasty-quickcheck >= 0.10 + , QuickCheck >= 2.12 + , transformers + , what4 + + ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns + +test-suite bvdomain_tests_hh + type: exitcode-stdio-1.0 + default-language: Haskell2010 + + hs-source-dirs: test, test/HH + main-is: BVDomTests.hs + + other-modules: VerifyBindings + + build-depends: base + , parameterized-utils + , tasty >= 0.10 + , tasty-hedgehog + , hedgehog >= 1.0.2 + , transformers + , what4 + + ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
revision 2
Name: what4 Version: 1.0 -x-revision: 1 +x-revision: 2 Author: Galois Inc. Maintainer: jhendrix@galois.com, rdockins@galois.com Copyright: (c) Galois, Inc 2014-2020 extra >= 1.6, filepath >= 1.3, fingertree >= 0.1.4, - hashable >= 1.3, + hashable >= 1.3 && < 1.4, hashtables >= 1.2.3, io-streams >= 1.5, lens >= 4.18,