de.uka.ilkd.key.strategy.feature

Class ContainsQuantifierFeature

java.lang.Object

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

de.uka.ilkd.key.strategy.feature.ContainsQuantifierFeature

All Implemented Interfaces:

Feature

public class ContainsQuantifierFeature
extends AbstractBetaFeature

Binary feature that returns zero iff the focus of a rule contains a quantifier NB: this can nowadays be done more nicely using term features

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

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

ContainsQuantifierFeature

private ContainsQuantifierFeature()

Method Detail

doComputation

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

Specified by:

doComputation in class AbstractBetaFeature