Module LogtkDtree.Default

module Default: LogtkIndex.UNIT_IDX  with module E = LogtkIndex.BasicEquation

type t 
module E: LogtkIndex.EQUATION 
Module that describes indexed equations
type rhs = E.rhs 
Right hand side of equation
val empty : unit -> t
val is_empty : t -> bool
val add : t -> E.t -> t
LogtkIndex the given (in)equation
val add_seq : t -> E.t Sequence.t -> t
val remove : t -> E.t -> t
val remove_seq : t -> E.t Sequence.t -> t
val size : t -> int
Number of indexed (in)equations
val iter : t -> (LogtkIndex.term -> E.t -> unit) -> unit
Iterate on indexed equations
val retrieve : ?allow_open:bool ->
?subst:LogtkIndex.subst ->
sign:bool ->
t ->
LogtkIndex.scope ->
LogtkIndex.term ->
LogtkIndex.scope ->
'a ->
('a ->
LogtkIndex.term -> rhs -> E.t -> LogtkIndex.subst -> 'a) ->
'a
retrieve ~sign (idx,si) (t,st) acc folds on (in)equations l ?= r of given sign and substitutions subst, such that subst(l, si) = t. It therefore finds generalizations of the query term.
val to_dot : Buffer.t -> t -> unit
print the index in the DOT format