Reference to the current state of kbcv.
The currentIndex in the undo/redo stack.
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.
the new procedure state
the flag to unset
the updated list of selected indices for equations and rules
the message to output
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.
the new erc consisting of one equational system and two term rewrite systems
the new procedure state
the flag to unset
the updated list of selected indices for equations and rules
the message to output
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.
the new erc consisting of one equational system and two term rewrite systems
the new procedure state
the flag to unset
the new precedence
the updated list of selected indices for equations and rules
the message to output
Changes the procedure state and unsets the given flag.
Changes the procedure state and unsets the given flag.
the new procedure state
the flag to unset
the message to output
Unsets the given flag.
Unsets the given flag.
the flag to unset
the message to output
Indicates whether the efficient complesion is used (true) or the simple one (false).
A reference to the current erc consisting of one equational system and two term rewrite systems.
Indicates whether kbcv is in expert (true) or in normal mode (false).
The currently set flags.
A reference to the lists of selected indices for equations and rules.
Indicates whether kbcv is using the built-in lexicographic path order (true) or an external termination tool (false).
Indicates whether the "from left to right"-flag is set (true) or not (false).
The current message string.
The list of all messages in the undo/redo stack.
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.
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.
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.
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.
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.
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.
Creates a new state on the undo stack and clears the redo stack.
the new e
the new erc
the new procedure state
the new list of used variables
the currently used termination tool
the currently set flags
the new precedence
the new lists of selected equation and rule indices
the new number of runs to use for automatic completion
the list of new strategies
the current proof tree
the message to output
The number of concurrent kbcv.model.KBCV.Runs which is used in automatic completion.
A reference to the currently used precedence for lpo.
Reference to the previous state of kbcv.
The previously executed command.
The arguments of the previously executed command.
The current state of the completion procedure.
The current proof tree.
Redo the last udone command.
The stack of all undone commands to this point.
Indicates if i steps are redoable or not.
Indicates if i steps are redoable or not.
number of steps to redo
Clear the redo stack.
Indicates whether the "from right to left"-flag is set (true) or not (false).
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.
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.
Creates a new state on the undo stack and clears the redo stack.
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
The strategies for the kbcv.model.KBCV.Runs used by automatic completion.
The currently used termination tool.
A list of available termination tools and their arguments.
Undo the last executed command.
The stack of all executed commands to this point.
Indicates if i steps are undoable or not.
Indicates if i steps are undoable or not.
number of steps to undo
A list of variables currently used in the system.
This class manages the current state of kbcv on two seperate stacks to provide undo/redo functionality.