module NPDtree: sig
.. end
Non-Perfect Discrimination Tree
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 Dtree
, and maybe more optimized too.
module Make (
E
:
Index.EQUATION
)
: Index.UNIT_IDX
with module E = E
module MakeTerm (
X
:
Set.OrderedType
)
: Index.TERM_IDX
with type elt = X.t