de.uka.ilkd.key.strategy.feature.findprefix

Class FindPrefixRestrictionFeature

java.lang.Object

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

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

de.uka.ilkd.key.strategy.feature.findprefix.FindPrefixRestrictionFeature

All Implemented Interfaces:

Feature

public class FindPrefixRestrictionFeature
extends BinaryTacletAppFeature

Feature for investigating whether some restrictions to the prefix of the find formula apply.

Author:

christoph

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	FindPrefixRestrictionFeature.PositionModifier
static class	FindPrefixRestrictionFeature.PrefixChecker

Field Summary

Fields

Modifier and Type	Field and Description
private FindPrefixRestrictionFeature.PositionModifier[]	positionModifiers
private FindPrefixRestrictionFeature.PrefixChecker[]	prefixCheckers

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

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.

Method Summary

Modifier and Type	Method and Description
private boolean	checkPrefix(PosInOccurrence pos) Applies the PrefixCheckers.
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

prefixCheckers

private final FindPrefixRestrictionFeature.PrefixChecker[] prefixCheckers

positionModifiers

private final FindPrefixRestrictionFeature.PositionModifier[] positionModifiers

Constructor Detail

FindPrefixRestrictionFeature

public FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)

Construct a feature that checks the prefix with the passed PrefixCheckers. Computes zero costs, if all PrefixCheckers return true, otherwise computes top cost.

Parameters:

prefixCheckers - the PrefixCheckers to be used.

FindPrefixRestrictionFeature

public FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PositionModifier positionModifier,
                                    FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)

Construct a feature that checks the prefix with the passed PrefixCheckers. Computes zero costs, if all PrefixCheckers return true, otherwise computes top cost. Before the prefix check all PositionModifiers are applied. This allows for instance to ignore prefixing updates.

Parameters:

positionModifier - the PositionModifier to be applied.

prefixCheckers - the PrefixCheckers to be used.

FindPrefixRestrictionFeature

public FindPrefixRestrictionFeature(FindPrefixRestrictionFeature.PositionModifier[] positionModifiers,
                                    FindPrefixRestrictionFeature.PrefixChecker... prefixCheckers)

Construct a feature that checks the prefix with the passed PrefixCheckers. Computes zero costs, if all PrefixCheckers return true, otherwise computes top cost. Before the prefix check all PositionModifiers are applied. This allows for instance to ignore prefixing updates.

Parameters:

positionModifiers - the PositionModifiers to be applied.

prefixCheckers - the PrefixCheckers to be used.

Method Detail

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.

checkPrefix

private boolean checkPrefix(PosInOccurrence pos)

Applies the PrefixCheckers.

Parameters:

pos - the PosInOccurrence to be checked.

Returns:

true, if all PrefixCheckers return true