What4.WordMap

Description

Synopsis

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

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.

Arguments

:: forall sym (w :: Nat) (a :: BaseType). 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.