de.uka.ilkd.key.macros

Class OneStepProofMacro.OneStepStrategy

java.lang.Object

de.uka.ilkd.key.macros.OneStepProofMacro.OneStepStrategy

All Implemented Interfaces:

Named, Feature, Strategy

Enclosing class:

OneStepProofMacro

private static class OneStepProofMacro.OneStepStrategy
extends java.lang.Object
implements Strategy

Strategy with counter, s.t. only one rule is applied

Field Summary

Fields

Modifier and Type	Field and Description
private int	counter
Strategy	delegate
private static Name	NAME

Constructor Summary

Constructors

Constructor and Description
OneStepStrategy(Strategy delegate)

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pio, Goal goal) Evaluate the cost of a RuleApp.
void	instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal, RuleAppCostCollector collector) Instantiate an incomplete RuleApp.
boolean	isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) If no rule was applied yet, apply the first rule and increase counter, s.t. no more rules can be applied.
boolean	isStopAtFirstNonCloseableGoal() Checks if the Strategy should stop at the first non closeable Goal.
Name	name() returns the name of this element

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.strategy.Strategy

updateStrategySettings

Field Detail

NAME

private static final Name NAME

counter

private int counter

delegate

public Strategy delegate

Constructor Detail

OneStepStrategy

public OneStepStrategy(Strategy delegate)

Method Detail

name

public Name name()

Description copied from interface: Named

returns the name of this element

Specified by:

name in interface Named

Returns:

the name of the element

isApprovedApp

public boolean isApprovedApp(RuleApp app,
                             PosInOccurrence pio,
                             Goal goal)

If no rule was applied yet, apply the first rule and increase counter, s.t. no more rules can be applied.

Specified by:

isApprovedApp in interface Strategy

Returns:

true iff the rule should be applied, false otherwise

computeCost

public RuleAppCost computeCost(RuleApp app,
                               PosInOccurrence pio,
                               Goal goal)

Description copied from interface: Feature

Evaluate the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Parameters:

app - the RuleApp

pio - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

the cost of the rule application expressed as a RuleAppCost object. TopRuleAppCost.INSTANCE indicates that the rule shall not be applied at all (it is discarded by the strategy).

instantiateApp

public void instantiateApp(RuleApp app,
                           PosInOccurrence pio,
                           Goal goal,
                           RuleAppCostCollector collector)

Description copied from interface: Strategy

Instantiate an incomplete RuleApp. This method is called when the AutomatedRuleApplicationManager comes across a rule application in which some schema variables are not yet instantiated, or which is in some other way incomplete. The strategy then has the opportunity to return/provide a list of (more) complete rule applications by feeding them into the provided RuleAppCostCollector.

Specified by:

instantiateApp in interface Strategy

isStopAtFirstNonCloseableGoal

public boolean isStopAtFirstNonCloseableGoal()

Description copied from interface: Strategy

Checks if the Strategy should stop at the first non closeable Goal.

Specified by:

isStopAtFirstNonCloseableGoal in interface Strategy

Returns:

true stop, false continue on other Goals.