de.uka.ilkd.key.macros

Class AutoPilotPrepareProofMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro

All Implemented Interfaces:

ProofMacro

public class AutoPilotPrepareProofMacro
extends StrategyProofMacro

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	AutoPilotPrepareProofMacro.AutoPilotStrategy

Nested classes/interfaces inherited from interface de.uka.ilkd.key.macros.ProofMacro

ProofMacro.ProgressBarListener

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String[]	ADMITTED_RULES
private static java.util.Set<java.lang.String>	ADMITTED_RULES_SET
private static Name	NON_HUMAN_INTERACTION_RULESET

Constructor Summary

Constructors

Constructor and Description
AutoPilotPrepareProofMacro()

Method Summary

Modifier and Type	Method and Description
protected static java.util.Set<java.lang.String>	asSet(java.lang.String[] strings)
protected Strategy	createStrategy(Proof proof, PosInOccurrence posInOcc)
java.lang.String	getCategory() Gets the category of this macro.
java.lang.String	getDescription() Gets the description of this macro.
java.lang.String	getName() Gets the name of this macro.
java.lang.String	getScriptCommandName() Gets a unique short name for this macro that can be used in proof scripts.
private static boolean	hasModality(Node node)
private static boolean	hasModality(Term term)
private static boolean	isInRuleSet(Rule rule, Name ruleSetName)
private static boolean	isNonHumanInteractionTagged(Rule rule)

Methods inherited from class de.uka.ilkd.key.macros.StrategyProofMacro

applyTo, canApplyTo, doPostProcessing

Methods inherited from class de.uka.ilkd.key.macros.AbstractProofMacro

applyTo, canApplyTo, getMaxSteps, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

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

Field Detail

ADMITTED_RULES

private static final java.lang.String[] ADMITTED_RULES

ADMITTED_RULES_SET

private static final java.util.Set<java.lang.String> ADMITTED_RULES_SET

NON_HUMAN_INTERACTION_RULESET

private static final Name NON_HUMAN_INTERACTION_RULESET

Constructor Detail

AutoPilotPrepareProofMacro

public AutoPilotPrepareProofMacro()

Method Detail

getName

public java.lang.String getName()

Description copied from interface: ProofMacro

Gets the name of this macro. Used as menu entry

Returns:

a non-null constant string

getCategory

public java.lang.String getCategory()

Description copied from interface: ProofMacro

Gets the category of this macro. Used as name of the menu under which the macro is sorted. Return null if no submenu is to be created.

Returns:

a constant string, or null

getDescription

public java.lang.String getDescription()

Description copied from interface: ProofMacro

Gets the description of this macro. Used as tooltip.

Returns:

a non-null constant string

getScriptCommandName

public java.lang.String getScriptCommandName()

Description copied from class: AbstractProofMacro

Gets a unique short name for this macro that can be used in proof scripts. If null is returned, the macro cannot be addressed from within scripts. By default, proof macros do not support scripts, thus null is returned.

Specified by:

getScriptCommandName in interface ProofMacro

Overrides:

getScriptCommandName in class AbstractProofMacro

Returns:

null if not supported, or a non-null constant string as the short name

asSet

protected static java.util.Set<java.lang.String> asSet(java.lang.String[] strings)

hasModality

private static boolean hasModality(Node node)

hasModality

private static boolean hasModality(Term term)

isNonHumanInteractionTagged

private static boolean isNonHumanInteractionTagged(Rule rule)

isInRuleSet

private static boolean isInRuleSet(Rule rule,
                                   Name ruleSetName)

createStrategy

protected Strategy createStrategy(Proof proof,
                                  PosInOccurrence posInOcc)

Specified by:

createStrategy in class StrategyProofMacro