Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

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 :: (Num i, Bits i, SymWord 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.