de.uka.ilkd.key.strategy

Class RuleAppContainer

java.lang.Object

de.uka.ilkd.key.strategy.RuleAppContainer

All Implemented Interfaces:

java.lang.Comparable<RuleAppContainer>

Direct Known Subclasses:

BuiltInRuleAppContainer, TacletAppContainer

public abstract class RuleAppContainer
extends java.lang.Object
implements java.lang.Comparable<RuleAppContainer>

Container for RuleApp instances with cost as determined by a given Strategy. Instances of this class are immutable.

Field Summary

Fields

Modifier and Type	Field and Description
private RuleAppCost	cost The costs of the stored rule app
private RuleApp	ruleApp The stored rule app

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	RuleAppContainer(RuleApp p_app, RuleAppCost p_cost)

Method Summary

Modifier and Type	Method and Description
int	compareTo(RuleAppContainer o)
abstract RuleApp	completeRuleApp(Goal p_goal) Create a RuleApp that is suitable to be applied or null.
static RuleAppContainer	createAppContainer(RuleApp p_app, PosInOccurrence p_pio, Goal p_goal) Create container for a RuleApp.
static ImmutableList<RuleAppContainer>	createAppContainers(ImmutableList<? extends RuleApp> rules, PosInOccurrence pos, Goal goal) Create containers for RuleApps.
abstract ImmutableList<RuleAppContainer>	createFurtherApps(Goal p_goal) Create a list of new RuleAppContainers that are to be considered for application.
RuleAppCost	getCost()
protected RuleApp	getRuleApp()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

ruleApp

private final RuleApp ruleApp

The stored rule app

cost

private final RuleAppCost cost

The costs of the stored rule app

Constructor Detail

RuleAppContainer

protected RuleAppContainer(RuleApp p_app,
                           RuleAppCost p_cost)

Method Detail

compareTo

public final int compareTo(RuleAppContainer o)

Specified by:

compareTo in interface java.lang.Comparable<RuleAppContainer>

createFurtherApps

public abstract ImmutableList<RuleAppContainer> createFurtherApps(Goal p_goal)

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

completeRuleApp

public abstract RuleApp completeRuleApp(Goal p_goal)

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

getRuleApp

protected final RuleApp getRuleApp()

getCost

public final RuleAppCost getCost()

createAppContainer

public static RuleAppContainer createAppContainer(RuleApp p_app,
                                                  PosInOccurrence p_pio,
                                                  Goal p_goal)

Create container for a RuleApp.

Returns:

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

createAppContainers

public static ImmutableList<RuleAppContainer> createAppContainers(ImmutableList<? extends RuleApp> rules,
                                                                  PosInOccurrence pos,
                                                                  Goal goal)

Create containers for RuleApps.

Returns:

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