de.uka.ilkd.key.strategy.feature

Class DirectlyBelowFeature

java.lang.Object

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

de.uka.ilkd.key.strategy.feature.DirectlyBelowFeature

All Implemented Interfaces:

Feature

Direct Known Subclasses:

DirectlyBelowSymbolFeature

public abstract class DirectlyBelowFeature
extends BinaryFeature

This feature returns zero if and only if the focus of the given rule application exists, is not top-level and the symbol immediately above the focus is badSymbol. Optionally, one can also specify that zero should only be returned if the symbol immediately above the focus is badSymbol and the focus has a certain subterm index. TODO: eliminate this class and use term features instead

Field Summary

Fields

Modifier and Type	Field and Description
protected java.lang.Object	badSymbol
private int	index

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	DirectlyBelowFeature(java.lang.Object badSymbol, int index)

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	isBadSymbol(Operator op)

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

badSymbol

protected final java.lang.Object badSymbol

index

private final int index

Constructor Detail

DirectlyBelowFeature

protected DirectlyBelowFeature(java.lang.Object badSymbol,
                               int index)

Method Detail

filter

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

isBadSymbol

protected abstract boolean isBadSymbol(Operator op)