Packages

c

edu.cmu.cs.ls.keymaerax.bellerophon

SequentialInterpreter

abstract class SequentialInterpreter extends Interpreter with Logging

Sequential interpreter for Bellerophon tactic expressions.

Linear Supertypes
Logging, Interpreter, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SequentialInterpreter
  2. Logging
  3. Interpreter
  4. AnyRef
  5. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new SequentialInterpreter(listeners: Seq[IOListener])

    listeners

    Pre- and pos-processing hooks for step-wise tactic execution.

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. def apply(expr: BelleExpr, v: BelleValue): BelleValue

    Returns the result of applying tactic expr to the proof value v (usually a provable).

    Returns the result of applying tactic expr to the proof value v (usually a provable).

    Definition Classes
    SequentialInterpreterInterpreter
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def bval(s: Sequent): BelleProvable

    Maps sequents to BelleProvables.

    Maps sequents to BelleProvables.

    Attributes
    protected
  7. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  10. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  11. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. var isDead: Boolean
    Definition Classes
    SequentialInterpreterInterpreter
  14. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. def kill(): Unit

    Stops the interpreter and kills all its tactic executions.

    Stops the interpreter and kills all its tactic executions.

    Definition Classes
    SequentialInterpreterInterpreter
  16. val listeners: Seq[IOListener]
    Definition Classes
    SequentialInterpreterInterpreter
  17. val logger: Logger
    Attributes
    protected
    Definition Classes
    Logging
  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 replaceConclusion(original: ProvableSig, n: Int, subderivation: ProvableSig): (ProvableSig, Int)

    Replaces the nth subgoal of original with the remaining subgoals of result.

    Replaces the nth subgoal of original with the remaining subgoals of result.

    original

    A Provable whose nth subgoal is equal to "result".

    n

    The numerical index of the subgoal of original to rewrite (Seqs are zero-indexed)

    returns

    A pair of: * A new provable that is identical to original, except that the nth subgoal is replaced with the remaining subgoals of result; and * The new index of the (n+1)th goal. //@todo clarify

    Attributes
    protected
    To do

    result is undefined. Subderivation rather

  22. def runExpr(expr: BelleExpr, v: BelleValue): BelleValue

    Returns the result of running tactic expr on value v.

    Returns the result of running tactic expr on value v.

    Attributes
    protected
  23. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  24. def toString(): String
    Definition Classes
    AnyRef → Any
  25. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  26. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  27. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Logging

Inherited from Interpreter

Inherited from AnyRef

Inherited from Any

Ungrouped