Packages

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. Protected

Type Members

  1. type AsPartiallyOrdered[B] = (B) => PartiallyOrdered[B]
    Definition Classes
    PartiallyOrdered

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. def --(consts: Iterable[ConstantTerm]): ConstantFreedom

    Give the given constants bottom status.

  4. def <[B >: ConstantFreedom](that: B)(implicit arg0: AsPartiallyOrdered[B]): Boolean
    Definition Classes
    PartiallyOrdered
  5. def <=[B >: ConstantFreedom](that: B)(implicit arg0: (B) => PartiallyOrdered[B]): Boolean
    Definition Classes
    ConstantFreedom → PartiallyOrdered
  6. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  7. def >[B >: ConstantFreedom](that: B)(implicit arg0: AsPartiallyOrdered[B]): Boolean
    Definition Classes
    PartiallyOrdered
  8. def >=[B >: ConstantFreedom](that: B)(implicit arg0: AsPartiallyOrdered[B]): Boolean
    Definition Classes
    PartiallyOrdered
  9. def addTopStatus(consts: Iterable[ConstantTerm]): ConstantFreedom

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

  10. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  11. def changedConstants(that: ConstantFreedom): Set[ConstantTerm]

    List all constants whose status is different in this and that

  12. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  13. def diffIsShieldingLC(lc1: LinearCombination, lc2: LinearCombination, bc: BindingContext): Boolean

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

  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(that: Any): Boolean
    Definition Classes
    ConstantFreedom → AnyRef → Any
  16. def findNonFreeness(unshieldedConj: Conjunction, bc: BindingContext): ConstantFreedom

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

  17. def freeConstsAreUniversal(bc: BindingContext): Boolean

    Only used for runtime assertion purposes

  18. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  19. def hashCode(): Int
    Definition Classes
    ConstantFreedom → AnyRef → Any
  20. def isBottom: Boolean
  21. def isBottomWRT(constants: Set[ConstantTerm]): Boolean
  22. def isBottomWRT(constant: ConstantTerm): Boolean
  23. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  24. def isShielded(c: Conjunction, bc: BindingContext): Boolean

    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 .

  25. def meet(that: ConstantFreedom): ConstantFreedom
  26. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  27. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  28. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  29. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  30. def toString(): String
    Definition Classes
    ConstantFreedom → AnyRef → Any
  31. def tryCompareTo[B >: ConstantFreedom](that: B)(implicit arg0: (B) => PartiallyOrdered[B]): Option[Int]
    Definition Classes
    ConstantFreedom → PartiallyOrdered
  32. def unshieldedPart(c: Conjunction, bc: BindingContext): Conjunction

    Determine the (disjunctively connected) unshielded part of a formula

  33. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  34. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  35. 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 PartiallyOrdered[ConstantFreedom]

Inherited from AnyRef

Inherited from Any

Ungrouped