Module Make.StmQSource

Sourcemodule Stm = Stm
Sourcemodule WeightFun : sig ... end
Sourcetype t

A priority queue.

Sourceval add : t -> Stm.t -> unit

Add a stream to the Queue

Sourceval add_lst : t -> Stm.t list -> unit

Add a list of streams to the queue

Sourceval length : t -> int

Number of elements

Sourceval is_empty : t -> bool

check whether the queue is empty

Sourceval take_first : t -> Stm.C.t option

Attempts to take a clause out of the queue. Guarded recursion: can't loop forever

Sourceval take_first_anyway : t -> Stm.C.t option

Takes a clause out of the queue. Unguarded recursion, may loop forever

Sourceval 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

Sourceval 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

Sourceval name : t -> string

Name of the implementation/role of the queue

Available Queues
Sourceval 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 to take_first_when_available and take_first_anyway.

  • parameter name

    the name of this stream queue

Sourceval default : unit -> t

Obtain the default queue

IO
Sourceval to_string : t -> string