de.uka.ilkd.key.strategy.feature

Class AllowedCutPositionFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.strategy.feature.AllowedCutPositionFeature

All Implemented Interfaces:

Feature

public class AllowedCutPositionFeature
extends BinaryFeature

Feature that returns zero iff the application focus of a rule is a potential cut position (taclet cut_direct). For positions that are below quantifiers, the feature generally returns zero.

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	INSTANCE

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	AllowedCutPositionFeature()

Method Summary

Modifier and Type	Method and Description
boolean	filter(RuleApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
private boolean	onlyBelowRightJunctors(PosInOccurrence pos)

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

computeCost

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

AllowedCutPositionFeature

private AllowedCutPositionFeature()

Method Detail

filter

public boolean filter(RuleApp app,
                      PosInOccurrence pos,
                      Goal goal)

Description copied from class: BinaryFeature

Compute whether the result of the feature is zero (true) or infinity (false)

Specified by:

filter in class BinaryFeature

Parameters:

app - the RuleApp

pos - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

true iff the the result of the feature is supposed to be zero.

onlyBelowRightJunctors

private boolean onlyBelowRightJunctors(PosInOccurrence pos)