public class NonDuplicateAppFeature extends AbstractNonDuplicateAppFeature
Modifier and Type | Field and Description |
---|---|
static Feature |
INSTANCE |
TOP_COST, ZERO_COST
Constructor and Description |
---|
NonDuplicateAppFeature() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio)
Compare whether two
PosInOccurrence s 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.
|
noDuplicateFindTaclet, sameApplication
filter
computeCost
public static final Feature INSTANCE
protected boolean containsRuleApp(ImmutableList<RuleApp> list, TacletApp rapp, PosInOccurrence pio)
public boolean filter(TacletApp app, PosInOccurrence pos, Goal goal)
BinaryTacletAppFeature
true
)
or infinity (false
)filter
in class BinaryTacletAppFeature
app
- the TacletApppos
- position where app
is to be appliedgoal
- the goal on which app
is to be appliedprotected boolean comparePio(TacletApp newApp, TacletApp oldApp, PosInOccurrence newPio, PosInOccurrence oldPio)
AbstractNonDuplicateAppFeature
PosInOccurrence
s are equal. This can be
done using equals
or eqEquals
(checking for
same or equal formulas), which has to be decided by the subclassescomparePio
in class AbstractNonDuplicateAppFeature
protected boolean semiSequentContains(Semisequent semisequent, SequentFormula cfma)
AbstractNonDuplicateAppFeature
semiSequentContains
in class AbstractNonDuplicateAppFeature