de.uka.ilkd.key.macros

Class AbstractPropositionalExpansionMacro.PropExpansionStrategy

java.lang.Object

de.uka.ilkd.key.macros.AbstractPropositionalExpansionMacro.PropExpansionStrategy

All Implemented Interfaces:

Named, Feature, Strategy

Enclosing class:

AbstractPropositionalExpansionMacro

private class AbstractPropositionalExpansionMacro.PropExpansionStrategy
extends java.lang.Object
implements Strategy

This strategy accepts all rule apps for which the rule name is in the admitted set and rejects everything else.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Set<java.lang.String>	admittedRuleNames
private boolean	allowOSS
private Strategy	delegate
private Name	NAME

Constructor Summary

Constructors

Constructor and Description
PropExpansionStrategy(Strategy delegate, java.util.Set<java.lang.String> admittedRuleNames, boolean allowOSS)

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp ruleApp, 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) Re-Evaluate a RuleApp.
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 final Name NAME

admittedRuleNames

private final java.util.Set<java.lang.String> admittedRuleNames

delegate

private final Strategy delegate

allowOSS

private final boolean allowOSS

Constructor Detail

PropExpansionStrategy

public PropExpansionStrategy(Strategy delegate,
                             java.util.Set<java.lang.String> admittedRuleNames,
                             boolean allowOSS)

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

computeCost

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

Description copied from interface: Feature

Evaluate the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Parameters:

ruleApp - 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).

isApprovedApp

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

Description copied from interface: Strategy

Re-Evaluate a RuleApp. This method is called immediately before a rule is really applied

Specified by:

isApprovedApp in interface Strategy

Returns:

true iff the rule should be applied, false otherwise

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.