de.uka.ilkd.key.macros

Class StrategyProofMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

All Implemented Interfaces:

ProofMacro

Direct Known Subclasses:

AbstractBlastingMacro, AbstractPropositionalExpansionMacro, AutoMacro, AutoPilotPrepareProofMacro, FinishSymbolicExecutionMacro, FinishSymbolicExecutionUntilMergePointMacro, OneStepProofMacro, PrepareInfFlowContractPreBranchesMacro, TestGenMacro, UseInformationFlowContractMacro, WellDefinednessMacro

public abstract class StrategyProofMacro
extends AbstractProofMacro

The abstract class StrategyProofMacro can be used to define proof macros which use their own strategy. In order to implement a StrategyProofMacro, override #createStrategy(KeYMediator, PosInOccurrence). This class is aware of Position in occurrences and can also be applied to inner nodes. Both AutomatedRuleApplicationManager and Strategy are changed for the course of the macro but are restored afterwards using a ProverTaskListener.

See Also:

ProverTaskListener, Strategy

Nested Class Summary

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

ProofMacro.ProgressBarListener

Constructor Summary

Constructors

Constructor and Description
StrategyProofMacro()

Method Summary

Modifier and Type	Method and Description
ProofMacroFinishedInfo	applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) Apply this macro on the given goals.
boolean	canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc) Can this macro be applied on the given goals?
protected abstract Strategy	createStrategy(Proof proof, PosInOccurrence posInOcc)
protected void	doPostProcessing(Proof proof) Subclasses can use this method to do some postprocessing on the proof-object after the strategy has finished.
private static ImmutableList<Goal>	setDifference(ImmutableList<Goal> goals1, ImmutableList<Goal> goals2)

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

applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.macros.ProofMacro

getCategory, getDescription, getName

Constructor Detail

StrategyProofMacro

public StrategyProofMacro()

Method Detail

createStrategy

protected abstract Strategy createStrategy(Proof proof,
                                           PosInOccurrence posInOcc)

canApplyTo

public boolean canApplyTo(Proof proof,
                          ImmutableList<Goal> goals,
                          PosInOccurrence posInOcc)

Can this macro be applied on the given goals? This method should not make any changes but check if the macro can be applied or not on the given goals. This method may be called from within the GUI thread and be compatible with that fact. This macro can always be applied (does not change anything perhaps) TODO make this only applicable if it has an impact.

Parameters:

proof - the current Proof (not null)

goals - the goals (not null)

posInOcc - the position in occurrence (may be null)

Returns:

true, if the macro is allowed to be applied

doPostProcessing

protected void doPostProcessing(Proof proof)

Subclasses can use this method to do some postprocessing on the proof-object after the strategy has finished.

Parameters:

proof - The proof object.

applyTo

public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic,
                                      Proof proof,
                                      ImmutableList<Goal> goals,
                                      PosInOccurrence posInOcc,
                                      ProverTaskListener listener)
                               throws java.lang.InterruptedException

Description copied from interface: ProofMacro

Apply this macro on the given goals. This method can change the proof by applying rules to it. This method is usually called from a dedicated thread and not the GUI thread. The thread it runs on may be interrupted. In this case, the macro may report the interruption by an InterruptedException. A ProverTaskListener can be provided to which the progress will be reported. If no reports are desired, null cna be used for this parameter. If more than one listener is needed, consider combining them using a single listener object using the composite pattern.

Parameters:

uic - the UserInterfaceControl to use

proof - the current Proof (not null)

goals - the goals (not null)

posInOcc - the position in occurrence (may be null)

listener - the listener to use for progress reports (may be null)

Throws:

java.lang.InterruptedException - if the application of the macro has been interrupted.

setDifference

private static ImmutableList<Goal> setDifference(ImmutableList<Goal> goals1,
                                                 ImmutableList<Goal> goals2)