de.uka.ilkd.key.strategy

Class BuiltInRuleAppContainer

java.lang.Object

de.uka.ilkd.key.strategy.RuleAppContainer

de.uka.ilkd.key.strategy.BuiltInRuleAppContainer

All Implemented Interfaces:

java.lang.Comparable<RuleAppContainer>

public class BuiltInRuleAppContainer
extends RuleAppContainer

Instances of this class are immutable

Field Summary

Fields

Modifier and Type	Field and Description
private PosInOccurrence	applicationPosition
private IBuiltInRuleApp	bir
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

Modifier	Constructor and Description
private	BuiltInRuleAppContainer(IBuiltInRuleApp bir, PosInOccurrence pio, RuleAppCost cost, Goal goal)

Method Summary

Modifier and Type	Method and Description
RuleApp	completeRuleApp(Goal goal) Create a RuleApp that is suitable to be applied or null.
(package private) static RuleAppContainer	createAppContainer(IBuiltInRuleApp bir, PosInOccurrence pio, Goal goal) Create container for RuleApp.
ImmutableList<RuleAppContainer>	createFurtherApps(Goal goal) Create a list of new RuleAppContainers that are to be considered for application.
(package private) static ImmutableList<RuleAppContainer>	createInitialAppContainers(ImmutableList<IBuiltInRuleApp> birs, PosInOccurrence pio, Goal goal) Create container for RuleApp.
private PosInOccurrence	getPosInOccurrence(Goal p_goal) Copied from FindTaclet.
private boolean	isStillApplicable(Goal goal)

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

bir

private final IBuiltInRuleApp bir

Constructor Detail

BuiltInRuleAppContainer

private BuiltInRuleAppContainer(IBuiltInRuleApp bir,
                                PosInOccurrence pio,
                                RuleAppCost cost,
                                Goal goal)

Method Detail

isStillApplicable

private boolean isStillApplicable(Goal goal)

Returns:

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

getPosInOccurrence

private PosInOccurrence getPosInOccurrence(Goal p_goal)

Copied from FindTaclet.

createAppContainer

static RuleAppContainer createAppContainer(IBuiltInRuleApp bir,
                                           PosInOccurrence pio,
                                           Goal goal)

Create container for RuleApp.

Returns:

container for the currently applicable BuiltInRuleApp, the cost may be an instance of TopRuleAppCost.

createInitialAppContainers

static ImmutableList<RuleAppContainer> createInitialAppContainers(ImmutableList<IBuiltInRuleApp> birs,
                                                                  PosInOccurrence pio,
                                                                  Goal goal)

Create container for RuleApp.

Returns:

container for the currently applicable BuiltInRuleApp, the cost may be an instance of TopRuleAppCost.

createFurtherApps

public ImmutableList<RuleAppContainer> createFurtherApps(Goal goal)

Description copied from class: RuleAppContainer

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

Specified by:

createFurtherApps in class RuleAppContainer

completeRuleApp

public RuleApp completeRuleApp(Goal goal)

Description copied from class: RuleAppContainer

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

Specified by:

completeRuleApp in class RuleAppContainer