Min-priority queue for tableau formulas, backed by :gb_trees.
Elements are bucketed by integer cost; within the same cost bucket they are
served FIFO. The cost is supplied by the caller (see Rules.rule_cost/1).
Summary
Functions
Returns true if the queue contains no elements.
Inserts element at the given cost. Equal-cost elements are served FIFO.
Returns an empty priority queue.
Removes and returns the lowest-cost element together with the updated queue.
Types
@type t() :: :gb_trees.tree(non_neg_integer(), :queue.queue(ShotTx.Prover.Rules.rule_t()))
Functions
Returns true if the queue contains no elements.
@spec insert(t(), element :: term(), cost :: non_neg_integer()) :: t()
Inserts element at the given cost. Equal-cost elements are served FIFO.
@spec new() :: t()
Returns an empty priority queue.
Removes and returns the lowest-cost element together with the updated queue.