Documentation

Concrete bitvector values: width, value Invariant: The value must be within the range 0 .. 2^width-1

Apply an integer function to the values of bitvectors. This function assumes both bitvectors are the same width.

Apply an integer function to the values of a bitvector. This function assumes the function will not require masking.

Smart constructor for BVs that checks for the width limit

A sequence map represents a mapping from nonnegative integer indices to values. These are used to represent both finite and infinite sequences.

Generate a finite sequence map from a list of values

Generate an infinite sequence map from a stream of values

Create a finite list of length n of the values from [0..n-1] in the given the sequence emap.

Create an infinite stream of all the values in a sequence map

Reverse the order of a finite sequence map

Concatenate the first n values of the first sequence map onto the beginning of the second sequence map.

Given a number n and a sequence map, return two new sequence maps: the first containing the values from `[0..n-1]` and the next containing the values from n onward.

Drop the first n elements of the given SeqMap.

Given a sequence map, return a new sequence map that is memoized using a finite map memo table.

Apply the given evaluation function pointwise to the two given sequence maps.

Apply the given function to each value in the given sequence map

For efficiency reasons, we handle finite sequences of bits as special cases in the evaluator. In cases where we know it is safe to do so, we prefer to used a "packed word" representation of bit sequences. This allows us to rely directly on Integer types (in the concrete evaluator) and SBV's Word types (in the symbolic simulator).

However, if we cannot be sure all the bits of the sequence will eventually be forced, we must instead rely on an explicit sequence of bits representation.

An arbitrarily-chosen number of elements where we switch from a dense sequence representation of bit-level words to SeqMap representation.

Force a word value into packed word form

Force a word value into a sequence of bits

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in big-endian order.

Turn a word value into a sequence of bits, forcing each bit. The sequence is returned in reverse of the usual order, which is little-endian order.

Compute the size of a word value

Select an individual bit from a word value

Produce a new WordValue from the one given by updating the ith bit with the given bit value.

Generic value type, parameterized by bit and word types.

NOTE: we maintain an important invariant regarding sequence types. VSeq must never be used for finite sequences of bits. Always use the VWord constructor instead! Infinite sequences of bits are handled by the VStream constructor, just as for other types.

Force the evaluation of a word value

Force the evaluation of a value

This type class defines a collection of operations on bits and words that are necessary to define generic evaluator primitives that operate on both concrete and symbolic values uniformly.

This class defines additional operations necessary to define generic evaluation functions.

Create a packed word of n bits.

Functions that assume word inputs

A type lambda that expects a Type.

A type lambda that expects a Type of kind #.

Generate a stream.

This is strict!

Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.

Construct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.

Extract a bit value.

Extract an integer value.

Extract a finite sequence value.

Extract a sequence.

Extract a packed word.

If the given list of values are all fully-evaluated thunks containing bits, return a packed word built from the same bits. However, if any value is not a fully-evaluated bit, return Nothing.

Turn a value into an integer represented by w bits.

Extract a function from a value.

Extract a polymorphic function from a value.

Extract a polymorphic function from a value.

Extract a tuple from a value.

Extract a record from a value.

Lookup a field in a record.

Given an expected type, returns an expression that evaluates to this value, if we can determine it.

XXX: View patterns would probably clean up this definition a lot.