Related Docs: object RegularityBlockedTask | package goal

Formulae of the shape `t1 = 0 & ... & tn = 0 & !(s1 = 0 & ... & sm = 0)` that are blocked because the equations `t1 = 0 & ... & tn = 0 & s1 = 0 & ... & sm = 0` would reduce the facts of a goal to a mere subset

Linear Supertypes
Ordering
1. Alphabetic
2. By inheritance
Inherited
6. AnyRef
7. Any
1. Hide All
2. Show all
Visibility
1. Public
2. All

Value Members

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

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

Definition Classes
AnyRef → Any
3. final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
4. val age: Int

Definition Classes
5. def apply(goal: Goal, ptf: ProofTreeFactory): ProofTree

Definition Classes
6. final def asInstanceOf[T0]: T0

Definition Classes
Any
7. def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )

Attributes
protected[ap.proof.goal]
Definition Classes
9. final def eq(arg0: AnyRef): Boolean

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

Definition Classes
AnyRef → Any
11. def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
12. val formula: Conjunction

Definition Classes
13. final def getClass(): Class[_]

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

Definition Classes
AnyRef → Any
15. def isCoveredFormula(f: Conjunction): Boolean

Return `true` if `f` is a formula that can be handled by this task

Return `true` if `f` is a formula that can be handled by this task

Attributes
protected[ap.proof.goal]
Definition Classes
16. final def isInstanceOf[T0]: Boolean

Definition Classes
Any
17. val name: String

Definition Classes
18. final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
19. final def notify(): Unit

Definition Classes
AnyRef
20. final def notifyAll(): Unit

Definition Classes
AnyRef
21. val priority: Int

Definition Classes
22. def releaseFormula(f: Conjunction, goal: Goal): Boolean

Decide whether the given formula should still be blocked, or be released at this point.

Decide whether the given formula should still be blocked, or be released at this point.

Attributes
protected
Definition Classes
23. final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
24. def toString(): String

Definition Classes
25. def updateFormula(f: Conjunction, goal: Goal): FormulaTask

Create a new `FormulaTask` by updating the value of `formula`

Create a new `FormulaTask` by updating the value of `formula`

Attributes
protected[ap.proof.goal]
Definition Classes

Update the task with possibly new information from the goal

Update the task with possibly new information from the goal

Definition Classes
27. final def wait(): Unit

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )