| 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 :: Nat) (tp :: BaseType) = SimpleWordMap !(SymExpr sym (BaseArrayType ((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) BaseBoolType)) !(SymExpr sym (BaseArrayType ((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) tp))
- emptyWordMap :: forall sym (w :: Natural) (a :: BaseType). (IsExprBuilder sym, 1 <= w) => sym -> NatRepr w -> BaseTypeRepr a -> IO (WordMap sym w a)
- muxWordMap :: forall sym (w :: Nat) (a :: BaseType). IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> Pred sym -> WordMap sym w a -> WordMap sym w a -> IO (WordMap sym w a)
- insertWordMap :: forall sym (w :: Nat) (a :: BaseType). IsExprBuilder sym => sym -> NatRepr w -> BaseTypeRepr a -> SymBV sym w -> SymExpr sym a -> WordMap sym w a -> IO (WordMap sym w a)
- lookupWordMap :: forall sym (w :: Nat) (a :: BaseType). 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 :: Nat) (tp :: BaseType) Source #
A WordMap represents a finite partial map from bitvectors of width w
to elements of type tp.
Constructors
| SimpleWordMap !(SymExpr sym (BaseArrayType ((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) BaseBoolType)) !(SymExpr sym (BaseArrayType ((EmptyCtx :: Ctx BaseType) ::> BaseBVType w) tp)) |
emptyWordMap :: forall sym (w :: Natural) (a :: BaseType). (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 :: forall sym (w :: Nat) (a :: BaseType). 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
| :: forall sym (w :: Nat) (a :: BaseType). 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.