de.uka.ilkd.key.strategy

Class TacletAppContainer

java.lang.Object

de.uka.ilkd.key.strategy.RuleAppContainer

de.uka.ilkd.key.strategy.TacletAppContainer

All Implemented Interfaces:

java.lang.Comparable<RuleAppContainer>

Direct Known Subclasses:

FindTacletAppContainer, NoFindTacletAppContainer

public abstract class TacletAppContainer
extends RuleAppContainer

Instances of this class are immutable

Field Summary

Fields

Modifier and Type	Field and Description
private long	age

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	TacletAppContainer(RuleApp p_app, RuleAppCost p_cost, long p_age)

Method Summary

Modifier and Type	Method and Description
private ImmutableList<RuleAppContainer>	addContainer(NoPosTacletApp app, ImmutableList<RuleAppContainer> targetList, Goal p_goal) Create a container object for the given taclet app, provided that the app is sufficientlyComplete, and add the container to targetList
private ImmutableList<RuleAppContainer>	addContainer(NoPosTacletApp app, ImmutableList<RuleAppContainer> targetList, Goal p_goal, RuleAppCost cost) Create a container object for the given taclet app, provided that the app is sufficientlyComplete, and add the container to targetList
private ImmutableList<RuleAppContainer>	addInstances(NoPosTacletApp app, ImmutableList<RuleAppContainer> targetList, Goal p_goal) Add all instances of the given taclet app (that are possibly produced using method instantiateApp of the strategy) to targetList
TacletApp	completeRuleApp(Goal p_goal) Create a RuleApp that is suitable to be applied or null.
(package private) static RuleAppContainer	createAppContainers(NoPosTacletApp p_app, Goal p_goal) Create containers for NoFindTaclets.
(package private) static RuleAppContainer	createAppContainers(NoPosTacletApp p_app, PosInOccurrence p_pio, Goal p_goal) Create containers for FindTaclets or NoFindTaclets.
private TacletAppContainer	createContainer(Goal p_goal)
protected static TacletAppContainer	createContainer(NoPosTacletApp p_app, PosInOccurrence p_pio, Goal p_goal, boolean p_initial)
private static TacletAppContainer	createContainer(NoPosTacletApp p_app, PosInOccurrence p_pio, Goal p_goal, RuleAppCost p_cost, 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)
private ImmutableList<NoPosTacletApp>	incMatchIfFormulas(Goal p_goal)
private ImmutableList<RuleAppContainer>	instantiateApp(NoPosTacletApp app, ImmutableList<RuleAppContainer> targetList, Goal p_goal) Use the method instantiateApp of the strategy for choosing the values of schema variables that have not been instantiated so far
protected abstract boolean	isStillApplicable(Goal p_goal)
private static boolean	sufficientlyCompleteApp(NoPosTacletApp app)

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

age

private final long age

Constructor Detail

TacletAppContainer

protected TacletAppContainer(RuleApp p_app,
                             RuleAppCost p_cost,
                             long p_age)

Method Detail

getTacletApp

protected NoPosTacletApp getTacletApp()

getAge

public long getAge()

incMatchIfFormulas

private ImmutableList<NoPosTacletApp> incMatchIfFormulas(Goal p_goal)

createContainer

protected static TacletAppContainer createContainer(NoPosTacletApp p_app,
                                                    PosInOccurrence p_pio,
                                                    Goal p_goal,
                                                    boolean p_initial)

createContainer

private static TacletAppContainer createContainer(NoPosTacletApp p_app,
                                                  PosInOccurrence p_pio,
                                                  Goal p_goal,
                                                  RuleAppCost p_cost,
                                                  boolean p_initial)

createFurtherApps

public final ImmutableList<RuleAppContainer> createFurtherApps(Goal p_goal)

Create a list of new RuleAppContainers that are to be considered for application.

Specified by:

createFurtherApps in class RuleAppContainer

addInstances

private ImmutableList<RuleAppContainer> addInstances(NoPosTacletApp app,
                                                     ImmutableList<RuleAppContainer> targetList,
                                                     Goal p_goal)

Add all instances of the given taclet app (that are possibly produced using method instantiateApp of the strategy) to targetList

instantiateApp

private ImmutableList<RuleAppContainer> instantiateApp(NoPosTacletApp app,
                                                       ImmutableList<RuleAppContainer> targetList,
                                                       Goal p_goal)

Use the method instantiateApp of the strategy for choosing the values of schema variables that have not been instantiated so far

addContainer

private ImmutableList<RuleAppContainer> addContainer(NoPosTacletApp app,
                                                     ImmutableList<RuleAppContainer> targetList,
                                                     Goal p_goal)

Create a container object for the given taclet app, provided that the app is sufficientlyComplete, and add the container to targetList

addContainer

private ImmutableList<RuleAppContainer> addContainer(NoPosTacletApp app,
                                                     ImmutableList<RuleAppContainer> targetList,
                                                     Goal p_goal,
                                                     RuleAppCost cost)

Create a container object for the given taclet app, provided that the app is sufficientlyComplete, and add the container to targetList

sufficientlyCompleteApp

private static boolean sufficientlyCompleteApp(NoPosTacletApp app)

createContainer

private TacletAppContainer createContainer(Goal p_goal)

createAppContainers

static RuleAppContainer createAppContainers(NoPosTacletApp p_app,
                                            Goal p_goal)

Create containers for NoFindTaclets.

createInitialAppContainers

protected static ImmutableList<RuleAppContainer> createInitialAppContainers(ImmutableList<NoPosTacletApp> p_app,
                                                                            PosInOccurrence p_pio,
                                                                            Goal p_goal)

createAppContainers

static RuleAppContainer createAppContainers(NoPosTacletApp p_app,
                                            PosInOccurrence p_pio,
                                            Goal p_goal)

Create containers for FindTaclets or NoFindTaclets.

Parameters:

p_app - if p_pio is null, p_app has to be a TacletApp for a NoFindTaclet, otherwise for a FindTaclet.

Returns:

list of containers for currently applicable TacletApps, the cost may be an instance of TopRuleAppCost.

ifFormulasStillValid

protected boolean ifFormulasStillValid(Goal p_goal)

Returns:

true iff instantiation of the if-formulas of the stored taclet app exist and are valid are still valid, i.e. the referenced formulas still exist

isStillApplicable

protected abstract boolean isStillApplicable(Goal p_goal)

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)

getPosInOccurrence

protected PosInOccurrence getPosInOccurrence(Goal p_goal)

completeRuleApp

public TacletApp completeRuleApp(Goal p_goal)

Create a RuleApp that is suitable to be applied or null.

Specified by:

completeRuleApp in class RuleAppContainer