Class/Object

ap.proof.goal

TaskManager

Related Docs: object TaskManager | package goal

Permalink

class TaskManager extends AnyRef

An immutable class (priority queue) for handling a set of tasks in a proof goal. Currently, this is implemented using a sorted set, but it would be better to use a real immutable queue (leftist heap?).

TODO: So far, no real 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. All

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. def +(t: PrioritisedTask): TaskManager

    Permalink
  4. def ++(elems: Iterator[PrioritisedTask]): TaskManager

    Permalink
  5. def ++(elems: Iterable[PrioritisedTask]): TaskManager

    Permalink
  6. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  7. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  8. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  9. def dequeueWhile(pred: (Task) ⇒ Boolean): (TaskManager, Seq[Task])

    Permalink

    Dequeue as long as the given predicate is satisfied

  10. def enqueue(elems: PrioritisedTask*): TaskManager

    Permalink
  11. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  12. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  13. def filter(p: (PrioritisedTask) ⇒ Boolean): TaskManager

    Permalink

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

  14. def finalEagerTask: Boolean

    Permalink
  15. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  16. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  17. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  18. def isEmpty: Boolean

    Permalink
  19. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  20. def max: Task

    Permalink

    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.

  21. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  22. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  23. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  24. def prioritisedTasks: Iterable[PrioritisedTask]

    Permalink
  25. def removeFirst: TaskManager

    Permalink

    Remove the first task from the queue.

  26. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  27. def taskInfos: TaskInfoCollector

    Permalink

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

  28. def toString(): String

    Permalink
    Definition Classes
    TaskManager → AnyRef → Any
  29. def updateTasks(goal: Goal, stopUpdating: (Task) ⇒ Boolean): TaskManager

    Permalink

    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.

  30. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  31. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  32. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped