Name: what4 Version: 1.1 Author: Galois Inc. Maintainer: jhendrix@galois.com, rdockins@galois.com Copyright: (c) Galois, Inc 2014-2021 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.4, GHC==8.10.3 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-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, 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 && < 5.0, zenc >= 0.1.0 && < 0.2.0, ghc-prim >= 0.5.2 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.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.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 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, mtl >= 2.2.1, 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, libBF, 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 , containers >= 0.5.0.0 , 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 test-suite template_tests type: exitcode-stdio-1.0 default-language: Haskell2010 hs-source-dirs: test main-is : TestTemplate.hs build-depends: base , bv-sized , libBF , 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