de.uka.ilkd.key.strategy

Class IntroducedSymbolBy

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

de.uka.ilkd.key.strategy.IntroducedSymbolBy

All Implemented Interfaces:

Feature

public class IntroducedSymbolBy
extends BinaryTacletAppFeature

Field Summary

Fields

Modifier and Type	Field and Description
private Name	ruleSetName
private Name	schemaVar
private ProjectionToTerm	term

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	IntroducedSymbolBy(ProjectionToTerm termWithTopLevelOpToCheck, Name ruleSetName, Name schemaVar)

Method Summary

Modifier and Type	Method and Description
static Feature	create(ProjectionToTerm termWithTopLevelOpToCheck, java.lang.String ruleSetName, java.lang.String schemaVar)
protected boolean	filter(TacletApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

filter

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

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

Field Detail

ruleSetName

private final Name ruleSetName

schemaVar

private final Name schemaVar

term

private final ProjectionToTerm term

Constructor Detail

IntroducedSymbolBy

protected IntroducedSymbolBy(ProjectionToTerm termWithTopLevelOpToCheck,
                             Name ruleSetName,
                             Name schemaVar)

Method Detail

create

public static Feature create(ProjectionToTerm termWithTopLevelOpToCheck,
                             java.lang.String ruleSetName,
                             java.lang.String schemaVar)

filter

protected boolean filter(TacletApp app,
                         PosInOccurrence pos,
                         Goal goal)

Description copied from class: BinaryTacletAppFeature

Compute whether the result of the feature is zero (true) or infinity (false)

Specified by:

filter in class BinaryTacletAppFeature

Parameters:

app - the TacletApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

true iff the the result of the feature is supposed to be zero.