Class/Object

ap.proof

ConstantFreedom

Related Docs: object ConstantFreedom | package proof

Permalink

class ConstantFreedom extends PartiallyOrdered[ConstantFreedom]

Class to represent the set of constants that are considered as "free" (i.e., that are only unifiable with themselves). Objects of this class are stored in the nodes of proof tree and are updated when the proof is expanded in order to eventually reach a fixed point.

TODO: avoid the creation of new objects whenever possible

Linear Supertypes
PartiallyOrdered[ConstantFreedom], AnyRef, Any
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. ConstantFreedom
  2. PartiallyOrdered
  3. AnyRef
  4. 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 --(consts: Iterable[ConstantTerm]): ConstantFreedom

    Permalink

    Give the given constants bottom status.

  4. def <[B >: ConstantFreedom](that: B)(implicit arg0: (B) ⇒ PartiallyOrdered[B]): Boolean

    Permalink
    Definition Classes
    PartiallyOrdered
  5. def <=[B >: ConstantFreedom](that: B)(implicit arg0: (B) ⇒ PartiallyOrdered[B]): Boolean

    Permalink
    Definition Classes
    ConstantFreedom → PartiallyOrdered
  6. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  7. def >[B >: ConstantFreedom](that: B)(implicit arg0: (B) ⇒ PartiallyOrdered[B]): Boolean

    Permalink
    Definition Classes
    PartiallyOrdered
  8. def >=[B >: ConstantFreedom](that: B)(implicit arg0: (B) ⇒ PartiallyOrdered[B]): Boolean

    Permalink
    Definition Classes
    PartiallyOrdered
  9. def addTopStatus(consts: Iterable[ConstantTerm]): ConstantFreedom

    Permalink

    Set the status of the given constants to the top value (as free as possible)

  10. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  11. def changedConstants(that: ConstantFreedom): Set[ConstantTerm]

    Permalink

    List all constants whose status is different in this and that

    List all constants whose status is different in this and that

  12. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  13. def diffIsShieldingLC(lc1: LinearCombination, lc2: LinearCombination, bc: BindingContext): Boolean

    Permalink

    Determine whether the formula lc1 - lc2 = 0 & phi is shielded (for arbitrary phi)

    Determine whether the formula lc1 - lc2 = 0 & phi is shielded (for arbitrary phi)

  14. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  15. def equals(that: Any): Boolean

    Permalink
    Definition Classes
    ConstantFreedom → AnyRef → Any
  16. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  17. def findNonFreeness(unshieldedConj: Conjunction, bc: BindingContext): ConstantFreedom

    Permalink

    Given a constraint from which all shielded parts have been removed, determine which constants have to be considered as non-free

  18. def freeConstsAreUniversal(bc: BindingContext): Boolean

    Permalink

    Only used for runtime assertion purposes

  19. final def getClass(): Class[_]

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

    Permalink
    Definition Classes
    ConstantFreedom → AnyRef → Any
  21. def isBottom: Boolean

    Permalink
  22. def isBottomWRT(constants: Set[ConstantTerm]): Boolean

    Permalink
  23. def isBottomWRT(constant: ConstantTerm): Boolean

    Permalink
  24. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  25. def isShielded(c: Conjunction, bc: BindingContext): Boolean

    Permalink

    Determine whether c is a formula of the shape a*x + t = 0 & phi , where a != 0 and x is a quasi-universal constant that is maximal in a*x + t = 0 .

    Determine whether c is a formula of the shape a*x + t = 0 & phi , where a != 0 and x is a quasi-universal constant that is maximal in a*x + t = 0 .

  26. def meet(that: ConstantFreedom): ConstantFreedom

    Permalink
  27. final def ne(arg0: AnyRef): Boolean

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

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

    Permalink
    Definition Classes
    AnyRef
  30. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  31. def toString(): String

    Permalink
    Definition Classes
    ConstantFreedom → AnyRef → Any
  32. def tryCompareTo[B >: ConstantFreedom](that: B)(implicit arg0: (B) ⇒ PartiallyOrdered[B]): Option[Int]

    Permalink
    Definition Classes
    ConstantFreedom → PartiallyOrdered
  33. def unshieldedPart(c: Conjunction, bc: BindingContext): Conjunction

    Permalink

    Determine the (disjunctively connected) unshielded part of a formula

  34. final def wait(): Unit

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

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

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

Inherited from PartiallyOrdered[ConstantFreedom]

Inherited from AnyRef

Inherited from Any

Ungrouped