de.uka.ilkd.key.strategy.feature

Class TopLevelFindFeature

java.lang.Object

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

de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

de.uka.ilkd.key.strategy.feature.TopLevelFindFeature

All Implemented Interfaces:

Feature

Direct Known Subclasses:

TopLevelFindFeature.TopLevelWithoutUpdate, TopLevelFindFeature.TopLevelWithUpdate

public abstract class TopLevelFindFeature
extends BinaryTacletAppFeature

Feature for investigating whether the focus of a rule application is a top-level formula, a top-level formula of the antecedent or a top-level formula of the succedent

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	TopLevelFindFeature.TopLevelWithoutUpdate
private static class	TopLevelFindFeature.TopLevelWithUpdate

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	ANTEC
static Feature	ANTEC_OR_SUCC
static Feature	ANTEC_OR_SUCC_WITH_UPDATE
static Feature	ANTEC_WITH_UPDATE
static Feature	SUCC
static Feature	SUCC_WITH_UPDATE

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Constructor and Description
TopLevelFindFeature()

Method Summary

Modifier and Type	Method and Description
protected abstract boolean	checkPosition(PosInOccurrence pos)
protected boolean	filter(TacletApp app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)

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

filter

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

ANTEC_OR_SUCC

public static final Feature ANTEC_OR_SUCC

ANTEC

public static final Feature ANTEC

SUCC

public static final Feature SUCC

ANTEC_OR_SUCC_WITH_UPDATE

public static final Feature ANTEC_OR_SUCC_WITH_UPDATE

ANTEC_WITH_UPDATE

public static final Feature ANTEC_WITH_UPDATE

SUCC_WITH_UPDATE

public static final Feature SUCC_WITH_UPDATE

Constructor Detail

TopLevelFindFeature

public TopLevelFindFeature()

Method Detail

filter

protected boolean filter(TacletApp app,
                         PosInOccurrence pos,
                         Goal goal)

Description copied from class: BinaryTacletAppFeature

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

Specified by:

filter in class BinaryTacletAppFeature

Parameters:

app - the TacletApp

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.

checkPosition

protected abstract boolean checkPosition(PosInOccurrence pos)