de.uka.ilkd.key.strategy.feature

Class CheckApplyEqFeature

java.lang.Object

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

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

de.uka.ilkd.key.strategy.feature.CheckApplyEqFeature

All Implemented Interfaces:

Feature

public class CheckApplyEqFeature
extends BinaryTacletAppFeature

This feature checks that an equation is not applied to itself. This means that the focus of the rule application must not be one side of an equation that is the instantiation of the first if-formula. If the rule application is admissible, zero is returned.

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	CheckApplyEqFeature()

Method Summary

Modifier and Type	Method and Description
protected boolean	filter(TacletApp p_app, PosInOccurrence pos, Goal goal) Compute whether the result of the feature is zero (true) or infinity (false)
private boolean	isNotSelfApplication(PosInOccurrence pos, IfFormulaInstantiation ifInst)

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

INSTANCE

public static final Feature INSTANCE

Constructor Detail

CheckApplyEqFeature

private CheckApplyEqFeature()

Method Detail

filter

protected boolean filter(TacletApp p_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:

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

isNotSelfApplication

private boolean isNotSelfApplication(PosInOccurrence pos,
                                     IfFormulaInstantiation ifInst)