de.uka.ilkd.key.strategy.feature

Class SimplifyReplaceKnownCandidateFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.AbstractPolarityFeature

de.uka.ilkd.key.strategy.feature.SimplifyReplaceKnownCandidateFeature

All Implemented Interfaces:

Feature

public class SimplifyReplaceKnownCandidateFeature
extends AbstractPolarityFeature
implements Feature

Binary feature that returns true iff the hyper-tableaux simplification method approves the given application (which is supposed to be the application of a replace-known rule). Used terminology is defined in Diss. by Martin Giese.

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	INSTANCE

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SimplifyReplaceKnownCandidateFeature()

Method Summary

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

Methods inherited from class de.uka.ilkd.key.strategy.feature.AbstractPolarityFeature

polarity

Methods inherited from class java.lang.Object

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

Field Detail

INSTANCE

public static final Feature INSTANCE

Constructor Detail

SimplifyReplaceKnownCandidateFeature

private SimplifyReplaceKnownCandidateFeature()

Method Detail

computeCost

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

Compute the cost of a RuleApp.

Specified by:

computeCost in interface Feature

Parameters:

ruleApp - 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

isAllowedPosition

private boolean isAllowedPosition(PosInOccurrence pos)