de.uka.ilkd.key.strategy.feature

Class CountBranchFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.CountBranchFeature

All Implemented Interfaces:

Feature

public class CountBranchFeature
extends java.lang.Object
implements Feature

Feature that returns the number of branches for a given taclet application Size of "assumes" sequents is currently not considered

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	INSTANCE

Constructor Summary

Constructors

Modifier	Constructor and Description
private	CountBranchFeature()

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp app, PosInOccurrence pos, Goal goal) Compute the cost of a RuleApp.

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static Feature INSTANCE

Constructor Detail

CountBranchFeature

private CountBranchFeature()

Method Detail

computeCost

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

Compute 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 app