| Copyright | (c) Galois Inc 2014-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.WordMap
Description
Synopsis
- data WordMap sym w tp = SimpleWordMap !(SymExpr sym (BaseArrayType (EmptyCtx ::> BaseBVType w) BaseBoolType)) !(SymExpr sym (BaseArrayType (EmptyCtx ::> BaseBVType w) tp))
- emptyWordMap :: (IsExprBuilder sym, 1 <= w) => sym -> NatRepr w -> BaseTypeRepr a -> IO (WordMap sym w a)
- muxWordMap :: IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> Pred sym -> WordMap sym w a -> WordMap sym w a -> IO (WordMap sym w a)
- insertWordMap :: IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> SymBV sym w -> SymExpr sym a -> WordMap sym w a -> IO (WordMap sym w a)
- lookupWordMap :: IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> SymBV sym w -> WordMap sym w a -> IO (PartExpr (Pred sym) (SymExpr sym a))
Documentation
data WordMap sym w tp Source #
A WordMap represents a finite partial map from bitvectors of width w
to elements of type tp.
Constructors
| SimpleWordMap !(SymExpr sym (BaseArrayType (EmptyCtx ::> BaseBVType w) BaseBoolType)) !(SymExpr sym (BaseArrayType (EmptyCtx ::> BaseBVType w) tp)) |
emptyWordMap :: (IsExprBuilder sym, 1 <= w) => sym -> NatRepr w -> BaseTypeRepr a -> IO (WordMap sym w a) Source #
Create a word map where every element is undefined.
muxWordMap :: IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> Pred sym -> WordMap sym w a -> WordMap sym w a -> IO (WordMap sym w a) Source #
Compute a pointwise if-then-else operation on the elements of two word maps.
Arguments
| :: IsExprBuilder sym | |
| => sym | |
| -> NatRepr w | |
| -> BaseTypeRepr a | |
| -> SymBV sym w | index |
| -> SymExpr sym a | new value |
| -> WordMap sym w a | word map to update |
| -> IO (WordMap sym w a) |
Update a word map at the given index.
Arguments
| :: IsExprBuilder sym | |
| => sym | |
| -> NatRepr w | |
| -> BaseTypeRepr a | |
| -> SymBV sym w | index |
| -> WordMap sym w a | |
| -> IO (PartExpr (Pred sym) (SymExpr sym a)) |
Lookup the value of an index in a word map.