| java.lang.Object
 de.uka.ilkd.key.strategy.feature.BinaryFeature
de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature
de.uka.ilkd.key.strategy.feature.AbstractNonDuplicateAppFeature
All known Subclasses: de.uka.ilkd.key.strategy.feature.NonDuplicateAppFeature, de.uka.ilkd.key.strategy.feature.EqNonDuplicateAppFeature,
| AbstractNonDuplicateAppFeature | | protected AbstractNonDuplicateAppFeature()(Code) | | |
| comparePio | | abstract protected boolean comparePio(TacletApp newApp, TacletApp oldApp, PosInOccurrence newPio, PosInOccurrence oldPio)(Code) | | Compare whether two PosInOccurrences are equal. This can be
done using equals or eqEquals (checking for
same or equal formulas), which has to be decided by the subclasses
|
| noDuplicateFindTaclet | | protected boolean noDuplicateFindTaclet(TacletApp app, PosInOccurrence pos, Goal goal)(Code) | | Search for a duplicate of the application app by walking
upwards in the proof tree. Here, we assume that pos is
non-null, and as an optimisation we stop as soon as we have reached a
point where the formula containing the focus no longer occurs in the
sequent
|
| sameApplication | | protected boolean sameApplication(RuleApp ruleCmp, TacletApp newApp, PosInOccurrence newPio)(Code) | | Check whether the old rule application ruleCmp is a
duplicate of the new application newApp at position
newPio.newPio can be null
|
| semiSequentContains | | abstract protected boolean semiSequentContains(Semisequent semisequent, ConstrainedFormula cfma)(Code) | | Check whether a semisequent contains a formula. Again, one can either
search for the same or an equal formula
|
|
|