class EquivalenceRelation extends AnyRef
a container for relations like ==, !=, and <= on terms which are indexed by shape)
the class approximates the relations based on the available knowledge initially nothing is known, and instances are added over time
knowledge grows monotonously and cannot be removed inconsistency can arise (which can, e.g., be used to terminate a proof)
the class implements - reflexivity, symmetry, and (cached) transitivity of == - irreflexivity and symmetry of != - reflexivity, anti-symmetry wrt ==, and (not cached) transitivity of <= - congruence of <= wrt == - disjointness of == and != (used to detect inconsistency)
- Alphabetic
- By Inheritance
- EquivalenceRelation
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
belowOrEqual(s: Term, t: Term): Unit
records the knowledge s <= t
-
def
checkBelowOrEqual(s: Term, t: Term): Option[Boolean]
checks if s <= t is known to be true or false; possibly inconclusive
-
def
checkEquivalent(s: Term, t: Term): Option[Boolean]
checks if s == t or s != t is known; possibly inconclusive
-
def
checkStrictlyBelow(s: Term, t: Term): Option[Boolean]
checks if s < t is known to be true or false; possibly inconclusive
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
equivalent(s: Term, t: Term): Unit
records the knowledge s == t
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
def
getClass(s: Term): Option[EquivalenceClass]
the equivalence class of s (if any)
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getOrAddClass(t: Term): EquivalenceClass
the equivalence class of s (possibly a singleton)
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
inconsistent: Boolean
true if the available knowledge is inconsistent
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
notEquivalent(s: Term, t: Term): Unit
records the knowledge s != t
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
strictlyBelow(s: Term, t: Term): Unit
records the knowledge s < t
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()