de.uka.ilkd.key.strategy.termfeature

Class EqTermFeature

java.lang.Object

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

de.uka.ilkd.key.strategy.termfeature.EqTermFeature

All Implemented Interfaces:

TermFeature

public class EqTermFeature
extends BinaryTermFeature

Term feature for testing equality of two terms. The feature returns zero iff it is invoked on a term that is equal to the current value of pattern. NB: it is not possible to use general ProjectionToTerm here, because the information necessary to evaluate a ProjectionToTerm is not available in a term feature

Field Summary

Fields

Modifier and Type	Field and Description
private TermBuffer	pattern

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	EqTermFeature(TermBuffer pattern)

Method Summary

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

pattern

private final TermBuffer pattern

Constructor Detail

EqTermFeature

private EqTermFeature(TermBuffer pattern)

Method Detail

create

public static TermFeature create(TermBuffer pattern)

filter

protected boolean filter(Term term,
                         Services services)

Specified by:

filter in class BinaryTermFeature