public class FindTacletAppContainer extends TacletAppContainer
Modifier and Type | Field and Description |
---|---|
private PosInOccurrence |
applicationPosition |
private FormulaTag |
positionTag
The position of the rule app in two different representations:
positionTag denotes the concerned formula and survives
modifications of the sequent and of parts of the formula, and
applicationPosition is the original position for which the
rule app was created |
Constructor and Description |
---|
FindTacletAppContainer(NoPosTacletApp p_app,
PosInOccurrence p_pio,
RuleAppCost p_cost,
Goal p_goal,
long p_age) |
Modifier and Type | Method and Description |
---|---|
protected PosInOccurrence |
getPosInOccurrence(Goal p_goal) |
private boolean |
independentSubformulas(PosInOccurrence changePos,
SequentFormula newFormula)
checks if the modification path and the position where this taclet application
has been matched again denote independent subformulas.
|
protected boolean |
isStillApplicable(Goal p_goal) |
private boolean |
subformulaOrPreceedingUpdateHasChanged(Goal p_goal) |
private boolean |
updateContextIsRecorded() |
completeRuleApp, createAppContainers, createAppContainers, createContainer, createFurtherApps, createInitialAppContainers, getAge, getTacletApp, ifFormulasStillValid
compareTo, createAppContainer, createAppContainers, getCost, getRuleApp
private final FormulaTag positionTag
positionTag
denotes the concerned formula and survives
modifications of the sequent and of parts of the formula, and
applicationPosition
is the original position for which the
rule app was createdprivate final PosInOccurrence applicationPosition
FindTacletAppContainer(NoPosTacletApp p_app, PosInOccurrence p_pio, RuleAppCost p_cost, Goal p_goal, long p_age)
protected boolean isStillApplicable(Goal p_goal)
isStillApplicable
in class TacletAppContainer
private boolean subformulaOrPreceedingUpdateHasChanged(Goal p_goal)
private boolean independentSubformulas(PosInOccurrence changePos, SequentFormula newFormula)
F
if F
is a subformula of the modified one
or the modification took part inside an update which may occur in the update
prefix instantiation of the taclet applicationapplicationPosition
is in the scope of
the position p_pos
(the formulas are not compared, only the
positions within the formulas) and no indirect relationship exists which
is established by a modification that occurred inside an updateprivate boolean updateContextIsRecorded()
true
iff the update context (updates above the
application position) is relevant and stored for this taclet app.
In this case, the taclet app has to be discarded as soon as the
update context changesprotected PosInOccurrence getPosInOccurrence(Goal p_goal)
getPosInOccurrence
in class TacletAppContainer