Module Make.SubsumptionIndexSource

Sourcetype t
Sourcemodule C : Logtk.Index_intf.CLAUSE with type t = C.t
Sourceval name : string
Sourceval empty : unit -> t

Empty index

Sourceval add : t -> C.t -> t

Index the clause

Sourceval add_seq : t -> C.t Iter.t -> t
Sourceval add_list : t -> C.t list -> t
Sourceval remove : t -> C.t -> t

Un-index the clause

Sourceval remove_seq : t -> C.t Iter.t -> t

Fold on a set of indexed candidate clauses, that may subsume the given clause.

Sourceval retrieve_subsuming_c : t -> C.t -> C.t Iter.t

Fold on a set of indexed candidate clauses, that may be subsumed by the given clause

Sourceval retrieve_subsumed_c : t -> C.t -> C.t Iter.t
Sourceval retrieve_alpha_equiv : t -> Logtk.Index_intf.lits -> Logtk.Index_intf.labels -> C.t Iter.t

Retrieve clauses that are potentially alpha-equivalent to the given clause

Sourceval retrieve_alpha_equiv_c : t -> C.t -> C.t Iter.t

Retrieve clauses that are potentially alpha-equivalent to the given clause

Sourceval iter : t -> C.t Iter.t
Sourceval fold : ('a -> C.t -> 'a) -> 'a -> t -> 'a