de.uka.ilkd.key.strategy.feature

Class RuleSetDispatchFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.RuleSetDispatchFeature

All Implemented Interfaces:

Feature

public class RuleSetDispatchFeature
extends java.lang.Object
implements Feature

Feature for relating rule sets with feature terms. Given a taclet application, this feature will iterate over the rule sets that the taclet belongs to, and for each rule set the corresponding feature term (if existing) is evaluated. The result of the feature is the sum of the results of the different rule set features.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<RuleSet,Feature>	rulesetToFeature

Constructor Summary

Constructors

Constructor and Description
RuleSetDispatchFeature()

Method Summary

Modifier and Type	Method and Description
void	add(RuleSet ruleSet, Feature f) Bind feature f to the rule set ruleSet.
void	clear(RuleSet ruleSet) Remove all features that have been related to ruleSet.
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pos, Goal goal) Evaluate the cost of a RuleApp.
Feature	get(RuleSet ruleSet) Returns the used Feature for the given RuleSet.

Methods inherited from class java.lang.Object

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

Field Detail

rulesetToFeature

private final java.util.Map<RuleSet,Feature> rulesetToFeature

Constructor Detail

RuleSetDispatchFeature

public RuleSetDispatchFeature()

Method Detail

computeCost

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

Description copied from interface: Feature

Evaluate the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Parameters:

app - the RuleApp

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

add

public void add(RuleSet ruleSet,
                Feature f)

Bind feature f to the rule set ruleSet. If this method is called more than once for the same rule set, the given features are added to each other.

clear

public void clear(RuleSet ruleSet)

Remove all features that have been related to ruleSet.

get

public Feature get(RuleSet ruleSet)

Returns the used Feature for the given RuleSet.

Parameters:

ruleSet - The RuleSet to get its Feature.

Returns:

The Feature used for the given RuleSet or null if not available.