de.uka.ilkd.key.macros.scripts

Class AutoCommand

java.lang.Object

de.uka.ilkd.key.macros.scripts.AbstractCommand<AutoCommand.Parameters>

de.uka.ilkd.key.macros.scripts.AutoCommand

All Implemented Interfaces:

ProofScriptCommand<AutoCommand.Parameters>

public class AutoCommand
extends AbstractCommand<AutoCommand.Parameters>

The AutoCommand invokes the automatic strategy "Auto".

Author:

Mattias Ulbrich, Alexander Weigl

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	AutoCommand.Parameters

Field Summary

Fields inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

documentation, log, proof, service, state, uiControl

Constructor Summary

Constructors

Constructor and Description
AutoCommand()

Method Summary

Modifier and Type	Method and Description
AutoCommand.Parameters	evaluateArguments(EngineState state, java.util.Map<java.lang.String,java.lang.String> arguments)
void	execute(AbstractUserInterfaceControl uiControl, AutoCommand.Parameters arguments, EngineState state)
java.lang.String	getName() Returns the name of this proof command.
private void	setupFocussedBreakpointStrategy(java.util.Optional<java.lang.String> maybeMatchesRegEx, java.util.Optional<java.lang.String> breakpointArg, Goal goal, ProverCore proverCore, Services services) Sets up a focused automatic strategy.

Methods inherited from class de.uka.ilkd.key.macros.scripts.AbstractCommand

execute, getArguments, getDocumentation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

AutoCommand

public AutoCommand()

Method Detail

getName

public java.lang.String getName()

Description copied from interface: ProofScriptCommand

Returns the name of this proof command. The name should be constant and not be clash with the name of other commands. The name is essential for finding this command within an hashmap.

Returns:

a non-null, non-empty string

See Also:

ProofScriptEngine

evaluateArguments

public AutoCommand.Parameters evaluateArguments(EngineState state,
                                                java.util.Map<java.lang.String,java.lang.String> arguments)

Specified by:

evaluateArguments in interface ProofScriptCommand<AutoCommand.Parameters>

Overrides:

evaluateArguments in class AbstractCommand<AutoCommand.Parameters>

Returns:

execute

public void execute(AbstractUserInterfaceControl uiControl,
                    AutoCommand.Parameters arguments,
                    EngineState state)
             throws ScriptException,
                    java.lang.InterruptedException

Specified by:

execute in interface ProofScriptCommand<AutoCommand.Parameters>

Overrides:

execute in class AbstractCommand<AutoCommand.Parameters>

Parameters:

uiControl - the current ui controller

arguments - the script arguments

state - the current state

Throws:

ScriptException - if something bad happens

java.lang.InterruptedException - if something bad happens

setupFocussedBreakpointStrategy

private void setupFocussedBreakpointStrategy(java.util.Optional<java.lang.String> maybeMatchesRegEx,
                                             java.util.Optional<java.lang.String> breakpointArg,
                                             Goal goal,
                                             ProverCore proverCore,
                                             Services services)
                                      throws ScriptException

Sets up a focused automatic strategy. Focus is on the sequent formula matching the matchesRegEx (may not be null).

Parameters:

maybeMatchesRegEx - The RegEx which should match on the sequent formula to focus.

breakpointArg - An optional breakpoint argument.

goal - The Goal to apply the strategy on, needed for the rule application manager.

proverCore - The ProverCore, needed for resetting the strategy afterward.

services - The Services object.

Throws:

ScriptException