public abstract class AbstractNonDuplicateAppFeature extends BinaryTacletAppFeature
TOP_COST, ZERO_COST
Modifier | Constructor and Description |
---|---|
protected |
AbstractNonDuplicateAppFeature() |
Modifier and Type | Method and Description |
---|---|
protected abstract boolean |
comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio)
Compare whether two
PosInOccurrence s 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) |
filter, filter
computeCost
protected abstract boolean comparePio(TacletApp newApp, TacletApp oldApp, PosInOccurrence newPio, PosInOccurrence oldPio)
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 subclassesprotected abstract boolean semiSequentContains(Semisequent semisequent, SequentFormula cfma)
protected boolean sameApplication(RuleApp ruleCmp, TacletApp newApp, PosInOccurrence newPio)
ruleCmp
is a
duplicate of the new application newApp
at position
newPio
.newPio
can be null
private boolean equalInterestingInsts(SVInstantiations inst0, SVInstantiations inst1)
private boolean subset(ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts0, ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts1)
protected boolean noDuplicateFindTaclet(TacletApp app, PosInOccurrence pos, Goal goal)
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