de.uka.ilkd.key.strategy.termfeature

Class ContainsExecutableCodeTermFeature

java.lang.Object

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

de.uka.ilkd.key.strategy.termfeature.ContainsExecutableCodeTermFeature

All Implemented Interfaces:

TermFeature

public class ContainsExecutableCodeTermFeature
extends BinaryTermFeature

Returns zero iff a term contains a program or (optionally) a query expression

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	considerQueries
static TermFeature	PROGRAMS
static TermFeature	PROGRAMS_OR_QUERIES

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

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ContainsExecutableCodeTermFeature(boolean considerQueries)

Method Summary

Modifier and Type	Method and Description
private boolean	containsExec(Term t, Services services)
protected boolean	filter(Term t, 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

considerQueries

private final boolean considerQueries

PROGRAMS

public static final TermFeature PROGRAMS

PROGRAMS_OR_QUERIES

public static final TermFeature PROGRAMS_OR_QUERIES

Constructor Detail

ContainsExecutableCodeTermFeature

private ContainsExecutableCodeTermFeature(boolean considerQueries)

Method Detail

filter

protected boolean filter(Term t,
                         Services services)

Specified by:

filter in class BinaryTermFeature

containsExec

private boolean containsExec(Term t,
                             Services services)