| Copyright | (c) Galois Inc 2021 |
|---|---|
| License | BSD3 |
| Maintainer | Ryan Scott <rscott@galois.com> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
What4.Utils.ResolveBounds.BV
Description
A utility for using an OnlineSolver to query if a SymBV is concrete
or symbolic, and if it is symbolic, what the lower and upper bounds are.
Synopsis
- resolveSymBV :: forall w sym solver scope st fs. (1 <= w, sym ~ ExprBuilder scope st fs, OnlineSolver solver) => sym -> SearchStrategy -> NatRepr w -> SolverProcess scope solver -> SymBV sym w -> IO (ResolvedSymBV w)
- data SearchStrategy
- data ResolvedSymBV w
- = BVConcrete (BV w)
- | BVSymbolic (Domain w)
Documentation
Arguments
| :: forall w sym solver scope st fs. (1 <= w, sym ~ ExprBuilder scope st fs, OnlineSolver solver) | |
| => sym | |
| -> SearchStrategy | The strategy to use when searching for lower and upper bounds. For
many use cases, |
| -> NatRepr w | The bitvector width |
| -> SolverProcess scope solver | The online solver process to use to search for lower and upper bounds. |
| -> SymBV sym w | The bitvector to resolve. |
| -> IO (ResolvedSymBV w) |
Use an OnlineSolver to attempt to resolve a SymBV as concrete.
If it cannot, return the lower and upper bounds. This is primarly intended
for compound expressions whose bounds cannot trivially be determined by
using signedBVBounds or unsignedBVBounds.
data SearchStrategy Source #
The strategy to use to search for lower and upper bounds in
resolveSymBV.
Constructors
| ExponentialSearch | After making an initial guess for a bound, increase (for upper bounds) or decrease (for lower bounds) the initial guess by an exponentially increasing amount (1, 2, 4, 8, ...) until the bound has been exceeded. At that point, back off from exponential search and use binary search until the bound has been determined. For many use cases, this is a reasonable default. |
| BinarySearch | Use binary search to found each bound, using |
Instances
| Pretty SearchStrategy Source # | |
Defined in What4.Utils.ResolveBounds.BV | |
data ResolvedSymBV w Source #
The results of an OnlineSolver trying to resolve a SymBV as
concrete.
Constructors
| BVConcrete (BV w) | A concrete bitvector, including its value as a |
| BVSymbolic (Domain w) | A symbolic |
Instances
| Show (ResolvedSymBV w) Source # | |
Defined in What4.Utils.ResolveBounds.BV Methods showsPrec :: Int -> ResolvedSymBV w -> ShowS # show :: ResolvedSymBV w -> String # showList :: [ResolvedSymBV w] -> ShowS # | |