Packages

implicit class ExpressionAugmentor[E <: Expression] extends AnyRef

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. ExpressionAugmentor
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new ExpressionAugmentor(e: E)

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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. val e: E
  7. def elaborateToFunctions(signature: Set[NamedSymbol]): Expression

    Elaborates in e variable uses of functions listed in signature.

    Elaborates in e variable uses of functions listed in signature. Replaces all literal occurrences of BaseVariable of the same name as a function in signature, but ignores all non-BaseVariable occurrences and ignores all non-function symbols in signature. Also elaborates FuncOf to PredOf per sort in signature.

  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  10. def exhaustiveSubst(subst: USubst): Expression

    Applies substitutions per substs exhaustively.

  11. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  12. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. def implicitSubst(other: Expression): SubstitutionPair
  15. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  16. def listSubPos: List[(Kind, PosInExpr)]

    Lists all subpositions of expression e, categorized by their kind.

  17. def matchingTerms(matcher: (Term) ⇒ Boolean): List[Term]

    Returns all sub-terms of this expression that pass matcher.

  18. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. def replaceAll(repls: Map[Expression, Expression]): E

    Replace all occurrences of what in e by repl.

    Replace all occurrences of what in e by repl. what and repl must be of the same kind, either Term, Formula, or Program. Replaces literal occurrences even in places disallowed by uniform substitution (minimal safeguarding to not replace in some obvious invalid places).

    Exceptions thrown

    ClassCastException When repl cannot be cast to the type expected at an occurrence of what (e.g., when replacing x with f() inside x:=y).

  22. def replaceAll(what: Expression, repl: Expression): E

    Replace all occurrences of what in e by repl.

    Replace all occurrences of what in e by repl. what and repl must be of the same kind, either Term, Formula, or Program. Replaces literal occurrences even in places disallowed by uniform substitution (minimal safeguarding to not replace in some obvious invalid places).

    Exceptions thrown

    ClassCastException When repl cannot be cast to the type expected at an occurrence of what (e.g., when replacing x with f() inside x:=y).

  23. def replaceAt(pos: PosInExpr, repl: Expression): Expression
  24. def replaceFree(what: Term, repl: Term): E
  25. def sub(pos: PosInExpr): Option[Expression]
  26. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  27. def toString(): String
    Definition Classes
    AnyRef → Any
  28. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  31. def ~>>(other: Expression): SubstitutionPair

    The substitution pair term~>other after dottifying other to fit arguments of term.

Inherited from AnyRef

Inherited from Any

Ungrouped