class TaskManager extends AnyRef

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

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TaskManager
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def +(t: PrioritisedTask): TaskManager
  4. def ++(elems: Iterable[PrioritisedTask]): TaskManager
  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  8. def dequeueWhile(pred: (Task) => Boolean): (TaskManager, Seq[Task])

    Dequeue as long as the given predicate is satisfied

  9. def enqueue(elems: PrioritisedTask*): TaskManager
  10. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  11. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  12. def filter(p: (PrioritisedTask) => Boolean): TaskManager

    Eliminate all prioritised tasks for which the given predicate is false.

  13. def finalEagerTask: Boolean
  14. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  15. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  16. def isEmpty: Boolean
  17. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  18. def max: Task

    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.

    returns

    the element with the smallest priority.

  19. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  20. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  21. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  22. def prioritisedTasks: Iterable[PrioritisedTask]
  23. def removeFirst: TaskManager

    Remove the first task from the queue.

  24. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  25. val taskAggregator: VectorTaskAggregator
  26. def taskConstants: Set[ConstantTerm]
  27. def taskSummary: TaskSummary

    Computed information about the prioritised tasks (eager tasks are not considered at this point)

  28. def taskSummaryFor(agg: TaskAggregator): TaskSummary
  29. def toString(): String
    Definition Classes
    TaskManager → AnyRef → Any
  30. def updateTasks(goal: Goal, stopUpdating: (Task) => Boolean): TaskManager

    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.

  31. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  32. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  33. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

    (Since version 9)

Inherited from AnyRef

Inherited from Any

Ungrouped