de.uka.ilkd.key.strategy.feature

Class ContainsTermFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.ContainsTermFeature

All Implemented Interfaces:

Feature

public class ContainsTermFeature
extends java.lang.Object
implements Feature

Feature for checking if the term of the first projection contains the term of the second projection.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	ContainsTermFeature.ContainsTermVisitor

Field Summary

Fields

Modifier and Type	Field and Description
private ProjectionToTerm	proj1
private ProjectionToTerm	proj2
static RuleAppCost	TOP_COST Constant that represents the boolean value false
static RuleAppCost	ZERO_COST Constant that represents the boolean value true

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ContainsTermFeature(ProjectionToTerm proj1, ProjectionToTerm proj2)

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 proj1, ProjectionToTerm proj2)

Methods inherited from class java.lang.Object

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

Field Detail

ZERO_COST

public static final RuleAppCost ZERO_COST

Constant that represents the boolean value true

TOP_COST

public static final RuleAppCost TOP_COST

Constant that represents the boolean value false

proj1

private final ProjectionToTerm proj1

proj2

private final ProjectionToTerm proj2

Constructor Detail

ContainsTermFeature

private ContainsTermFeature(ProjectionToTerm proj1,
                            ProjectionToTerm proj2)

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

create

public static Feature create(ProjectionToTerm proj1,
                             ProjectionToTerm proj2)

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