de.uka.ilkd.key.strategy

Class FindTacletAppContainer

java.lang.Object

de.uka.ilkd.key.strategy.RuleAppContainer

de.uka.ilkd.key.strategy.TacletAppContainer

de.uka.ilkd.key.strategy.FindTacletAppContainer

All Implemented Interfaces:

java.lang.Comparable<RuleAppContainer>

public class FindTacletAppContainer
extends TacletAppContainer

Instances of this class are immutable

Field Summary

Fields

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 Summary

Constructors

Constructor and Description
FindTacletAppContainer(NoPosTacletApp p_app, PosInOccurrence p_pio, RuleAppCost p_cost, Goal p_goal, long p_age)

Method Summary

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()

Methods inherited from class de.uka.ilkd.key.strategy.TacletAppContainer

completeRuleApp, createAppContainers, createAppContainers, createContainer, createFurtherApps, createInitialAppContainers, getAge, getTacletApp, ifFormulasStillValid

Methods inherited from class de.uka.ilkd.key.strategy.RuleAppContainer

compareTo, createAppContainer, createAppContainers, getCost, getRuleApp

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

positionTag

private final 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

applicationPosition

private final PosInOccurrence applicationPosition

Constructor Detail

FindTacletAppContainer

FindTacletAppContainer(NoPosTacletApp p_app,
                       PosInOccurrence p_pio,
                       RuleAppCost p_cost,
                       Goal p_goal,
                       long p_age)

Method Detail

isStillApplicable

protected boolean isStillApplicable(Goal p_goal)

Specified by:

isStillApplicable in class TacletAppContainer

Returns:

true iff the stored rule app is applicable for the given sequent, i.e. if the find-position does still exist (if-formulas are not considered)

subformulaOrPreceedingUpdateHasChanged

private boolean subformulaOrPreceedingUpdateHasChanged(Goal p_goal)

Returns:

true iff a subformula that contains the find position stored by this object has been altered since the creation of this object or if a preceding update has changed

independentSubformulas

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. The modification affects a formula 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 application

Returns:

true iff applicationPosition 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 update

updateContextIsRecorded

private boolean updateContextIsRecorded()

Returns:

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 changes

getPosInOccurrence

protected PosInOccurrence getPosInOccurrence(Goal p_goal)

Overrides:

getPosInOccurrence in class TacletAppContainer

Returns:

non-null for FindTaclets