kbcv.model

Stacks

class Stacks extends AnyRef

This class manages the current state of kbcv on two seperate stacks to provide undo/redo functionality.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. Hide All
  2. Show all
  1. Stacks
  2. AnyRef
  3. Any
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Stacks (model: Model)

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 clone (): AnyRef

    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws()
  8. def curr : State

    Reference to the current state of kbcv.

  9. def currIndex : Int

    The currentIndex in the undo/redo stack.

  10. def del (a: String, f: Int, i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Changes the procedure state, unsets the given flag, and updates the list of selected indices.

    Changes the procedure state, unsets the given flag, and updates the list of selected indices.

    a

    the new procedure state

    f

    the flag to unset

    i

    the updated list of selected indices for equations and rules

    msg

    the message to output

  11. def del (s: (), a: String, f: Int, i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Overrides the erc, changes the procedure state, unsets the given flag, and updates the list of selected indices.

    Overrides the erc, changes the procedure state, unsets the given flag, and updates the list of selected indices.

    s

    the new erc consisting of one equational system and two term rewrite systems

    a

    the new procedure state

    f

    the flag to unset

    i

    the updated list of selected indices for equations and rules

    msg

    the message to output

  12. def del (s: (), a: String, f: Int, p: Precedence, i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Overrides the system, changes the procedure state, unsets the given flag, overrides the current precedence, and updates the list of selected indices.

    Overrides the system, changes the procedure state, unsets the given flag, overrides the current precedence, and updates the list of selected indices.

    s

    the new erc consisting of one equational system and two term rewrite systems

    a

    the new procedure state

    f

    the flag to unset

    p

    the new precedence

    i

    the updated list of selected indices for equations and rules

    msg

    the message to output

  13. def del (a: String, f: Int, msg: (String, List[String], String)): Unit

    Changes the procedure state and unsets the given flag.

    Changes the procedure state and unsets the given flag.

    a

    the new procedure state

    f

    the flag to unset

    msg

    the message to output

  14. def del (f: Int, msg: (String, List[String], String)): Unit

    Unsets the given flag.

    Unsets the given flag.

    f

    the flag to unset

    msg

    the message to output

  15. def e0 : IES

  16. def efficient : Boolean

    Indicates whether the efficient complesion is used (true) or the simple one (false).

  17. def eq (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef
  18. def equals (arg0: Any): Boolean

    Definition Classes
    AnyRef → Any
  19. def erc : ()

    A reference to the current erc consisting of one equational system and two term rewrite systems.

  20. def expert : Boolean

    Indicates whether kbcv is in expert (true) or in normal mode (false).

  21. def finalize (): Unit

    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws()
  22. def flags : Int

    The currently set flags.

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

    Attributes
    final
    Definition Classes
    AnyRef → Any
  24. def hashCode (): Int

    Definition Classes
    AnyRef → Any
  25. def indices : (List[Int], List[Int])

    A reference to the lists of selected indices for equations and rules.

  26. def isInstanceOf [T0] : Boolean

    Attributes
    final
    Definition Classes
    Any
  27. def lpo : Boolean

    Indicates whether kbcv is using the built-in lexicographic path order (true) or an external termination tool (false).

  28. def lr : Boolean

    Indicates whether the "from left to right"-flag is set (true) or not (false).

  29. def msg : String

    The current message string.

  30. def msgs : List[(String, List[String], String)]

    The list of all messages in the undo/redo stack.

  31. def ne (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef
  32. def next (p: Precedence, msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  33. def next (s: (), p: Precedence, msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  34. def next (s: (), msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  35. def next (e: IES, s: (), a: String, p: Precedence, i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  36. def next (s: (), a: String, p: Precedence, i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  37. def next (s: (), a: String, i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  38. def next (s: (), a: String, msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  39. def next (s: (), p: Precedence, i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  40. def next (e: IES, s: (), i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  41. def next (s: (), i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  42. def next (pt: ProofTree, msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  43. def next (e: IES, s: (), a: String, v: List[String], t: List[(String, String)], f: Int, p: Precedence, i: (List[Int], List[Int]), n: Short, r: List[(Int, List[Int], Int, Int, List[Int])], pt: ProofTree, msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

    Creates a new state on the undo stack and clears the redo stack.

    e

    the new e

    s

    the new erc

    a

    the new procedure state

    v

    the new list of used variables

    t

    the currently used termination tool

    f

    the currently set flags

    p

    the new precedence

    i

    the new lists of selected equation and rule indices

    n

    the new number of runs to use for automatic completion

    r

    the list of new strategies

    pt

    the current proof tree

    msg

    the message to output

  44. def notify (): Unit

    Attributes
    final
    Definition Classes
    AnyRef
  45. def notifyAll (): Unit

    Attributes
    final
    Definition Classes
    AnyRef
  46. def numRuns : Short

    The number of concurrent kbcv.model.KBCV.Runs which is used in automatic completion.

  47. def precedence : Precedence

    A reference to the currently used precedence for lpo.

  48. def prev : State

    Reference to the previous state of kbcv.

  49. def prevCmd : String

    The previously executed command.

  50. def prevCmdArgs : List[String]

    The arguments of the previously executed command.

  51. def procState : String

    The current state of the completion procedure.

  52. def proofTree : ProofTree

    The current proof tree.

  53. def redo (): Stack[State]

    Redo the last udone command.

  54. val redoStack : Stack[State]

    The stack of all undone commands to this point.

  55. def redoable (i: Int): Boolean

    Indicates if i steps are redoable or not.

    Indicates if i steps are redoable or not.

    i

    number of steps to redo

  56. def reset : Unit

    Clear the redo stack.

  57. def rl : Boolean

    Indicates whether the "from right to left"-flag is set (true) or not (false).

  58. def set (s: (), a: String, f: Int, i: (List[Int], List[Int]), msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  59. def set (a: String, f: Int, msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  60. def set (f: Int, msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  61. def set (n: Short, msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  62. def set (r: List[(Int, List[Int], Int, Int, List[Int])], msg: (String, List[String], String)): Unit

    Creates a new state on the undo stack and clears the redo stack.

  63. val startState : State

    The default start state for kbcv.

    The default start state for kbcv. The values are as follows:

          initial es: is empty
          erc: all systems are empty,
          procedure state: simplify equation,
          variables: empty,
          termination tool: ./ttt2 -cpf xml - 5,
          lpo: true,
          precedence: empty,
          selected indices: none,
          number of runs for automatic completion: 1,
          strategies: run1: top down, step size 1, left to right,
                      run2: top down, step size 1, right to left,
                      run3: bottom up, step size 1, left to right,
                      run4: bottom up, step size 1, right to left,
                      run5: random, step size 1, left to right,
                      run6: random, step size 1, right to left,
          proof tree: a single App rule with an equation referencing -1
    
  64. def strategies : List[(Int, List[Int], Int, Int, List[Int])]

    The strategies for the kbcv.model.KBCV.Runs used by automatic completion.

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

    Attributes
    final
    Definition Classes
    AnyRef
  66. def termTool : String

    The currently used termination tool.

  67. def termTools : List[(String, String)]

    A list of available termination tools and their arguments.

  68. def toString (): String

    Definition Classes
    AnyRef → Any
  69. def undo (): Stack[State]

    Undo the last executed command.

  70. val undoStack : Stack[State]

    The stack of all executed commands to this point.

  71. def undoable (i: Int): Boolean

    Indicates if i steps are undoable or not.

    Indicates if i steps are undoable or not.

    i

    number of steps to undo

  72. def vars : List[String]

    A list of variables currently used in the system.

  73. def wait (): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()
  74. def wait (arg0: Long, arg1: Int): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()
  75. def wait (arg0: Long): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()

Inherited from AnyRef

Inherited from Any