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

Class ForEachCP

java.lang.Object

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

All Implemented Interfaces:

Feature

public class ForEachCP
extends java.lang.Object
implements Feature

Feature representing a ChoicePoint that iterates over the terms returned by a TermGenerator. The terms are stored in a TermBuffer one after the other and can subsequently be used to instantiate a rule application

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	ForEachCP.CP

Field Summary

Fields

Modifier and Type	Field and Description
private Feature	body
private TermGenerator	generator
private BackTrackingManager	manager
private TermBuffer	var

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ForEachCP(TermBuffer var, TermGenerator generator, Feature body, BackTrackingManager manager)

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(TermBuffer var, TermGenerator generator, Feature body, 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

var

private final TermBuffer var

generator

private final TermGenerator generator

body

private final Feature body

Constructor Detail

ForEachCP

private ForEachCP(TermBuffer var,
                  TermGenerator generator,
                  Feature body,
                  BackTrackingManager manager)

Method Detail

create

public static Feature create(TermBuffer var,
                             TermGenerator generator,
                             Feature body,
                             BackTrackingManager manager)

Parameters:

var - TermBuffer in which the terms are going to be stored

generator - the terms that are to be iterated over

body - a feature that is supposed to be evaluated repeatedly for the possible values of var

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).