| java.lang.Object de.uka.ilkd.key.strategy.feature.BinaryFeature de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature
All known Subclasses: de.uka.ilkd.key.strategy.feature.AutomatedRuleFeature, de.uka.ilkd.key.strategy.feature.DiffFindAndIfFeature, de.uka.ilkd.key.strategy.feature.TrivialMonomialLCRFeature, de.uka.ilkd.key.strategy.feature.MatchedIfFeature, de.uka.ilkd.key.strategy.feature.AbstractConstraintStrengthenFeature, de.uka.ilkd.key.strategy.feature.SmallerThanFeature, de.uka.ilkd.key.strategy.feature.TacletRequiringInstantiationFeature, de.uka.ilkd.key.strategy.feature.TopLevelFindFeature, de.uka.ilkd.key.strategy.quantifierHeuristics.ExistentiallyConnectedFormulasFeature, de.uka.ilkd.key.strategy.feature.AbstractNonDuplicateAppFeature, de.uka.ilkd.key.strategy.feature.ReducibleMonomialsFeature, de.uka.ilkd.key.strategy.feature.CheckApplyEqFeature, de.uka.ilkd.key.strategy.feature.NotWithinMVFeature, de.uka.ilkd.key.strategy.feature.InEquationMultFeature, de.uka.ilkd.key.strategy.feature.OnlyInScopeOfQuantifiersFeature, de.uka.ilkd.key.strategy.feature.UCIncompatibleFeature, de.uka.ilkd.key.strategy.feature.PolynomialValuesCmpFeature, de.uka.ilkd.key.strategy.feature.InstantiatedSVFeature,
BinaryTacletAppFeature | abstract public class BinaryTacletAppFeature extends BinaryFeature (Code) | | Abstract superclass for features of TacletApps that have either zero or top
cost.
|
BinaryTacletAppFeature | protected BinaryTacletAppFeature()(Code) | | |
BinaryTacletAppFeature | protected BinaryTacletAppFeature(boolean p_nonTacletValue)(Code) | | Parameters: p_nonTacletValue - the value that is to be returned should the feature be appliedto a rule that is not a taclet |
filter | abstract protected boolean filter(TacletApp app, PosInOccurrence pos, Goal goal)(Code) | | Compute whether the result of the feature is zero (true )
or infinity (false )
Parameters: app - the TacletApp Parameters: pos - position where app is to be applied Parameters: goal - the goal on which app is to be applied true iff the the result of the feature is supposed to be zero. |
|
|