de.uka.ilkd.key.strategy.feature

Class DirectlyBelowSymbolFeature

java.lang.Object

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

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

de.uka.ilkd.key.strategy.feature.DirectlyBelowSymbolFeature

All Implemented Interfaces:

Feature

public class DirectlyBelowSymbolFeature
extends DirectlyBelowFeature

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 inherited from class de.uka.ilkd.key.strategy.feature.DirectlyBelowFeature

badSymbol

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	DirectlyBelowSymbolFeature(Operator badSymbol, int index)

Method Summary

Modifier and Type	Method and Description
static Feature	create(Operator badSymbol)
static Feature	create(Operator badSymbol, int index)
protected boolean	isBadSymbol(Operator op)

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

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

Constructor Detail

DirectlyBelowSymbolFeature

private DirectlyBelowSymbolFeature(Operator badSymbol,
                                   int index)

Method Detail

create

public static Feature create(Operator badSymbol)

create

public static Feature create(Operator badSymbol,
                             int index)

isBadSymbol

protected boolean isBadSymbol(Operator op)

Specified by:

isBadSymbol in class DirectlyBelowFeature