Cabal revisions of what4-1.2.1
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-Cabal-version: 2.4-Name: what4-Version: 1.2.1-Author: Galois Inc.-Maintainer: jhendrix@galois.com, rdockins@galois.com-Copyright: (c) Galois, Inc 2014-2021-License: BSD-3-Clause-License-file: LICENSE-Build-type: Simple-Homepage: https://github.com/GaloisInc/what4-Bug-reports: https://github.com/GaloisInc/what4/issues-Tested-with: GHC==8.6.5, GHC==8.8.4, GHC==8.10.4, GHC==9.0.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.--data-files: solverBounds.config--Extra-source-files:- test/responses/*.exp- test/responses/*.rsp--Extra-doc-files:- README.md- CHANGES.md- doc/README.md- doc/implementation.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--common bldflags- default-language: Haskell2010- ghc-options: -Wall- -Werror=incomplete-patterns- -Werror=missing-methods- -Werror=overlapping-patterns- -Wcompat- -Wpartial-fields--common testdefs- hs-source-dirs: test- build-depends: base- , parameterized-utils- , tasty >= 0.10- , what4--common testdefs-quickcheck- import: testdefs- build-depends: tasty-quickcheck >= 0.10- , QuickCheck >= 2.12--common testdefs-hedgehog- import: testdefs- build-depends: hedgehog >= 1.0.2- , tasty-hedgehog--common testdefs-hunit- import: testdefs- build-depends: tasty-hunit >= 0.9--library- import: bldflags- build-depends:- base >= 4.8 && < 5,- attoparsec >= 0.13,- bimap >= 0.2,- bifunctors >= 5,- bv-sized >= 1.0.0,- bytestring >= 0.10,- deriving-compat >= 0.5,- config-value >= 0.8 && < 0.9,- 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,- libBF >= 0.6 && < 0.7,- mtl >= 2.2.1,- panic >= 0.3,- parameterized-utils >= 2.1 && < 2.2,- prettyprinter >= 1.7.0,- process >= 1.2,- scientific >= 0.3.6,- temporary >= 1.2,- template-haskell,- text >= 1.2.4.0 && < 1.3,- th-abstraction >=0.1 && <0.5,- th-lift >= 0.8.2 && < 0.9,- th-lift-instances >= 0.1 && < 0.2,- transformers >= 0.4,- unordered-containers >= 0.2.10,- utf8-string >= 1.0.1,- vector >= 0.12.1,- versions >= 4.0 && < 6.0,- zenc >= 0.1.0 && < 0.2.0,- ghc-prim >= 0.5.2-- 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.SFloat- What4.SWord- What4.WordMap-- What4.Expr- What4.Expr.App- 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.ExternalABC- What4.Solver.STP- What4.Solver.Yices- What4.Solver.Z3-- What4.Protocol.Online- What4.Protocol.SMTLib2- What4.Protocol.SMTLib2.Parse- What4.Protocol.SMTLib2.Response- What4.Protocol.SMTLib2.Syntax- What4.Protocol.SMTWriter- What4.Protocol.ReadDecimal- What4.Protocol.SExp- What4.Protocol.PolyRoot- What4.Protocol.VerilogWriter- What4.Protocol.VerilogWriter.AST- What4.Protocol.VerilogWriter.ABCVerilog- What4.Protocol.VerilogWriter.Backend-- 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.FloatHelpers- What4.Utils.LeqMap- What4.Utils.MonadST- What4.Utils.OnlyIntRepr- What4.Utils.Process- What4.Utils.Streams- What4.Utils.StringLiteral- What4.Utils.Word16String- What4.Utils.Versions-- Test.Verification-- 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- import: bldflags, testdefs-hunit- type: exitcode-stdio-1.0-- 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:- bv-sized,- bytestring,- containers,- data-binary-ieee754,- lens,- mtl >= 2.2.1,- process,- text,- versions--test-suite config-test- import: bldflags, testdefs-hunit- type: exitcode-stdio-1.0- main-is: ConfigTest.hs- build-depends: containers- , parameterized-utils- , prettyprinter- , tasty-checklist >= 1.0 && < 1.1- , text--test-suite online-solver-test- import: bldflags, testdefs-hunit- type: exitcode-stdio-1.0-- main-is: OnlineSolverTest.hs-- if flag(solverTests)- buildable: True- if ! flag(STPTestDisable)- cpp-options: -DTEST_STP- else- buildable: False-- build-depends:- bv-sized,- bytestring,- containers,- data-binary-ieee754,- lens,- process,- text,- versions--test-suite expr-builder-smtlib2- import: bldflags, testdefs-hunit- type: exitcode-stdio-1.0-- main-is: ExprBuilderSMTLib2.hs-- build-depends:- bv-sized,- bytestring,- containers,- data-binary-ieee754,- libBF,- text,- versions---test-suite exprs_tests- import: bldflags, testdefs-hedgehog, testdefs-hunit- type: exitcode-stdio-1.0-- main-is: ExprsTest.hs-- other-modules:- GenWhat4Expr-- build-depends: bv-sized---test-suite iteexprs_tests- import: bldflags, testdefs-hedgehog, testdefs-hunit- type: exitcode-stdio-1.0-- main-is: IteExprs.hs-- other-modules:- GenWhat4Expr-- build-depends: bv-sized- , containers >= 0.5.0.0---test-suite bvdomain_tests- import: bldflags, testdefs-quickcheck- type: exitcode-stdio-1.0-- hs-source-dirs: test/QC- main-is: BVDomTests.hs-- other-modules: VerifyBindings-- build-depends: transformers---test-suite bvdomain_tests_hh- import: bldflags, testdefs-hedgehog- type: exitcode-stdio-1.0-- hs-source-dirs: test/HH- main-is: BVDomTests.hs-- other-modules: VerifyBindings-- build-depends: transformers---test-suite template_tests- import: bldflags, testdefs-hedgehog- type: exitcode-stdio-1.0- main-is : TestTemplate.hs- build-depends: bv-sized- , libBF- , transformers---test-suite solver_parsing_tests- import: bldflags, testdefs-hunit- type: exitcode-stdio-1.0- main-is : SolverParserTest.hs- build-depends: contravariant- , exceptions- , io-streams- , lumberjack- , tasty-sugar >= 1.1 && < 1.2- , text+Cabal-version: 2.4 +Name: what4 +Version: 1.2.1 +x-revision: 1 +Author: Galois Inc. +Maintainer: jhendrix@galois.com, rdockins@galois.com +Copyright: (c) Galois, Inc 2014-2021 +License: BSD-3-Clause +License-file: LICENSE +Build-type: Simple +Homepage: https://github.com/GaloisInc/what4 +Bug-reports: https://github.com/GaloisInc/what4/issues +Tested-with: GHC==8.6.5, GHC==8.8.4, GHC==8.10.4, GHC==9.0.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. + +data-files: solverBounds.config + +Extra-source-files: + test/responses/*.exp + test/responses/*.rsp + +Extra-doc-files: + README.md + CHANGES.md + doc/README.md + doc/implementation.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 + +common bldflags + default-language: Haskell2010 + ghc-options: -Wall + -Werror=incomplete-patterns + -Werror=missing-methods + -Werror=overlapping-patterns + -Wcompat + -Wpartial-fields + +common testdefs + hs-source-dirs: test + build-depends: base + , parameterized-utils + , tasty >= 0.10 + , what4 + +common testdefs-quickcheck + import: testdefs + build-depends: tasty-quickcheck >= 0.10 + , QuickCheck >= 2.12 + +common testdefs-hedgehog + import: testdefs + build-depends: hedgehog >= 1.0.2 + , tasty-hedgehog + +common testdefs-hunit + import: testdefs + build-depends: tasty-hunit >= 0.9 + +library + import: bldflags + build-depends: + base >= 4.8 && < 5, + attoparsec >= 0.13, + bimap >= 0.2, + bifunctors >= 5, + bv-sized >= 1.0.0, + bytestring >= 0.10, + deriving-compat >= 0.5, + config-value >= 0.8 && < 0.9, + 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 && < 1.4, + hashtables >= 1.2.3, + io-streams >= 1.5, + lens >= 4.18, + libBF >= 0.6 && < 0.7, + mtl >= 2.2.1, + panic >= 0.3, + parameterized-utils >= 2.1 && < 2.2, + prettyprinter >= 1.7.0, + process >= 1.2, + scientific >= 0.3.6, + temporary >= 1.2, + template-haskell, + text >= 1.2.4.0 && < 1.3, + th-abstraction >=0.1 && <0.5, + th-lift >= 0.8.2 && < 0.9, + th-lift-instances >= 0.1 && < 0.2, + transformers >= 0.4, + unordered-containers >= 0.2.10, + utf8-string >= 1.0.1, + vector >= 0.12.1, + versions >= 4.0 && < 6.0, + zenc >= 0.1.0 && < 0.2.0, + ghc-prim >= 0.5.2 + + 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.SFloat + What4.SWord + What4.WordMap + + What4.Expr + What4.Expr.App + 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.ExternalABC + What4.Solver.STP + What4.Solver.Yices + What4.Solver.Z3 + + What4.Protocol.Online + What4.Protocol.SMTLib2 + What4.Protocol.SMTLib2.Parse + What4.Protocol.SMTLib2.Response + What4.Protocol.SMTLib2.Syntax + What4.Protocol.SMTWriter + What4.Protocol.ReadDecimal + What4.Protocol.SExp + What4.Protocol.PolyRoot + What4.Protocol.VerilogWriter + What4.Protocol.VerilogWriter.AST + What4.Protocol.VerilogWriter.ABCVerilog + What4.Protocol.VerilogWriter.Backend + + 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.FloatHelpers + What4.Utils.LeqMap + What4.Utils.MonadST + What4.Utils.OnlyIntRepr + What4.Utils.Process + What4.Utils.Streams + What4.Utils.StringLiteral + What4.Utils.Word16String + What4.Utils.Versions + + Test.Verification + + 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 + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + + 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: + bv-sized, + bytestring, + containers, + data-binary-ieee754, + lens, + mtl >= 2.2.1, + process, + text, + versions + +test-suite config-test + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + main-is: ConfigTest.hs + build-depends: containers + , parameterized-utils + , prettyprinter + , tasty-checklist >= 1.0 && < 1.1 + , text + +test-suite online-solver-test + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + + main-is: OnlineSolverTest.hs + + if flag(solverTests) + buildable: True + if ! flag(STPTestDisable) + cpp-options: -DTEST_STP + else + buildable: False + + build-depends: + bv-sized, + bytestring, + containers, + data-binary-ieee754, + lens, + process, + text, + versions + +test-suite expr-builder-smtlib2 + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + + main-is: ExprBuilderSMTLib2.hs + + build-depends: + bv-sized, + bytestring, + containers, + data-binary-ieee754, + libBF, + text, + versions + + +test-suite exprs_tests + import: bldflags, testdefs-hedgehog, testdefs-hunit + type: exitcode-stdio-1.0 + + main-is: ExprsTest.hs + + other-modules: + GenWhat4Expr + + build-depends: bv-sized + + +test-suite iteexprs_tests + import: bldflags, testdefs-hedgehog, testdefs-hunit + type: exitcode-stdio-1.0 + + main-is: IteExprs.hs + + other-modules: + GenWhat4Expr + + build-depends: bv-sized + , containers >= 0.5.0.0 + + +test-suite bvdomain_tests + import: bldflags, testdefs-quickcheck + type: exitcode-stdio-1.0 + + hs-source-dirs: test/QC + main-is: BVDomTests.hs + + other-modules: VerifyBindings + + build-depends: transformers + + +test-suite bvdomain_tests_hh + import: bldflags, testdefs-hedgehog + type: exitcode-stdio-1.0 + + hs-source-dirs: test/HH + main-is: BVDomTests.hs + + other-modules: VerifyBindings + + build-depends: transformers + + +test-suite template_tests + import: bldflags, testdefs-hedgehog + type: exitcode-stdio-1.0 + main-is : TestTemplate.hs + build-depends: bv-sized + , libBF + , transformers + + +test-suite solver_parsing_tests + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + main-is : SolverParserTest.hs + build-depends: contravariant + , exceptions + , io-streams + , lumberjack + , tasty-sugar >= 1.1 && < 1.2 + , text