Package | Description |
---|---|
de.uka.ilkd.key.strategy.feature |
Modifier and Type | Class and Description |
---|---|
class |
ContainsQuantifierFeature
Binary feature that returns zero iff the focus of a rule contains a
quantifier
NB: this can nowadays be done more nicely using term features
|
class |
CountMaxDPathFeature
Feature that returns the maximum number of literals occurring within a d-path
of the find-formula as a formula of the antecedent.
|
class |
CountPosDPathFeature
Feature that returns the maximum number of positive literals occurring within
a d-path of the find-formula as a formula of the antecedent.
|
class |
LeftmostNegAtomFeature
Feature that returns zero if there is no atom with negative polarity on a
common d-path and on the left of the find-position within the find-formula as
a formula of the antecedent.
|
class |
PurePosDPathFeature
Binary feature that returns zero iff the find-formula of a rule contains a
d-path consisting only of positive literals (as a formula of the antecedent).
|
class |
SimplifyBetaCandidateFeature
Binary feature that returns zero iff the hyper-tableaux simplification method
approves the given application (which is supposed to be the application of a
beta rule).
|
Copyright © 2003-2019 The KeY-Project.