Module type LogtkIndex.SUBSUMPTION_IDX

module type SUBSUMPTION_IDX = sig .. end

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