Module LogtkIndex

module LogtkIndex: sig .. end

Generic term indexing

type scope = LogtkSubsts.scope 
type term = LogtkFOTerm.t 
type subst = LogtkSubsts.t 


A leaf maps terms to a set of elements
module type LEAF = sig .. end
module MakeLeaf (X : Set.OrderedType) : LEAF  with type elt = X.t

LogtkFOTerm index

module type TERM_IDX = sig .. end

Subsumption LogtkIndex

type lits = (bool * term Sequence.t) Sequence.t 
Sequence of literals, as a cheap abstraction on query clauses
module type CLAUSE = sig .. end

A subsumption index (non perfect!)
module type SUBSUMPTION_IDX = sig .. end

Specialized rewriting index

module type EQUATION = sig .. end
module BasicEquation: EQUATION 
  with type t = LogtkFOTerm.t * LogtkFOTerm.t
  and type rhs = LogtkFOTerm.t
module type UNIT_IDX = sig .. end