Module Logtk.NPDtree (.ml)

module NPDtree: LogtkNPDtree


This module provides a simplification index and a term index, based on a non-perfect discrimination tree (see "the handbook of automated reasoning", chapter "term indexing", for instance). It should be more compact in memory than LogtkDtree, and maybe more optimized too.
module Make (E : LogtkIndex.EQUATION) : LogtkIndex.UNIT_IDX  with module E = E
module MakeTerm (X : Set.OrderedType) : LogtkIndex.TERM_IDX  with type elt = X.t