de.uka.ilkd.key.strategy.feature.instantiator

Class OneOfCP

java.lang.Object

de.uka.ilkd.key.strategy.feature.instantiator.OneOfCP

All Implemented Interfaces:

Feature

public class OneOfCP
extends java.lang.Object
implements Feature

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	OneOfCP.CP

Field Summary

Fields

Modifier and Type	Field and Description
private ChoicePoint	cp
private Feature[]	features
private BackTrackingManager	manager
private int	theChosenOne

Constructor Summary

Constructors

Modifier	Constructor and Description
private	OneOfCP(BackTrackingManager manager, Feature[] features)

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pos, Goal goal) Evaluate the cost of a RuleApp.
static Feature	create(Feature[] features, BackTrackingManager manager)

Methods inherited from class java.lang.Object

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

Field Detail

manager

private final BackTrackingManager manager

features

private final Feature[] features

theChosenOne

private int theChosenOne

cp

private final ChoicePoint cp

Constructor Detail

OneOfCP

private OneOfCP(BackTrackingManager manager,
                Feature[] features)

Method Detail

create

public static Feature create(Feature[] features,
                             BackTrackingManager manager)

computeCost

public RuleAppCost computeCost(RuleApp app,
                               PosInOccurrence pos,
                               Goal goal)

Description copied from interface: Feature

Evaluate the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Parameters:

app - the RuleApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

the cost of the rule application expressed as a RuleAppCost object. TopRuleAppCost.INSTANCE indicates that the rule shall not be applied at all (it is discarded by the strategy).