public class FindPrefixRestrictionFeature extends BinaryTacletAppFeature
Modifier and Type | Class and Description |
---|---|
static class |
FindPrefixRestrictionFeature.PositionModifier |
static class |
FindPrefixRestrictionFeature.PrefixChecker |
TOP_COST, ZERO_COST
Constructor and Description |
---|
FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PositionModifier[] positionModifiers,
FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)
Construct a feature that checks the prefix with the passed
PrefixCheckers.
|
FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PositionModifier positionModifier,
FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)
Construct a feature that checks the prefix with the passed
PrefixCheckers.
|
FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)
Construct a feature that checks the prefix with the passed
PrefixCheckers.
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
filter(TacletApp app,
PosInOccurrence pos,
Goal goal)
Compute whether the result of the feature is zero (
true )
or infinity (false ) |
filter
computeCost
public FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)
prefixCheckers
- the PrefixCheckers to be used.public FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PositionModifier positionModifier, FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)
positionModifier
- the PositionModifier to be applied.prefixCheckers
- the PrefixCheckers to be used.public FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PositionModifier[] positionModifiers, FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)
positionModifiers
- the PositionModifiers to be applied.prefixCheckers
- the PrefixCheckers to be used.protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal)
BinaryTacletAppFeature
true
)
or infinity (false
)filter
in class BinaryTacletAppFeature
app
- the TacletApppos
- position where app
is to be appliedgoal
- the goal on which app
is to be appliedCopyright © 2003-2019 The KeY-Project.