| java.lang.Object
 de.uka.ilkd.key.gui.InteractiveProver
| InteractiveProver | | public class InteractiveProver (Code) | | |
| Method Summary | |
| public void | addAutoModeListener(AutoModeListener p)
| | public void | applyInteractive(RuleApp app, Goal goal)
Apply a RuleApp and continue with update simplification or strategy
application according to current settings. | | protected void | fireAutoModeStarted(ProofEvent e)
| | public void | fireAutoModeStopped(ProofEvent e)
| | protected SetOfTacletApp | getAppsForName(Goal goal, String name, PosInOccurrence pos)
| | protected SetOfTacletApp | getAppsForName(Goal goal, String name, PosInOccurrence pos, TacletFilter filter)
| | public ListOfBuiltInRule | getBuiltInRule(PosInOccurrence pos, Constraint userConstraint)
collects all built-in rules that are applicable at the given sequent
position 'pos'. | | public SetOfRuleApp | getBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pos, Constraint userConstraint)
| | protected SetOfRuleApp | getBuiltInRuleAppsForName(String name, PosInOccurrence pos)
| | ListOfTacletApp | getFindTaclet(PosInSequent pos)
| | ListOfTacletApp | getNoFindTaclet()
| | public Proof | getProof()
| | ListOfTacletApp | getRewriteTaclet(PosInSequent pos)
| | public boolean | interactiveMode()
| | KeYMediator | mediator()
| | public void | removeAutoModeListener(AutoModeListener p)
| | public boolean | resumeAutoMode()
| | public void | setInteractive(boolean interact)
| | public void | setProof(Proof p)
| | void | setResumeAutoMode(boolean b)
| | public void | startAutoMode()
| | public void | startAutoMode(ListOfGoal goals)
starts the execution of rules with active strategy. | | public void | startFocussedAutoMode(PosInOccurrence focus, Goal goal)
starts the execution of rules with active strategy. | | public void | stopAutoMode()
|
| InteractiveProver | | public InteractiveProver(KeYMediator mediator)(Code) | | creates a new interactive prover object
|
| applyInteractive | | public void applyInteractive(RuleApp app, Goal goal)(Code) | | Apply a RuleApp and continue with update simplification or strategy
application according to current settings.
Parameters:
app -
Parameters:
goal - |
| fireAutoModeStarted | | protected void fireAutoModeStarted(ProofEvent e)(Code) | | fires the event that automatic execution has started
|
| fireAutoModeStopped | | public void fireAutoModeStopped(ProofEvent e)(Code) | | fires the event that automatic execution has stopped
|
| getAppsForName | | protected SetOfTacletApp getAppsForName(Goal goal, String name, PosInOccurrence pos)(Code) | | collects all Taclet applications at the given position of the specified
taclet
Parameters:
goal - the Goal for which the applications should be returned
Parameters:
name - the String with the taclet names whose applications are looked for
Parameters:
pos - the PosInOccurrence describing the position a list of all found rule applications of the given rule atposition pos |
| getAppsForName | | protected SetOfTacletApp getAppsForName(Goal goal, String name, PosInOccurrence pos, TacletFilter filter)(Code) | | collects all taclet applications for the given position and taclet
(identified by its name) matching the filter condition
Parameters:
goal - the Goal for which the applications should be returned
Parameters:
name - the String with the taclet names whose applications are looked for
Parameters:
pos - the PosInOccurrence describing the position
Parameters:
filter - the TacletFilter expressing restrictions a list of all found rule applications of the given rule atposition pos passing the filter |
| getBuiltInRule | | public ListOfBuiltInRule getBuiltInRule(PosInOccurrence pos, Constraint userConstraint)(Code) | | collects all built-in rules that are applicable at the given sequent
position 'pos'.
Parameters:
pos - the PosInSequent where to look for applicable rules
Parameters:
userConstraint - the user defined constraint |
| getBuiltInRuleApp | | public SetOfRuleApp getBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pos, Constraint userConstraint)(Code) | | collects all built-in rule applications for the given rule that are
applicable at position 'pos' and the current user constraint
Parameters:
rule - the BuiltInRule for which the applications are collected
Parameters:
pos - the PosInSequent the position information
Parameters:
userConstraint - the user defined constraint a SetOfRuleApp with all possible rule applications |
| getBuiltInRuleAppsForName | | protected SetOfRuleApp getBuiltInRuleAppsForName(String name, PosInOccurrence pos)(Code) | | collects all applications of a rule given by its name at a give position in the sequent
Parameters:
name - the name of the BuiltInRule for which applications are collected.
Parameters:
pos - the position in the sequent where the BuiltInRule should be applieda SetOfRuleApp with all possible applications of the rule |
| getFindTaclet | | ListOfTacletApp getFindTaclet(PosInSequent pos)(Code) | | collects all applicable FindTaclets of the current goal
(called by the SequentViewer)
a list of Taclets with all applicable FindTaclets |
| getNoFindTaclet | | ListOfTacletApp getNoFindTaclet()(Code) | | collects all applicable NoFindTaclets of the current goal (called by the
SequentViewer)
a list of Taclets with all applicable NoFindTaclets |
| getProof | | public Proof getProof()(Code) | | returns the proof the interactive prover is working on
the proof the interactive prover is working on |
| getRewriteTaclet | | ListOfTacletApp getRewriteTaclet(PosInSequent pos)(Code) | | collects all applicable RewriteTaclets of the current goal
(called by the SequentViewer)
a list of Taclets with all applicable RewriteTaclets |
| interactiveMode | | public boolean interactiveMode()(Code) | | |
| resumeAutoMode | | public boolean resumeAutoMode()(Code) | | |
| setInteractive | | public void setInteractive(boolean interact)(Code) | | |
| setProof | | public void setProof(Proof p)(Code) | | sets up a new proof
Parameters:
p - a Proof that contains the root of the proof tree |
| setResumeAutoMode | | void setResumeAutoMode(boolean b)(Code) | | |
| startAutoMode | | public void startAutoMode()(Code) | | starts the execution of rules with active strategy
|
| startAutoMode | | public void startAutoMode(ListOfGoal goals)(Code) | | starts the execution of rules with active strategy. The
strategy will only be applied on the goals of the list that
is handed over and on the new goals an applied rule adds
|
| startFocussedAutoMode | | public void startFocussedAutoMode(PosInOccurrence focus, Goal goal)(Code) | | starts the execution of rules with active strategy. Restrict the
application of rules to a particular goal and (for
focus!=null) to a particular subterm or subformula of
that goal
|
| stopAutoMode | | public void stopAutoMode()(Code) | | stops the execution of rules
|
|
|