A priority queue.

Add a stream to the Queue

Add a list of streams to the queue

Number of elements

check whether the queue is empty

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

• raises Not_found

  in the guard is reached

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

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

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

Name of the implementation/role of the queue

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

Obtain the default queue