de.uka.ilkd.key.strategy.quantifierHeuristics

Class InstantiationCostScalerFeature

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.InstantiationCostScalerFeature

All Implemented Interfaces:

Feature

public class InstantiationCostScalerFeature
extends java.lang.Object
implements Feature

Field Summary

Fields

Modifier and Type	Field and Description
private Feature	allowSplitting
private Feature	costFeature
private static RuleAppCost	MINUS_3000_COST
private static RuleAppCost	ONE_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	InstantiationCostScalerFeature(Feature costFeature, Feature allowSplitting)

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 costFeature, Feature allowSplitting)

Methods inherited from class java.lang.Object

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

Field Detail

costFeature

private final Feature costFeature

allowSplitting

private final Feature allowSplitting

ONE_COST

private static final RuleAppCost ONE_COST

MINUS_3000_COST

private static final RuleAppCost MINUS_3000_COST

Constructor Detail

InstantiationCostScalerFeature

private InstantiationCostScalerFeature(Feature costFeature,
                                       Feature allowSplitting)

Method Detail

create

public static Feature create(Feature costFeature,
                             Feature allowSplitting)

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