| java.lang.Object
 de.uka.ilkd.key.strategy.feature.AbstractBetaFeature
All known Subclasses: de.uka.ilkd.key.strategy.feature.CountMaxDPathFeature, de.uka.ilkd.key.strategy.feature.SimplifyBetaCandidateFeature, de.uka.ilkd.key.strategy.feature.LeftmostNegAtomFeature, de.uka.ilkd.key.strategy.feature.PurePosDPathFeature, de.uka.ilkd.key.strategy.feature.CountPosDPathFeature, de.uka.ilkd.key.strategy.feature.ContainsQuantifierFeature,
| AbstractBetaFeature | | abstract public class AbstractBetaFeature implements Feature(Code) | | This abstract class contains some auxiliary methods for the selection of
beta rules that are supposed to be applied. Used terminology is defined in
Diss. by Martin Giese.
|
| alwaysReplace | | public static boolean alwaysReplace(Term p_t)(Code) | | true iff the sign of "p_t" is not relevant (quantifiersetc. could be positive or negative) |
| compute | | public RuleAppCost compute(RuleApp app, PosInOccurrence pos, Goal goal)(Code) | | Compute the cost of a RuleApp.
Parameters:
app - the RuleApp
Parameters:
pos - position where app is to be applied
Parameters:
goal - the goal on which app is to be applied the cost of app |
| containsNegAtom | | protected static boolean containsNegAtom(Term p_t, boolean p_positive)(Code) | | true iff the givenformula contains a negated atom as a formula of the antecedent |
| containsQuantifier | | protected static boolean containsQuantifier(Term p_t)(Code) | | true iff "p_t" contains a quantifier or a modality |
| hasPurePosPath | | protected static boolean hasPurePosPath(Term p_t, boolean p_positive)(Code) | | p_t contains a d-path consisting only of positive literals (as a formula
of the antecedent)
|
| isBetaCandidate | | protected static boolean isBetaCandidate(Term p_t, boolean p_inAntec)(Code) | | true iff the formula p_t could be splitted using thebeta rule |
| maxDPath | | protected static int maxDPath(Term p_t, boolean p_positive)(Code) | | The length (number of literals) of the maximum d-path of the given
formula as a formula of the antecedent
|
| maxPosPath | | protected static int maxPosPath(Term p_t, boolean p_positive)(Code) | | The maximal number of positive literals occurring within a
d-path of "p_t" as a formula of the antecedent
|
|
|