WordValue

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.

Force a word value into packed word form

Force a word value into a sequence of bits

Extract a subsequence of bits from a WordValue. The first integer argument is the number of bits in the resulting word. The second integer argument is the number of less-significant digits to discard. Stated another way, the operation `extractWordVal n i w` is equivalent to first shifting w right by i bits, and then truncating to n 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 TODO, can we get rid of this? If feels like it should be unnecessary.

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.

Force the evaluation of a word value