de.uka.ilkd.key.macros

Class AbstractPropositionalExpansionMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

de.uka.ilkd.key.macros.AbstractPropositionalExpansionMacro

All Implemented Interfaces:

ProofMacro

Direct Known Subclasses:

FullPropositionalExpansionMacro, HeapSimplificationMacro, IntegerSimplificationMacro, PropositionalExpansionMacro, PropositionalExpansionWithSimplificationMacro, SelfcompositionStateExpansionMacro, UpdateSimplificationMacro

public abstract class AbstractPropositionalExpansionMacro
extends StrategyProofMacro

The Class AbstractPropositionalExpansionMacro applies purely propositional rules. The names of the set of rules to be applied is defined by the abstract method getAdmittedRuleNames(). This is very helpful to perform many "andLeft", "impRight" or even "andRight" steps at a time.

Author:

mattias ulbrich

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	AbstractPropositionalExpansionMacro.PropExpansionStrategy This strategy accepts all rule apps for which the rule name is in the admitted set and rejects everything else.

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

ProofMacro.ProgressBarListener

Constructor Summary

Constructors

Constructor and Description
AbstractPropositionalExpansionMacro()

Method Summary

Modifier and Type	Method and Description
protected abstract boolean	allowOSS() Whether this macro includes One Step Simplification.
protected static java.util.Set<java.lang.String>	asSet(java.lang.String... strings)
protected Strategy	createStrategy(Proof proof, PosInOccurrence posInOcc)
protected abstract java.util.Set<java.lang.String>	getAdmittedRuleNames() Gets the set of admitted rule names.
java.lang.String	getCategory() Gets the category of this macro.
protected boolean	ruleApplicationInContextAllowed(RuleApp ruleApp, PosInOccurrence pio, Goal goal) Checks whether the application of the passed rule is ok in the given context.

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, 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

getDescription, getName

Constructor Detail

AbstractPropositionalExpansionMacro

public AbstractPropositionalExpansionMacro()

Method Detail

asSet

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

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

getAdmittedRuleNames

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

Gets the set of admitted rule names.

Returns:

a constant non-null set

allowOSS

protected abstract boolean allowOSS()

Whether this macro includes One Step Simplification.

createStrategy

protected Strategy createStrategy(Proof proof,
                                  PosInOccurrence posInOcc)

Specified by:

createStrategy in class StrategyProofMacro

ruleApplicationInContextAllowed

protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp,
                                                  PosInOccurrence pio,
                                                  Goal goal)

Checks whether the application of the passed rule is ok in the given context.

Parameters:

ruleApp - rule to be applied

pio - context

goal - context

Returns:

true if rule may be applied