what4: Solver-agnostic symbolic values support for issuing queries
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.
[Skip to Readme]
Modules
[Index] [Quick Jump]
- Test
- What4
- What4.BaseTypes
- What4.Concrete
- What4.Config
- What4.Expr
- What4.FunctionName
- What4.IndexLit
- What4.Interface
- What4.InterpretedFloatingPoint
- What4.LabeledPred
- What4.Panic
- What4.Partial
- What4.ProblemFeatures
- What4.ProgramLoc
- Protocol
- What4.SWord
- What4.SatResult
- What4.SemiRing
- What4.Solver
- What4.Symbol
- Utils
- What4.Utils.AbstractDomains
- What4.Utils.AnnotatedMap
- What4.Utils.Arithmetic
- What4.Utils.BVDomain
- 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
- What4.WordMap
Flags
Manual Flags
Name | Description | Default |
---|---|---|
solvertests | extra tests that require all the solvers to be installed | Disabled |
drealtestdisable | when running solver tests, disable testing using dReal (ignored unless -fsolverTests) | Disabled |
stptestdisable | when running solver tests, disable testing using STP (ignored unless -fsolverTests) | Disabled |
Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info
Downloads
- what4-1.0.tar.gz [browse] (Cabal source package)
- Package description (revised from the package)
Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
Versions [RSS] | 1.0, 1.1, 1.2, 1.2.1, 1.3, 1.4, 1.5, 1.5.1, 1.6, 1.6.1, 1.6.2 |
---|---|
Change log | CHANGES.md |
Dependencies | ansi-wl-pprint (>=0.6.8), attoparsec (>=0.13), base (>=4.8 && <5), bifunctors (>=5), bimap (>=0.2), bv-sized (>=1.0.0), bytestring (>=0.10), containers (>=0.5.0.0), data-binary-ieee754, deepseq (>=1.3), deriving-compat (>=0.5), directory (>=1.2.2), exceptions (>=0.10), extra (>=1.6), filepath (>=1.3), fingertree (>=0.1.4), ghc-prim (>=0.5.3), hashable (>=1.3 && <1.4), 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), template-haskell, temporary (>=1.2), 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), what4, zenc (>=0.1.0 && <0.2.0) [details] |
License | BSD-3-Clause |
Copyright | (c) Galois, Inc 2014-2020 |
Author | Galois Inc. |
Maintainer | jhendrix@galois.com, rdockins@galois.com |
Revised | Revision 2 made by ryanglscott at 2023-02-10T21:06:59Z |
Category | Formal Methods, Theorem Provers, Symbolic Computation, SMT |
Home page | https://github.com/GaloisInc/what4 |
Bug tracker | https://github.com/GaloisInc/what4/issues |
Source repo | head: git clone https://github.com/GaloisInc/what4 |
Uploaded | by RobertDockins at 2020-07-22T06:03:00Z |
Distributions | Arch:1.5.1, LTSHaskell:1.5.1, Stackage:1.6.2 |
Reverse Dependencies | 8 direct, 8 indirect [details] |
Executables | quickstart |
Downloads | 4306 total (93 in the last 30 days) |
Rating | 2.25 (votes: 2) [estimated by Bayesian average] |
Your Rating | |
Status | Docs uploaded by user Build status unknown [no reports yet] |