term.util

Equation

case class Equation (l: Term, r: Term) extends Product with Serializable

Represents an equation between two terms.

Equations are undirected so s ≈ t is identified with t ≈ s.

l

the left-hand side of the equation

r

the right-hand side of the equation

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. Hide All
  2. Show all
  1. Equation
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. Any
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Equation (l: Term, r: Term)

    Creates a new equation from two terms.

    Creates a new equation from two terms.

    l

    the left-hand side of the equation

    r

    the right-hand side of the equation

Value Members

  1. def != (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef

  2. def != (arg0: Any): Boolean

    Attributes
    final
    Definition Classes
    Any

  3. def ## (): Int

    Attributes
    final
    Definition Classes
    AnyRef → Any

  4. def == (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef

  5. def == (arg0: Any): Boolean

    Attributes
    final
    Definition Classes
    Any

  6. def asInstanceOf [T0] : T0

    Attributes
    final
    Definition Classes
    Any

  7. def canEqual (other: Any): Boolean

    Definition Classes
    Equation → Equals

  8. def clone (): AnyRef

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

  9. def eq (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef

  10. def equals (other: Any): Boolean

    Definition Classes
    Equation → Equals → AnyRef → Any

  11. def finalize (): Unit

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

  12. def getClass (): java.lang.Class[_]

    Attributes
    final
    Definition Classes
    AnyRef

  13. def hashCode (): Int

    Definition Classes
    Equation → AnyRef → Any

  14. def isInstanceOf [T0] : Boolean

    Attributes
    final
    Definition Classes
    Any

  15. def isJoinable (rs: TRS): Boolean

    Returns true if the left- and right-hand sides of this equation may be rewritten to the same normal form with respect to rs.

  16. def isTrivial : Boolean

    Returns true if this equation is a trivial equation, i.

    Returns true if this equation is a trivial equation, i.e., the left- and right-hand sides of this equations are the same, and false otherwise.

  17. def lhs : Term

    Returns the left-hand side term of this equation.

  18. def ne (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef

  19. def notify (): Unit

    Attributes
    final
    Definition Classes
    AnyRef

  20. def notifyAll (): Unit

    Attributes
    final
    Definition Classes
    AnyRef

  21. def productArity : Int

    Definition Classes
    Equation → Product

  22. def productElement (arg0: Int): Any

    Definition Classes
    Equation → Product

  23. def productIterator : Iterator[Any]

    Definition Classes
    Product

  24. def productPrefix : String

    Definition Classes
    Equation → Product

  25. def rhs : Term

    Returns the right-hand side term of this equation.

  26. def simpl (rs: TRS): E

    Returns this equation with the left- and right-hand sides reduced by one step with respect to the term rewrite system rs.

  27. def simplLHS (rs: TRS): E

    Returns this equation with the left-hand side reduced by one step with respect to the term rewrite system rs.

  28. def simplLHSToNF (rs: TRS): E

    Returns this equation with the left-hand side reduced to normal form with respect to the term rewrite system rs.

  29. def simplRHS (rs: TRS): E

    Returns this equation with the right-hand side reduced by one step with respect to the term rewrite system rs.

  30. def simplRHSToNF (rs: TRS): E

    Returns this equation with the right-hand side reduced to normal form with respect to the term rewrite system rs.

  31. def simplToNF (rs: TRS): E

    Returns this equation with the left- and right-hand sides reduced to normal form with respect to the term rewrite system rs.

  32. def swap : Equation

    Returns this equation with swapped left- and right-hand sides.

  33. def synchronized [T0] (arg0: ⇒ T0): T0

    Attributes
    final
    Definition Classes
    AnyRef

  34. def toRule : Rule

    Returns a rule from the left-hand side of this equation to the right-hand side of this equation.

  35. def toString (): String

    Definition Classes
    Equation → AnyRef → Any

  36. def toTuple : (Term, Term)

    Returns a tuple containing the left- and right-hand side terms of this equation.

  37. def vars : List[V]

    Returns a list of all variables occuring in this equation.

  38. def wait (): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()

  39. def wait (arg0: Long, arg1: Int): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()

  40. def wait (arg0: Long): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()

  41. def xReduceLHS (rs: TRS): E

    Returns this equation with the left-hand side reduced by one step with respect to rs without any rules equal to this equation.

  42. def xRewriteLHS (rs: TRS): E

    Returns this equation with the left-hand side reduced to normal form with respect to rs without any rules equal to this equation.

  43. def productElements : Iterator[Any]

    Definition Classes
    Product
    Annotations
    @deprecated
    Deprecated

    use productIterator instead