de.uka.ilkd.key.strategy.feature

Class FindRightishFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.FindRightishFeature

All Implemented Interfaces:

Feature

public class FindRightishFeature
extends java.lang.Object
implements Feature

Walking from the root of a formula down to the focus of a rule application, count how often we choose the left branch (subterm) and how the right branches. This is used to identify the upper/righter/bigger summands in a polynomial that is arranged in a left-associated way.

Field Summary

Fields

Modifier and Type	Field and Description
private Operator	add
private static RuleAppCost	one

Constructor Summary

Constructors

Modifier	Constructor and Description
private	FindRightishFeature(IntegerLDT numbers)

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(IntegerLDT numbers)

Methods inherited from class java.lang.Object

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

Field Detail

add

private final Operator add

one

private static final RuleAppCost one

Constructor Detail

FindRightishFeature

private FindRightishFeature(IntegerLDT numbers)

Method Detail

create

public static Feature create(IntegerLDT numbers)

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