de.uka.ilkd.key.strategy.feature

Class DeleteMergePointRuleFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.DeleteMergePointRuleFeature

All Implemented Interfaces:

Feature

public class DeleteMergePointRuleFeature
extends java.lang.Object
implements Feature

Costs for the DeleteMergePointRule; incredibly cheap if the previous rule application was a MergeRule app, infinitely expensive otherwise. The alternative would be to always check whether there's another Goal around with the same MergePointStatement (then we may not delete), which is much more time intensive.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	INSTANCE

Constructor Summary

Constructors

Modifier	Constructor and Description
private	DeleteMergePointRuleFeature()

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pos, Goal goal) Evaluate the cost of a RuleApp.

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static final Feature INSTANCE

Constructor Detail

DeleteMergePointRuleFeature

private DeleteMergePointRuleFeature()

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