de.uka.ilkd.key.strategy.termfeature

Class SortExtendsTransTermFeature

java.lang.Object

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

de.uka.ilkd.key.strategy.termfeature.SortExtendsTransTermFeature

All Implemented Interfaces:

TermFeature

public class SortExtendsTransTermFeature
extends BinaryTermFeature

Term feature for testing whether the sort of a term is a subsort of a given sort (or exactly the given sort).

Field Summary

Fields

Modifier and Type	Field and Description
private Sort	sort

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SortExtendsTransTermFeature(Sort sort)

Method Summary

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

sort

private final Sort sort

Constructor Detail

SortExtendsTransTermFeature

private SortExtendsTransTermFeature(Sort sort)

Method Detail

create

public static TermFeature create(Sort sort)

filter

protected boolean filter(Term term,
                         Services services)

Specified by:

filter in class BinaryTermFeature