Module ARG.Stm

module Ctx : Ctx.S
module C : Clause.S with module Ctx = Ctx
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