Cabal revisions of what4-1.7
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.7-Author: Galois Inc.-Maintainer: rscott@galois.com, kquick@galois.com-Copyright: (c) Galois, Inc 2014-2023-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.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.2, GHC==9.4.4, GHC==9.6.2, GHC==9.8.1, GHC==9.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, CVC5, Yices, Bitwuzla, 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- hs-source-dirs: test/hedgehog- build-depends: hedgehog >= 1.0.2- , tasty-hedgehog >= 1.2- other-modules: Test.Tasty.Hedgehog.Alt--common testdefs-hunit- import: testdefs- build-depends: tasty-hunit >= 0.9--library- import: bldflags- build-depends:- base >= 4.10 && < 5,- async,- attoparsec >= 0.13,- bimap >= 0.2,- bifunctors >= 5,- BoundedChan >= 1 && < 2,- bv-sized >= 1.0.0,- bytestring >= 0.10,- deriving-compat >= 0.5,- concurrent-extra >= 0.7 && < 0.8,- config-value >= 0.8 && < 0.9,- containers >= 0.5.0.0,- deepseq >= 1.3,- directory >= 1.2.2,- exceptions >= 0.10,- 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,- megaparsec >= 8 && < 10,- mtl >= 2.2.1,- ordered-containers >= 0.2 && < 0.3,- panic >= 0.3,- parameterized-utils >= 2.1 && < 2.2,- parsec >= 3 && < 4,- prettyprinter >= 1.7.0,- process >= 1.2,- s-cargot >= 0.1 && < 0.2,- scientific >= 0.3.6,- stm,- temporary >= 1.2,- template-haskell,- text >= 1.2.4.0 && < 2.2,- th-lift >= 0.8.2 && < 0.9,- th-lift-instances >= 0.1 && < 0.2,- time >= 1.8 && < 1.13,- transformers >= 0.4,- unliftio >= 0.2 && < 0.3,- unordered-containers >= 0.2.10,- utf8-string >= 1.0.1,- vector >= 0.12.1,- versions >= 6.0.2 && < 6.1,- 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.FloatMode- What4.LabeledPred- What4.Panic- What4.Partial- What4.ProblemFeatures- What4.ProgramLoc- What4.SatResult- What4.SemiRing- What4.SpecialFunctions- What4.Symbol- What4.SFloat- What4.SWord- What4.WordMap-- What4.Expr- What4.Expr.Allocator- 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.Serialize.FastSExpr- What4.Serialize.Log- What4.Serialize.Normalize- What4.Serialize.Parser- What4.Serialize.Printer- What4.Serialize.SETokens-- What4.Solver- What4.Solver.Adapter- What4.Solver.Bitwuzla- What4.Solver.Boolector- What4.Solver.CVC4- What4.Solver.CVC5- 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.ResolveBounds.BV- What4.Utils.Serialize- 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 abduct- import: testdefs-hunit- type: exitcode-stdio-1.0- main-is: Abduct.hs- default-language: Haskell2010-- build-depends:- base,- parameterized-utils,- what4,- text,- temporary--test-suite adapter-test- import: bldflags, testdefs-hunit- type: exitcode-stdio-1.0-- main-is: AdapterTest.hs-- other-modules: ProbeSolvers-- 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,- lens,- mtl >= 2.2.1,- process,- tasty-expected-failure >= 0.12 && < 0.13,- 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-- other-modules: ProbeSolvers-- if flag(solverTests)- buildable: True- if ! flag(STPTestDisable)- cpp-options: -DTEST_STP- else- buildable: False-- build-depends:- async,- bv-sized,- bytestring,- clock,- containers,- exceptions,- lens,- prettyprinter,- process,- tasty-expected-failure >= 0.12 && < 0.13,- tasty-checklist >= 1.0 && < 1.1,- text,- units,- units-defs,- versions--test-suite expr-builder-smtlib2- import: bldflags, testdefs-hedgehog, testdefs-hunit- type: exitcode-stdio-1.0-- main-is: ExprBuilderSMTLib2.hs-- other-modules: ProbeSolvers-- build-depends:- bv-sized,- bytestring,- containers,- libBF,- prettyprinter,- process,- tasty-expected-failure >= 0.12 && < 0.13,- tasty-checklist >= 1.0.3 && < 1.1,- text,- versions---test-suite exprs_tests- import: bldflags, testdefs-hedgehog, testdefs-hunit- type: exitcode-stdio-1.0-- main-is: ExprsTest.hs-- other-modules:- Bool- GenWhat4Expr-- build-depends: bv-sized- , containers- , mtl--executable bool-normalization- import: bldflags, testdefs-hedgehog, testdefs-hunit- main-is: BoolNormalization.hs- other-modules: Bool- build-depends: containers- , mtl- , transformers---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 >= 2.0 && < 2.3- , text--test-suite what4-serialize-tests- default-language: Haskell2010- type: exitcode-stdio-1.0- ghc-options: -Wall -Wcompat -rtsopts -threaded- hs-source-dirs: test- main-is: SerializeTests.hs- other-modules: SymFnTests, SerializeTestUtils- build-depends: what4- , base- , containers- , directory- , exceptions- , hedgehog- , libBF- , tasty- , tasty-hunit- , tasty-hedgehog- , text- , parameterized-utils- , async- , directory- , ordered-containers--test-suite invariant-synthesis- import: bldflags, testdefs-hunit- type: exitcode-stdio-1.0-- main-is: InvariantSynthesis.hs-- other-modules: ProbeSolvers-- build-depends:- bv-sized,- process,- tasty-expected-failure >= 0.12 && < 0.13-+Cabal-version: 2.4 +Name: what4 +Version: 1.7 +x-revision: 1 +Author: Galois Inc. +Maintainer: rscott@galois.com, kquick@galois.com +Copyright: (c) Galois, Inc 2014-2023 +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.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.2, GHC==9.4.4, GHC==9.6.2, GHC==9.8.1, GHC==9.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, CVC5, Yices, Bitwuzla, 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 + hs-source-dirs: test/hedgehog + build-depends: hedgehog >= 1.0.2 + , tasty-hedgehog >= 1.2 + other-modules: Test.Tasty.Hedgehog.Alt + +common testdefs-hunit + import: testdefs + build-depends: tasty-hunit >= 0.9 + +library + import: bldflags + build-depends: + base >= 4.10 && < 5, + async, + attoparsec >= 0.13, + bimap >= 0.2, + bifunctors >= 5, + BoundedChan >= 1 && < 2, + bv-sized >= 1.0.0, + bytestring >= 0.10, + deriving-compat >= 0.5, + concurrent-extra >= 0.7 && < 0.8, + config-value >= 0.8 && < 0.9, + containers >= 0.5.0.0, + deepseq >= 1.3, + directory >= 1.2.2, + exceptions >= 0.10, + 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, + megaparsec >= 8 && < 10, + mtl >= 2.2.1, + ordered-containers >= 0.2 && < 0.3, + panic >= 0.3, + parameterized-utils >= 2.1 && < 2.2, + parsec >= 3 && < 4, + prettyprinter >= 1.7.0, + process >= 1.2, + s-cargot >= 0.1 && < 0.2, + scientific >= 0.3.6, + stm, + temporary >= 1.2, + template-haskell, + text >= 1.2.4.0 && < 2.2, + th-lift >= 0.8.2 && < 0.9, + th-lift-instances >= 0.1 && < 0.2, + time >= 1.8 && < 1.15, + transformers >= 0.4, + unliftio >= 0.2 && < 0.3, + unordered-containers >= 0.2.10, + utf8-string >= 1.0.1, + vector >= 0.12.1, + versions >= 6.0.2 && < 6.1, + 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.FloatMode + What4.LabeledPred + What4.Panic + What4.Partial + What4.ProblemFeatures + What4.ProgramLoc + What4.SatResult + What4.SemiRing + What4.SpecialFunctions + What4.Symbol + What4.SFloat + What4.SWord + What4.WordMap + + What4.Expr + What4.Expr.Allocator + 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.Serialize.FastSExpr + What4.Serialize.Log + What4.Serialize.Normalize + What4.Serialize.Parser + What4.Serialize.Printer + What4.Serialize.SETokens + + What4.Solver + What4.Solver.Adapter + What4.Solver.Bitwuzla + What4.Solver.Boolector + What4.Solver.CVC4 + What4.Solver.CVC5 + 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.ResolveBounds.BV + What4.Utils.Serialize + 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 abduct + import: testdefs-hunit + type: exitcode-stdio-1.0 + main-is: Abduct.hs + default-language: Haskell2010 + + build-depends: + base, + parameterized-utils, + what4, + text, + temporary + +test-suite adapter-test + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + + main-is: AdapterTest.hs + + other-modules: ProbeSolvers + + 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, + lens, + mtl >= 2.2.1, + process, + tasty-expected-failure >= 0.12 && < 0.13, + 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 + + other-modules: ProbeSolvers + + if flag(solverTests) + buildable: True + if ! flag(STPTestDisable) + cpp-options: -DTEST_STP + else + buildable: False + + build-depends: + async, + bv-sized, + bytestring, + clock, + containers, + exceptions, + lens, + prettyprinter, + process, + tasty-expected-failure >= 0.12 && < 0.13, + tasty-checklist >= 1.0 && < 1.1, + text, + units, + units-defs, + versions + +test-suite expr-builder-smtlib2 + import: bldflags, testdefs-hedgehog, testdefs-hunit + type: exitcode-stdio-1.0 + + main-is: ExprBuilderSMTLib2.hs + + other-modules: ProbeSolvers + + build-depends: + bv-sized, + bytestring, + containers, + libBF, + prettyprinter, + process, + tasty-expected-failure >= 0.12 && < 0.13, + tasty-checklist >= 1.0.3 && < 1.1, + text, + versions + + +test-suite exprs_tests + import: bldflags, testdefs-hedgehog, testdefs-hunit + type: exitcode-stdio-1.0 + + main-is: ExprsTest.hs + + other-modules: + Bool + GenWhat4Expr + + build-depends: bv-sized + , containers + , mtl + +executable bool-normalization + import: bldflags, testdefs-hedgehog, testdefs-hunit + main-is: BoolNormalization.hs + other-modules: Bool + build-depends: containers + , mtl + , transformers + + +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 >= 2.0 && < 2.3 + , text + +test-suite what4-serialize-tests + default-language: Haskell2010 + type: exitcode-stdio-1.0 + ghc-options: -Wall -Wcompat -rtsopts -threaded + hs-source-dirs: test + main-is: SerializeTests.hs + other-modules: SymFnTests, SerializeTestUtils + build-depends: what4 + , base + , containers + , directory + , exceptions + , hedgehog + , libBF + , tasty + , tasty-hunit + , tasty-hedgehog + , text + , parameterized-utils + , async + , directory + , ordered-containers + +test-suite invariant-synthesis + import: bldflags, testdefs-hunit + type: exitcode-stdio-1.0 + + main-is: InvariantSynthesis.hs + + other-modules: ProbeSolvers + + build-depends: + bv-sized, + process, + tasty-expected-failure >= 0.12 && < 0.13 +