what4
Version 1.6.2 revision 0 uploaded by ryanglscott.
Package meta
- 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.
- Author
- Galois Inc.
- Bug reports
- https://github.com/GaloisInc/what4/issues
- Category
- Formal Methods, Theorem Provers, Symbolic Computation, SMT
- Copyright
- (c) Galois, Inc 2014-2023
- Homepage
- https://github.com/GaloisInc/what4
- Maintainer
- rscott@galois.com, kquick@galois.com
- Package URL
- n/a
- Stability
- n/a