@hackage what41.7

Solver-agnostic symbolic values support for issuing queries

Categories
License
BSD-3-Clause
Maintainer
rscott@galois.com, kquick@galois.com
Links
Versions
- 1.7 Fri, 21 Mar 2025
- 1.6.3 Wed, 26 Feb 2025
- 1.6.2 Mon, 23 Sep 2024
- 1.6.1 Tue, 3 Sep 2024
- 1.6 Wed, 15 May 2024
- 1.5.1 Fri, 13 Oct 2023

Installation
In your cabal file:
Tested Compilers
Dependencies (47)
- base >=4.10 && <5
- bytestring >=0.10
- containers >=0.5.0.0
- deepseq >=1.3
- directory >=1.2.2
- filepath >=1.3
Dependents (10)
@hackage/crucible-syntax, @hackage/cryptol, @hackage/copilot-verifier, @hackage/crucible-llvm, @hackage/copilot-theorem, @hackage/crucible, Show all…

Package Flags

solvertests

(off by default)

extra tests that require all the solvers to be installed

drealtestdisable

(off by default)

when running solver tests, disable testing using dReal (ignored unless -fsolverTests)

stptestdisable

(off by default)

when running solver tests, disable testing using STP (ignored unless -fsolverTests)

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.

@hackage what41.7

Categories

License

Maintainer

Links

Versions

Installation

Tested Compilers

Dependencies (47)

Dependents (10)

Package Flags