de.uka.ilkd.key.strategy.termfeature

Class OperatorTF

java.lang.Object

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

de.uka.ilkd.key.strategy.termfeature.OperatorTF

All Implemented Interfaces:

TermFeature

public class OperatorTF
extends BinaryTermFeature

Term feature for checking whether the top operator of a term is identical to a given one

Field Summary

Fields

Modifier and Type	Field and Description
private Operator	op

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	OperatorTF(Operator op)

Method Summary

Modifier and Type	Method and Description
static TermFeature	create(Operator op)
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

op

private final Operator op

Constructor Detail

OperatorTF

private OperatorTF(Operator op)

Method Detail

create

public static TermFeature create(Operator op)

filter

protected boolean filter(Term term,
                         Services services)

Specified by:

filter in class BinaryTermFeature