Packages

c

edu.cmu.cs.ls.keymaerax.infrastruct

FastUSubstAboveURen

final class FastUSubstAboveURen extends RenUSubst

Fast implementation of: Renaming Uniform Substitution that, in goal-directed backwards Sequent direction, first runs a uniform renaming below and on the result subsequently the uniform substitution above it.

s(RG) |- s(RD)
-------------- USubst
  RG  |- RD
-------------- URen
   G  |- D

The direct application mechanism via apply() fast-forwards to the fast joint USubstRen infrastructure. Its tactical / prover core implementation works in sync using prover core operations by scheduling separate uniform substitutions and uniform renamings to the core when asked.

Note

reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.

See also

USubstRen

DirectUSubstAboveURen

Linear Supertypes
RenUSubst, (Expression) ⇒ Expression, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. FastUSubstAboveURen
  2. RenUSubst
  3. Function1
  4. AnyRef
  5. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new FastUSubstAboveURen(subsDefsInput: Seq[(Expression, Expression)])

Type Members

  1. type RenUSubstRepl = (Expression, Expression)

    A renaming substitution pair for a renaming uniform substitution.

    A renaming substitution pair for a renaming uniform substitution.

    Definition Classes
    RenUSubst
    See also

    edu.cmu.cs.ls.keymaerax.core.SubstitutionPair

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()

    edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def ++(other: RenUSubst): RenUSubst

    Union of renaming uniform substitutions, i.e., both replacement lists merged.

    Union of renaming uniform substitutions, i.e., both replacement lists merged.

    Definition Classes
    RenUSubst
  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. def andThen[A](g: (Expression) ⇒ A): (Expression) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  6. def apply(p: DifferentialProgram): DifferentialProgram
    Definition Classes
    FastUSubstAboveURen → RenUSubst
  7. def apply(p: Program): Program
    Definition Classes
    FastUSubstAboveURen → RenUSubst
  8. def apply(f: Formula): Formula
    Definition Classes
    FastUSubstAboveURen → RenUSubst
  9. def apply(t: Term): Term
    Definition Classes
    FastUSubstAboveURen → RenUSubst
  10. def apply(s: Sequent): Sequent

    Apply everywhere in the sequent.

    Apply everywhere in the sequent.

    Definition Classes
    RenUSubst
  11. def apply(e: Expression): Expression
    Definition Classes
    RenUSubst → Function1
  12. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  13. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  14. def compose[A](g: (A) ⇒ Expression): (A) ⇒ Expression
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  15. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. def equals(e: Any): Boolean
    Definition Classes
    FastUSubstAboveURen → AnyRef → Any
  17. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  18. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  19. lazy val getRenamingTactic: BelleExpr

    Get the renaming tactic part that performs this renaming

    Get the renaming tactic part that performs this renaming

    Definition Classes
    FastUSubstAboveURen → RenUSubst
  20. def hashCode(): Int
    Definition Classes
    FastUSubstAboveURen → AnyRef → Any
  21. def isEmpty: Boolean

    Returns true if there is no replacement.

    Returns true if there is no replacement.

    Definition Classes
    RenUSubst
  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  24. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  25. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  26. def reapply(subs: Seq[(Expression, Expression)]): FastUSubstAboveURen

    Create a similar RenUSubst of the same class with the alternative list of replacements

    Create a similar RenUSubst of the same class with the alternative list of replacements

    Definition Classes
    FastUSubstAboveURen → RenUSubst
  27. lazy val renaming: RenUSubst

    The uniform renaming part of this renaming uniform substitution

    The uniform renaming part of this renaming uniform substitution

    Definition Classes
    FastUSubstAboveURen → RenUSubst
  28. lazy val substitution: RenUSubst

    The uniform substitution part of this renaming uniform substitution as a RenUSubst

    The uniform substitution part of this renaming uniform substitution as a RenUSubst

    Definition Classes
    FastUSubstAboveURen → RenUSubst
    See also

    usubst

  29. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  30. lazy val toCore: (Expression) ⇒ Expression

    This RenUSubst implemented strictly from the core.

    This RenUSubst implemented strictly from the core.

    Definition Classes
    FastUSubstAboveURen → RenUSubst
    Note

    For contract purposes

  31. lazy val toForward: (ProvableSig) ⇒ ProvableSig

    Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.

    Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.

    Definition Classes
    FastUSubstAboveURen → RenUSubst
  32. def toString(): String
    Definition Classes
    FastUSubstAboveURen → Function1 → AnyRef → Any
  33. lazy val usubst: USubst

    The uniform substitution part of this renaming uniform substitution as a USubst

    The uniform substitution part of this renaming uniform substitution as a USubst

    Definition Classes
    FastUSubstAboveURen → RenUSubst
    See also

    substitution

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

Inherited from RenUSubst

Inherited from (Expression) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped