public abstract class TacletAppContainer extends RuleAppContainer
Modifier | Constructor and Description |
---|---|
protected |
TacletAppContainer(RuleApp p_app,
RuleAppCost p_cost,
long p_age) |
Modifier and Type | Method and Description |
---|---|
TacletApp |
completeRuleApp(Goal p_goal)
Create a
RuleApp that is suitable to be applied
or null . |
protected static TacletAppContainer |
createContainer(NoPosTacletApp p_app,
PosInOccurrence p_pio,
Goal p_goal,
boolean p_initial) |
ImmutableList<RuleAppContainer> |
createFurtherApps(Goal p_goal)
Create a list of new RuleAppContainers that are to be
considered for application.
|
protected static ImmutableList<RuleAppContainer> |
createInitialAppContainers(ImmutableList<NoPosTacletApp> p_app,
PosInOccurrence p_pio,
Goal p_goal) |
long |
getAge() |
protected PosInOccurrence |
getPosInOccurrence(Goal p_goal) |
protected NoPosTacletApp |
getTacletApp() |
protected boolean |
ifFormulasStillValid(Goal p_goal) |
protected abstract boolean |
isStillApplicable(Goal p_goal) |
compareTo, createAppContainer, createAppContainers, getCost, getRuleApp
protected TacletAppContainer(RuleApp p_app, RuleAppCost p_cost, long p_age)
protected NoPosTacletApp getTacletApp()
public long getAge()
protected static TacletAppContainer createContainer(NoPosTacletApp p_app, PosInOccurrence p_pio, Goal p_goal, boolean p_initial)
public final ImmutableList<RuleAppContainer> createFurtherApps(Goal p_goal)
createFurtherApps
in class RuleAppContainer
protected static ImmutableList<RuleAppContainer> createInitialAppContainers(ImmutableList<NoPosTacletApp> p_app, PosInOccurrence p_pio, Goal p_goal)
protected boolean ifFormulasStillValid(Goal p_goal)
protected abstract boolean isStillApplicable(Goal p_goal)
protected PosInOccurrence getPosInOccurrence(Goal p_goal)
public TacletApp completeRuleApp(Goal p_goal)
RuleApp
that is suitable to be applied
or null
.completeRuleApp
in class RuleAppContainer
Copyright © 2003-2019 The KeY-Project.