de.uka.ilkd.key.strategy.feature

Class LetFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.LetFeature

All Implemented Interfaces:

Feature

public class LetFeature
extends java.lang.Object
implements Feature

Feature for locally binding a TermBuffer to a certain value, namely to a term that is generated by a ProjectionToTerm. This is mostly useful to make feature terms more readable, and to avoid repeated evaluation of projections.

Field Summary

Fields

Modifier and Type	Field and Description
private Feature	body
private ProjectionToTerm	value
private TermBuffer	var

Constructor Summary

Constructors

Modifier	Constructor and Description
private	LetFeature(TermBuffer var, ProjectionToTerm value, Feature body)

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pos, Goal goal) Evaluate the cost of a RuleApp.
static Feature	create(TermBuffer var, ProjectionToTerm value, Feature body)

Methods inherited from class java.lang.Object

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

Field Detail

var

private final TermBuffer var

value

private final ProjectionToTerm value

body

private final Feature body

Constructor Detail

LetFeature

private LetFeature(TermBuffer var,
                   ProjectionToTerm value,
                   Feature body)

Method Detail

create

public static Feature create(TermBuffer var,
                             ProjectionToTerm value,
                             Feature body)

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