Data.SBV.Tools.STree

Implementation of full-binary symbolic trees, providing logarithmic time access to elements. Both reads and writes are supported.

Documentation

type STree i e = STreeInternal (SBV i) (SBV e)

A symbolic tree containing values of type e, indexed by elements of type i. Note that these are full-trees, and their their shapes remain constant. There is no API provided that can change the shape of the tree. These structures are useful when dealing with data-structures that are indexed with symbolic values where access time is important. STree structures provide logarithmic time reads and writes.

readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e

Reading a value. We bit-blast the index and descend down the full tree according to bit-values.

writeSTree :: (Mergeable (SBV e), Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e

Writing a value, similar to how reads are done. The important thing is that the tree representation keeps updates to a minimum.

mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e

Construct the fully balanced initial tree using the given values.