public class DirectlyBelowSymbolFeature extends DirectlyBelowFeature
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 insteadbadSymbol
TOP_COST, ZERO_COST
Modifier and Type | Method and Description |
---|---|
static Feature |
create(Operator badSymbol) |
static Feature |
create(Operator badSymbol,
int index) |
protected boolean |
isBadSymbol(Operator op) |
filter
computeCost
protected boolean isBadSymbol(Operator op)
isBadSymbol
in class DirectlyBelowFeature
Copyright © 2003-2019 The KeY-Project.