module type SUBSUMPTION_IDX = sig .. end
type
module C: Index_intf.CLAUSE
val name : string
val empty : unit -> t
Empty index
val add : t -> C.t -> t
Index the clause
val add_seq : t ->
C.t Sequence.t -> t
val add_list : t -> C.t list -> t
val remove : t -> C.t -> t
Un-index the clause
val remove_seq : t ->
C.t Sequence.t -> t
val retrieve_subsuming : t -> Index_intf.lits -> C.t Sequence.t
Fold on a set of indexed candidate clauses, that may subsume
the given clause.
val retrieve_subsuming_c : t -> C.t -> C.t Sequence.t
val retrieve_subsumed : t -> Index_intf.lits -> C.t Sequence.t
Fold on a set of indexed candidate clauses, that may be subsumed by
the given clause
val retrieve_subsumed_c : t -> C.t -> C.t Sequence.t
val iter : t -> C.t Sequence.t
val fold : ('a -> C.t -> 'a) -> 'a -> t -> 'a