Module Index_intf (.ml)

module Index_intf: sig .. end

Match the indexed terms against the given query term

type term = FOTerm.t

type subst = Substs.t

module type LEAF = sig .. end

module type TERM_IDX = sig .. end

type lits = term SLiteral.t Sequence.t

Sequence of literals, as a cheap abstraction on query clauses

module type CLAUSE = sig .. end

module type SUBSUMPTION_IDX = sig .. end

module type EQUATION = sig .. end

module type UNIT_IDX = sig .. end