Module Make.StmQ
module Stm = Stm
module WeightFun : sig ... end
val length : t -> int
Number of elements
val is_empty : t -> bool
check whether the queue is empty
val take_first : t -> Stm.C.t option
Attempts to take a clause out of the queue. Guarded recursion: can't loop forever @raises Not_found in the guard is reached
val take_fair_anyway : t -> Stm.C.t option list
Takes clauses from the queue in a fair manner. Unguarded recursion, may loop forever
val take_stm_nb : t -> Stm.C.t option list
Attempts to take as many clauses from the queue as there are streams in the queue. Calls take_first to do so and stops if its guard is reached
val take_stm_nb_fix_stm : t -> Stm.C.t option list
Attempts to take as many clauses from the queue as there are streams in the queue. Extract as many clauses as possible from first stream before moving to a new stream to find more clauses if necessary
val name : t -> string
Name of the implementation/role of the queue
Available Queues
val make : guard:int -> ratio:int -> weight:(Stm.t -> int) -> string -> t
Creates a priority queue that uses
weight
to sort streams.- parameter ratio
pick-given ratio. Only one in
ratio
truly returns a clause if there is one available in calls totake_first_when_available
andtake_fair_anyway
.
- parameter name
the name of this stream queue
val default : unit -> t
Obtain the default queue