de.uka.ilkd.key.strategy.feature

Class NonDuplicateAppFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

de.uka.ilkd.key.strategy.feature.AbstractNonDuplicateAppFeature

de.uka.ilkd.key.strategy.feature.NonDuplicateAppFeature

All Implemented Interfaces:

Feature

Direct Known Subclasses:

NonDuplicateAppModPositionFeature

public class NonDuplicateAppFeature
extends AbstractNonDuplicateAppFeature

Binary feature that returns zero iff a certain Taclet app has not already been performed

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	INSTANCE

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Constructor and Description
NonDuplicateAppFeature()

Method Summary

Modifier and Type	Method and Description
protected boolean	comparePio(TacletApp newApp, TacletApp oldApp, PosInOccurrence newPio, PosInOccurrence oldPio) Compare whether two PosInOccurrences are equal.
protected boolean	containsRuleApp(ImmutableList<RuleApp> list, TacletApp rapp, PosInOccurrence pio)
boolean	filter(TacletApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
protected boolean	semiSequentContains(Semisequent semisequent, SequentFormula cfma) Check whether a semisequent contains a formula.

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

noDuplicateFindTaclet, sameApplication

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

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

Field Detail

INSTANCE

public static final Feature INSTANCE

Constructor Detail

NonDuplicateAppFeature

public NonDuplicateAppFeature()

Method Detail

containsRuleApp

protected boolean containsRuleApp(ImmutableList<RuleApp> list,
                                  TacletApp rapp,
                                  PosInOccurrence pio)

filter

public boolean filter(TacletApp app,
                      PosInOccurrence pos,
                      Goal goal)

Description copied from class: BinaryTacletAppFeature

Compute whether the result of the feature is zero (true) or infinity (false)

Specified by:

filter in class BinaryTacletAppFeature

Parameters:

app - the TacletApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

true iff the the result of the feature is supposed to be zero.

comparePio

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

Description copied from class: AbstractNonDuplicateAppFeature

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

Specified by:

comparePio in class AbstractNonDuplicateAppFeature

semiSequentContains

protected boolean semiSequentContains(Semisequent semisequent,
                                      SequentFormula cfma)

Description copied from class: AbstractNonDuplicateAppFeature

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

Specified by:

semiSequentContains in class AbstractNonDuplicateAppFeature