public class BuiltInRuleAppContainer extends RuleAppContainer
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 |
Modifier | Constructor and Description |
---|---|
private |
BuiltInRuleAppContainer(IBuiltInRuleApp bir,
PosInOccurrence pio,
RuleAppCost cost,
Goal goal) |
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) |
compareTo, createAppContainer, createAppContainers, getCost, getRuleApp
private final FormulaTag positionTag
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 createdprivate final PosInOccurrence applicationPosition
private final IBuiltInRuleApp bir
private BuiltInRuleAppContainer(IBuiltInRuleApp bir, PosInOccurrence pio, RuleAppCost cost, Goal goal)
private boolean isStillApplicable(Goal goal)
private PosInOccurrence getPosInOccurrence(Goal p_goal)
static RuleAppContainer createAppContainer(IBuiltInRuleApp bir, PosInOccurrence pio, Goal goal)
TopRuleAppCost
.static ImmutableList<RuleAppContainer> createInitialAppContainers(ImmutableList<IBuiltInRuleApp> birs, PosInOccurrence pio, Goal goal)
TopRuleAppCost
.public ImmutableList<RuleAppContainer> createFurtherApps(Goal goal)
RuleAppContainer
createFurtherApps
in class RuleAppContainer
public RuleApp completeRuleApp(Goal goal)
RuleAppContainer
RuleApp
that is suitable to be applied
or null
.completeRuleApp
in class RuleAppContainer