de.uka.ilkd.key.strategy.feature

Class ApplyTFFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.ApplyTFFeature

All Implemented Interfaces:

Feature

public class ApplyTFFeature
extends java.lang.Object
implements Feature

Feature for invoking a term feature on the instantiation of a schema variable

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	demandInst
private RuleAppCost	noInstCost
private ProjectionToTerm	proj
private TermFeature	termFeature

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ApplyTFFeature(ProjectionToTerm proj, TermFeature termFeature, RuleAppCost noInstCost, boolean demandInst)

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(ProjectionToTerm proj, TermFeature tf)
static Feature	createNonStrict(ProjectionToTerm proj, TermFeature tf, RuleAppCost noInstCost)

Methods inherited from class java.lang.Object

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

Field Detail

proj

private final ProjectionToTerm proj

termFeature

private final TermFeature termFeature

noInstCost

private final RuleAppCost noInstCost

demandInst

private final boolean demandInst

Constructor Detail

ApplyTFFeature

private ApplyTFFeature(ProjectionToTerm proj,
                       TermFeature termFeature,
                       RuleAppCost noInstCost,
                       boolean demandInst)

Parameters:

proj - the ProjectionToTerm to the instantiation is supposed to be inspected

termFeature - the term feature to use

noInstCost - result if schemaVar is not instantiated

demandInst - if true then raise an exception if schemaVar is not instantiated (otherwise: return noInstCost)

Method Detail

createNonStrict

public static Feature createNonStrict(ProjectionToTerm proj,
                                      TermFeature tf,
                                      RuleAppCost noInstCost)

create

public static Feature create(ProjectionToTerm proj,
                             TermFeature tf)

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