Dequeue as long as the given predicate is satisfied
Eliminate all prioritised tasks for which the given predicate is false.
Returns the element with the smallest priority value in the queue, or throws an error if there is no element contained in the queue.
Returns the element with the smallest priority value in the queue, or throws an error if there is no element contained in the queue.
the element with the smallest priority.
Remove the first task from the queue.
Computed information about the prioritised tasks (eager tasks are not considered at this point)
Update all PrioritisedTask
stored by this managed, making
use of possibly new facts and information from the goal.
Update all PrioritisedTask
stored by this managed, making
use of possibly new facts and information from the goal. The argument
stopUpdating
can be used to tell at which point the updating
of tasks can be stopped, because some task or fact has been discovered that
can be used right away.
(Since version ) see corresponding Javadoc for more information.
An immutable class (priority queue) for handling a set of tasks in a proof goal. This is implemented using a leftist heap.
TODO: So far, no subsumption checks are performed