de.uka.ilkd.key.strategy.termfeature

Class IsInductionVariable

java.lang.Object

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

de.uka.ilkd.key.strategy.termfeature.IsInductionVariable

All Implemented Interfaces:

TermFeature

public class IsInductionVariable
extends BinaryTermFeature

The comment below was the description used in the variable condition: In the taclet language the variable condition is called "\isInductVar". This variable condition checks if a logical variable is marked as an induction variable. A variable is marked as such if its name has the suffix is "Ind" or "IND" and the name has length>3.

Author:

gladisch

Field Summary

Fields

Modifier and Type	Field and Description
static TermFeature	INSTANCE

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	IsInductionVariable()

Method Summary

Modifier and Type	Method and Description
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

INSTANCE

public static final TermFeature INSTANCE

Constructor Detail

IsInductionVariable

private IsInductionVariable()

Method Detail

filter

protected boolean filter(Term term,
                         Services services)

Specified by:

filter in class BinaryTermFeature