de.uka.ilkd.key.strategy.quantifierHeuristics

Class InstantiationCost

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.InstantiationCost

All Implemented Interfaces:

Feature

public class InstantiationCost
extends java.lang.Object
implements Feature

Feature that returns the number of branches after instantiated the quantifier formula.

Field Summary

Fields

Modifier and Type	Field and Description
private ProjectionToTerm	varInst

Constructor Summary

Constructors

Modifier	Constructor and Description
private	InstantiationCost(ProjectionToTerm var)

Method Summary

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

Methods inherited from class java.lang.Object

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

Field Detail

varInst

private final ProjectionToTerm varInst

Constructor Detail

InstantiationCost

private InstantiationCost(ProjectionToTerm var)

Method Detail

create

public static Feature create(ProjectionToTerm varInst)

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