public class EqNonDuplicateAppFeature extends AbstractNonDuplicateAppFeature
NonDuplicateAppFeature
, this feature
is also able to handle failing meta-constructs correctly (these constructs
return equal, but not identical formulas in case of a failure), but is less
efficient.Modifier and Type | Field and Description |
---|---|
static Feature |
INSTANCE |
TOP_COST, ZERO_COST
Modifier | Constructor and Description |
---|---|
private |
EqNonDuplicateAppFeature() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio)
Compare whether two
PosInOccurrence s are equal. |
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
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 semiSequentContains(Semisequent semisequent, SequentFormula cfma)
AbstractNonDuplicateAppFeature
semiSequentContains
in class AbstractNonDuplicateAppFeature
protected 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