de.uka.ilkd.key.strategy.feature

Class BinaryTacletAppFeature

java.lang.Object

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

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

All Implemented Interfaces:

Feature

Direct Known Subclasses:

AbstractNonDuplicateAppFeature, AutomatedRuleFeature, CheckApplyEqFeature, DiffFindAndIfFeature, DiffFindAndReplacewithFeature, ExistentiallyConnectedFormulasFeature, FindPrefixRestrictionFeature, InEquationMultFeature, InstantiatedSVFeature, IntroducedSymbolBy, MatchedIfFeature, NoSelfApplicationFeature, OnlyInScopeOfQuantifiersFeature, PolynomialValuesCmpFeature, ReducibleMonomialsFeature, SmallerThanFeature, TacletRequiringInstantiationFeature, TopLevelFindFeature, TriggerVarInstantiatedFeature, TrivialMonomialLCRFeature

public abstract class BinaryTacletAppFeature
extends BinaryFeature

Abstract superclass for features of TacletApps that have either zero or top cost.

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	nonTacletValue

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	BinaryTacletAppFeature()
protected	BinaryTacletAppFeature(boolean p_nonTacletValue)

Method Summary

Modifier and Type	Method and Description
protected boolean	filter(RuleApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
protected abstract 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.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

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

Field Detail

nonTacletValue

private final boolean nonTacletValue

Constructor Detail

BinaryTacletAppFeature

protected BinaryTacletAppFeature()

BinaryTacletAppFeature

protected BinaryTacletAppFeature(boolean p_nonTacletValue)

Parameters:

p_nonTacletValue - the value that is to be returned should the feature be applied to a rule that is not a taclet

Method Detail

filter

protected final boolean filter(RuleApp app,
                               PosInOccurrence pos,
                               Goal goal)

Description copied from class: BinaryFeature

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

Specified by:

filter in class BinaryFeature

Parameters:

app - the RuleApp

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.

filter

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

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

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.