Logtk.Index_intftype term = Term.ttype subst = Subst.tmodule type LEAF = sig ... endmodule type TERM_IDX = sig ... endtype lits = term SLiteral.t Iter.tIter of literals, as a cheap abstraction on query clauses
type labels = Util.Int_set.tmodule type CLAUSE = sig ... endmodule type SUBSUMPTION_IDX = sig ... endmodule type EQUATION = sig ... endmodule type UNIT_IDX = sig ... end