Hoogle Search
Within LTS Haskell 24.52 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
PartialT :: (sym -> Pred sym -> m (PartExpr (Pred sym) a)) -> PartialT sym (m :: Type -> Type) awhat4 What4.Partial No documentation available.
-
what4 What4.Partial Either a partial value, or a straight-up error.
-
ProblemFeatures uses bit mask to represent the features. The bits are: 0 : Uses linear arithmetic 1 : Uses non-linear arithmetic, i.e. multiplication (should also set bit 0) 2 : Uses computational reals (should also set bits 0 & 1) 3 : Uses integer variables (should also set bit 0) 4 : Uses bitvectors 5 : Uses exists-forall. 6 : Uses quantifiers (should also set bit 5) 7 : Uses symbolic arrays or complex numbers. 8 : Uses structs 9 : Uses strings 10 : Uses floating-point 11 : Computes UNSAT cores 12 : Computes UNSAT assumptions 13 : Uses uninterpreted functions 14 : Uses defined functions
-
what4 What4.ProblemFeatures Allowed features represents features that the constraint solver will need to support to solve the problem.
-
This module primarily defines the Position datatype for handling program location data. A program location may refer either to a source file location (file name, line and column number), a binary file location (file name and byte offset) or be a dummy "internal" location assigned to generated program fragments.
-
what4 What4.ProgramLoc A value with a source position associated.
Posd :: Position -> v -> Posd vwhat4 What4.ProgramLoc No documentation available.
-
what4 What4.ProgramLoc No documentation available.
-
what4 What4.ProgramLoc A very small type that contains a function and PC identifier.
module What4.Protocol.
PolyRoot Defines a numeric data-type where each number is represented as the root of a polynomial over a single variable. This currently only defines operations for parsing the roots from the format generated by Yices, and evaluating a polynomial over rational coefficients to the rational derived from the closest double.