Modifier | Constructor and Description |
---|---|
protected |
InfFlowContractAppFeature() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
comparePio(TacletApp newApp,
TacletApp oldApp,
PosInOccurrence newPio,
PosInOccurrence oldPio)
Compare whether two
PosInOccurrence s are equal. |
RuleAppCost |
computeCost(RuleApp ruleApp,
PosInOccurrence pos,
Goal goal)
Evaluate the cost of a
RuleApp . |
protected boolean |
duplicateFindTaclet(TacletApp app,
PosInOccurrence pos,
Goal goal)
Search for a duplicate of the application
app by walking upwards in the proof tree. |
private boolean |
equalInterestingInsts(SVInstantiations inst0,
SVInstantiations inst1) |
private java.util.ArrayList<SequentFormula> |
getRelatesTerms(Goal goal) |
private boolean |
isInfFlowProof(Proof proof) |
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 boolean |
semiSequentContains(Semisequent semisequent,
SequentFormula cfma)
Check whether a semisequent contains a formula.
|
private boolean |
subset(ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts0,
ImmutableMap<SchemaVariable,InstantiationEntry<?>> insts1) |
public static final Feature INSTANCE
protected 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 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 duplicateFindTaclet(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 sequentpublic RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pos, Goal goal)
Feature
RuleApp
.computeCost
in interface Feature
ruleApp
- the RuleApppos
- position where app
is to be appliedgoal
- the goal on which app
is to be appliedRuleAppCost
object. TopRuleAppCost.INSTANCE
indicates that the rule shall not be applied at all (it is discarded by
the strategy).private boolean isInfFlowProof(Proof proof)
private java.util.ArrayList<SequentFormula> getRelatesTerms(Goal goal)