de.uka.ilkd.key.strategy.termfeature

Class TermLabelTermFeature

java.lang.Object

de.uka.ilkd.key.strategy.termfeature.BinaryTermFeature

de.uka.ilkd.key.strategy.termfeature.TermLabelTermFeature

All Implemented Interfaces:

TermFeature

public class TermLabelTermFeature
extends BinaryTermFeature

A termfeature that can be used to check whether a term has a specific label create(TermLabel) or any label {HAS_ANY_LABEL at all.

Field Summary

Fields

Modifier and Type	Field and Description
static TermFeature	HAS_ANY_LABEL
private TermLabel	label

Fields inherited from class de.uka.ilkd.key.strategy.termfeature.BinaryTermFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	TermLabelTermFeature(TermLabel label)

Method Summary

Modifier and Type	Method and Description
static TermFeature	create(TermLabel label)
protected boolean	filter(Term term, Services services)

Methods inherited from class de.uka.ilkd.key.strategy.termfeature.BinaryTermFeature

compute

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

HAS_ANY_LABEL

public static final TermFeature HAS_ANY_LABEL

label

private final TermLabel label

Constructor Detail

TermLabelTermFeature

private TermLabelTermFeature(TermLabel label)

Method Detail

create

public static TermFeature create(TermLabel label)

filter

protected boolean filter(Term term,
                         Services services)

Specified by:

filter in class BinaryTermFeature