| Copyright | (c) Levent Erkok |
|---|---|
| License | BSD3 |
| Maintainer | erkokl@gmail.com |
| Stability | experimental |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.SBV.Tools.STree
Description
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) Source #
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 :: (SFiniteBits i, SymWord e) => STree i e -> SBV i -> SBV e Source #
Reading a value. We bit-blast the index and descend down the full tree according to bit-values.
writeSTree :: (SFiniteBits i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e Source #
Writing a value, similar to how reads are done. The important thing is that the tree representation keeps updates to a minimum.