de.uka.ilkd.key.strategy.feature

Class AbstractNonDuplicateAppFeature

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 Implemented Interfaces:

Feature

Direct Known Subclasses:

EqNonDuplicateAppFeature, NonDuplicateAppFeature

public abstract class AbstractNonDuplicateAppFeature
extends BinaryTacletAppFeature

Field Summary

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractNonDuplicateAppFeature()

Method Summary

Modifier and Type	Method and Description
protected abstract boolean	comparePio(TacletApp newApp, TacletApp oldApp, PosInOccurrence newPio, PosInOccurrence oldPio) Compare whether two PosInOccurrences are equal.
private boolean	equalInterestingInsts(SVInstantiations inst0, SVInstantiations inst1)
protected boolean	noDuplicateFindTaclet(TacletApp app, PosInOccurrence pos, Goal goal) Search for a duplicate of the application app by walking upwards in the proof tree.
protected boolean	sameApplication(RuleApp ruleCmp, TacletApp newApp, PosInOccurrence newPio) Check whether the old rule application ruleCmp is a duplicate of the new application newApp at position newPio.
protected abstract boolean	semiSequentContains(Semisequent semisequent, SequentFormula cfma) Check whether a semisequent contains a formula.
private boolean	subset(ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts0, ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts1)

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

filter, filter

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

AbstractNonDuplicateAppFeature

protected AbstractNonDuplicateAppFeature()

Method Detail

comparePio

protected abstract boolean comparePio(TacletApp newApp,
                                      TacletApp oldApp,
                                      PosInOccurrence newPio,
                                      PosInOccurrence oldPio)

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

semiSequentContains

protected abstract boolean semiSequentContains(Semisequent semisequent,
                                               SequentFormula cfma)

Check whether a semisequent contains a formula. Again, one can either search for the same or an equal formula

sameApplication

protected boolean sameApplication(RuleApp ruleCmp,
                                  TacletApp newApp,
                                  PosInOccurrence newPio)

Check whether the old rule application ruleCmp is a duplicate of the new application newApp at position newPio.newPio can be null

equalInterestingInsts

private boolean equalInterestingInsts(SVInstantiations inst0,
                                      SVInstantiations inst1)

subset

private boolean subset(ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts0,
                       ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts1)

noDuplicateFindTaclet

protected boolean noDuplicateFindTaclet(TacletApp app,
                                        PosInOccurrence pos,
                                        Goal goal)

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