Module Make.Stm
module Ctx : Libzipperposition.Ctx.S
module C = Env.C
type t
= private
{
id : int;
unique ID of the stream
parents : C.t list;
parent clauses for inference generating this stream
mutable penalty : int;
heuristic penalty
mutable hits : int;
how many attemts to retrieve unifier were there
mutable stm : C.t option OSeq.t;
the stream itself
}
exception
Empty_Stream
exception
Drip_n_Unfinished of C.t option list * int * int
Basics
val make : ?penalty:int -> parents:C.t list -> C.t option OSeq.t -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val id : t -> int
val is_empty : t -> bool
val penalty : t -> int
val drip : t -> C.t option
Remove the first element in the stream and return it.
- raises Empty_Stream
if the stream is empty
val drip_n : t -> int -> int -> C.t option list
Attempt to remove the n first elements in the stream and return them. Return less if the guard is reached.
- raises Drip_n_Unfinished(cl,n)
where cl is the list of elements already found and n the number of elements if the stream contains less than n elements
IO
val pp : t CCFormat.printer