de.uka.ilkd.key.strategy.feature

Class SimplifyBetaCandidateFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.AbstractBetaFeature

de.uka.ilkd.key.strategy.feature.SimplifyBetaCandidateFeature

All Implemented Interfaces:

Feature

public class SimplifyBetaCandidateFeature
extends AbstractBetaFeature

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

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.strategy.feature.AbstractBetaFeature

AbstractBetaFeature.TermInfo

Field Summary

Fields

Modifier and Type	Field and Description
static Feature	INSTANCE

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SimplifyBetaCandidateFeature()

Method Summary

Modifier and Type	Method and Description
protected RuleAppCost	doComputation(PosInOccurrence pos, Term findTerm, ServiceCaches caches)

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

alwaysReplace, computeCost, containsNegAtom, containsQuantifier, hasPurePosPath, isBetaCandidate, maxDPath, maxPosPath

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

SimplifyBetaCandidateFeature

private SimplifyBetaCandidateFeature()

Method Detail

doComputation

protected RuleAppCost doComputation(PosInOccurrence pos,
                                    Term findTerm,
                                    ServiceCaches caches)

Specified by:

doComputation in class AbstractBetaFeature