| java.lang.Object de.uka.ilkd.key.strategy.RuleAppContainer de.uka.ilkd.key.strategy.TacletAppContainer
All known Subclasses: de.uka.ilkd.key.strategy.NoFindTacletAppContainer, de.uka.ilkd.key.strategy.FindTacletAppContainer,
TacletAppContainer | abstract public class TacletAppContainer extends RuleAppContainer (Code) | | Instances of this class are immutable
|
Inner Class :final protected static class IfInstCache | |
Field Summary | |
final protected static IfInstCache | ifInstCache |
Method Summary | |
public RuleApp | completeRuleApp(Goal p_goal, Strategy strategy) Create a RuleApp that is suitable to be applied
or null . | static ListOfRuleAppContainer | createAppContainers(NoPosTacletApp p_app, Goal p_goal, Strategy p_strategy) Create containers for NoFindTaclets. | static ListOfRuleAppContainer | createAppContainers(NoPosTacletApp p_app, PosInOccurrence p_pio, Goal p_goal, Strategy p_strategy) Create containers for FindTaclets or NoFindTaclets.
Parameters: p_app - if p_pio is null, p_app has to bea TacletApp for a NoFindTaclet ,otherwise for a FindTaclet . | protected static TacletAppContainer | createContainer(RuleApp p_app, PosInOccurrence p_pio, Goal p_goal, Strategy p_strategy, boolean p_initial) | public ListOfRuleAppContainer | createFurtherApps(Goal p_goal, Strategy p_strategy) Create a list of new RuleAppContainers that are to be
considered for application. | public long | getAge() | protected PosInOccurrence | getPosInOccurrence(Goal p_goal) | protected NoPosTacletApp | getTacletApp() | protected boolean | ifFormulasStillValid(Goal p_goal) true iff instantiation of the if-formulas of the stored tacletapp exist and are valid are still valid, i.e. | abstract protected boolean | isStillApplicable(Goal p_goal) true iff the stored rule app is applicable for the given sequent,i.e. |
ifInstCache | final protected static IfInstCache ifInstCache(Code) | | |
completeRuleApp | public RuleApp completeRuleApp(Goal p_goal, Strategy strategy)(Code) | | Create a RuleApp that is suitable to be applied
or null .
|
createAppContainers | static ListOfRuleAppContainer createAppContainers(NoPosTacletApp p_app, Goal p_goal, Strategy p_strategy)(Code) | | Create containers for NoFindTaclets.
|
createAppContainers | static ListOfRuleAppContainer createAppContainers(NoPosTacletApp p_app, PosInOccurrence p_pio, Goal p_goal, Strategy p_strategy)(Code) | | Create containers for FindTaclets or NoFindTaclets.
Parameters: p_app - if p_pio is null, p_app has to bea TacletApp for a NoFindTaclet ,otherwise for a FindTaclet . list of containers for currently applicable TacletApps, the costmay be an instance of TopRuleAppCost . |
createFurtherApps | public ListOfRuleAppContainer createFurtherApps(Goal p_goal, Strategy p_strategy)(Code) | | Create a list of new RuleAppContainers that are to be
considered for application.
|
getAge | public long getAge()(Code) | | |
ifFormulasStillValid | protected boolean ifFormulasStillValid(Goal p_goal)(Code) | | true iff instantiation of the if-formulas of the stored tacletapp exist and are valid are still valid, i.e. the referenced formulasstill exist |
isStillApplicable | abstract protected boolean isStillApplicable(Goal p_goal)(Code) | | true iff the stored rule app is applicable for the given sequent,i.e. if the find-position does still exist (if-formulas are notconsidered) |
|
|