de.uka.ilkd.key.macros

Class AutoMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

de.uka.ilkd.key.macros.AutoMacro

All Implemented Interfaces:

ProofMacro

public class AutoMacro
extends StrategyProofMacro

The macro AutoMacro is a customizable ProofMacro for use in proof scripts. It is possible to

• set a breakpoint statement which makes the macro stop when the breakpoint is reached (option "breakpoint", default is no breakpoint),
• prevent the proof from splitting (option "splits", default is true, i.e., splitting allowed),
• whitelist certain rule names which will always be allowed, even after a breakpoint (option "whitelist", default is none, supply a comma-separated list of rule names),
• limit the rule applications to those working on formulas with a modality (parameter "symbex-only", default is true),
• prevent the application of rules that are tagged as not "human-readable" (parameter "human-readable-only", default is true).

All parameters are optional, the default configuration works like the FinishSymbolicExecutionMacro. The parameters mentioned above have to be prefixed with "arg_" in proof scripts. From proof scripts, it is also possible (for all macros, and so also for this one) to start the macro on one particular formula (via parameter "occ") and thus to realize focussed applications.

Author:

Dominic Steinhoefel

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	AutoMacro.AutoMacroFilterStrategy The Class FilterAppManager is a special strategy assigning to any rule infinite costs if the goal has no modality

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	ALLOW_SPLITS_PARAM_NAME argument name
private boolean	allowSplits True iff splits allowed.
private java.util.Optional<java.lang.String>	breakpoint The breakpoint parameter: String repr. of the statements
private static java.lang.String	BREAKPOINT_PARAM_NAME argument name
private static java.lang.String	ONLY_HUMAN_PARAM_NAME argument name
private boolean	onlyHumanReadable Set to true to suppress all rules tagged as "non-human readable"
private static java.lang.String[]	PARAMS All names of currently implemented parameters belong here.
private static java.lang.String	SYMBEX_ONLY_PARAM_NAME argument name
private boolean	symbexOnly Set to true to suppress all non-symbex rules
private java.util.List<java.lang.String>	whitelist Rules which never should be suppressed
private static java.lang.String	WHITELIST_PARAM_NAME argument name

Constructor Summary

Constructors

Constructor and Description
AutoMacro()

Method Summary

Modifier and Type	Method and Description
private boolean	checkBoolean(java.lang.String paramName, java.lang.String paramValue)
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.
boolean	hasParameter(java.lang.String paramName) Checks whether this ProofMacro has a parameter named paramName.
private static boolean	isSplittingTaclet(Rule taclet)
void	resetParams() Resets the macro parameters to their defaults.
void	setParameter(java.lang.String paramName, java.lang.String paramValue) Sets the parameter named paramName to the given String representation in paramValue.

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

Methods inherited from class java.lang.Object

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

Field Detail

BREAKPOINT_PARAM_NAME

private static final java.lang.String BREAKPOINT_PARAM_NAME

argument name

See Also:

Constant Field Values

ALLOW_SPLITS_PARAM_NAME

private static final java.lang.String ALLOW_SPLITS_PARAM_NAME

argument name

See Also:

Constant Field Values

WHITELIST_PARAM_NAME

private static final java.lang.String WHITELIST_PARAM_NAME

argument name

See Also:

Constant Field Values

SYMBEX_ONLY_PARAM_NAME

private static final java.lang.String SYMBEX_ONLY_PARAM_NAME

argument name

See Also:

Constant Field Values

ONLY_HUMAN_PARAM_NAME

private static final java.lang.String ONLY_HUMAN_PARAM_NAME

argument name

See Also:

Constant Field Values

PARAMS

private static final java.lang.String[] PARAMS

All names of currently implemented parameters belong here.

breakpoint

private java.util.Optional<java.lang.String> breakpoint

The breakpoint parameter: String repr. of the statements

allowSplits

private boolean allowSplits

True iff splits allowed.

whitelist

private java.util.List<java.lang.String> whitelist

Rules which never should be suppressed

symbexOnly

private boolean symbexOnly

Set to true to suppress all non-symbex rules

onlyHumanReadable

private boolean onlyHumanReadable

Set to true to suppress all rules tagged as "non-human readable"

Constructor Detail

AutoMacro

public AutoMacro()

Method Detail

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

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

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

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

resetParams

public void resetParams()

Description copied from interface: ProofMacro

Resets the macro parameters to their defaults.

Specified by:

resetParams in interface ProofMacro

Overrides:

resetParams in class AbstractProofMacro

hasParameter

public boolean hasParameter(java.lang.String paramName)

Description copied from interface: ProofMacro

Checks whether this ProofMacro has a parameter named paramName. For use in proof scripts.

Specified by:

hasParameter in interface ProofMacro

Overrides:

hasParameter in class AbstractProofMacro

Parameters:

paramName - The name to check.

Returns:

true iff this ProofMacro has a parameter named paramName.

setParameter

public void setParameter(java.lang.String paramName,
                         java.lang.String paramValue)
                  throws java.lang.IllegalArgumentException

Description copied from interface: ProofMacro

Sets the parameter named paramName to the given String representation in paramValue. For use in proof scripts.

Specified by:

setParameter in interface ProofMacro

Overrides:

setParameter in class AbstractProofMacro

Parameters:

paramName - The name of the parameter.

paramValue - The value of the parameter.

Throws:

java.lang.IllegalArgumentException - if there is no parameter of that name or the value is incorrectly formatted (e.g., cannot be converted to a number).

checkBoolean

private boolean checkBoolean(java.lang.String paramName,
                             java.lang.String paramValue)

createStrategy

protected Strategy createStrategy(Proof proof,
                                  PosInOccurrence posInOcc)

Specified by:

createStrategy in class StrategyProofMacro

isSplittingTaclet

private static boolean isSplittingTaclet(Rule taclet)