doc: add comment about representation

This commit is contained in:
Leonardo de Moura 2019-11-24 08:17:44 -08:00
parent 5842366416
commit e81f38c116

View file

@ -13,6 +13,9 @@ namespace DiscrTree
/-
(Imperfect) discrimination trees.
We use a hybrid representation.
- A `PersistentHashMap` for the root node which usually contains many children.
- A sorted array of key/node pairs for inner nodes.
The edges are labeled by keys:
- Constant names (and arity). Universe levels are ignored.