sbv-10.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
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.

Synopsis

- type STree i e = STreeInternal (SBV i) (SBV e)
- readSTree :: (SFiniteBits i, SymVal e) => STree i e -> SBV i -> SBV e
- writeSTree :: (SFiniteBits i, SymVal e) => STree i e -> SBV i -> SBV e -> STree i e
- mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e

# 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.

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

Construct the fully balanced initial tree using the given values.