de.uka.ilkd.key.macros

Class AbstractBlastingMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

de.uka.ilkd.key.macros.AbstractBlastingMacro

All Implemented Interfaces:

ProofMacro

Direct Known Subclasses:

SemanticsBlastingMacro

public abstract class AbstractBlastingMacro
extends StrategyProofMacro

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	AbstractBlastingMacro.SemanticsBlastingStrategy

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

ProofMacro.ProgressBarListener

Constructor Summary

Constructors

Constructor and Description
AbstractBlastingMacro()

Method Summary

Modifier and Type	Method and Description
protected void	addInvariantFormula(Goal goal)
ProofMacroFinishedInfo	applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) Apply this macro on the given goals.
private boolean	containsSubTypes(Sort s, java.util.Set<Sort> sorts)
private java.util.List<SequentFormula>	createFormulae(Services services, java.util.Set<Sort> sorts)
protected Strategy	createStrategy(Proof proof, PosInOccurrence posInOcc)
protected abstract java.util.Set<java.lang.String>	getAllowedPullOut()
protected abstract RuleFilter	getEqualityRuleFilter()
protected abstract RuleFilter	getSemanticsRuleFilter()

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

canApplyTo, doPostProcessing

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

AbstractBlastingMacro

public AbstractBlastingMacro()

Method Detail

getSemanticsRuleFilter

protected abstract RuleFilter getSemanticsRuleFilter()

getEqualityRuleFilter

protected abstract RuleFilter getEqualityRuleFilter()

getAllowedPullOut

protected abstract java.util.Set<java.lang.String> getAllowedPullOut()

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.

Specified by:

applyTo in interface ProofMacro

Overrides:

applyTo in class StrategyProofMacro

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.

addInvariantFormula

protected void addInvariantFormula(Goal goal)

createStrategy

protected Strategy createStrategy(Proof proof,
                                  PosInOccurrence posInOcc)

Specified by:

createStrategy in class StrategyProofMacro

containsSubTypes

private boolean containsSubTypes(Sort s,
                                 java.util.Set<Sort> sorts)

createFormulae

private java.util.List<SequentFormula> createFormulae(Services services,
                                                      java.util.Set<Sort> sorts)