Safe Haskell | None |
---|---|
Language | Haskell2010 |
Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental
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, SymVal 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, SymVal 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.