de.uka.ilkd.key.rule.conditions

Class TermLabelCondition

java.lang.Object

de.uka.ilkd.key.rule.VariableConditionAdapter

de.uka.ilkd.key.rule.conditions.TermLabelCondition

All Implemented Interfaces:

VariableCondition

public class TermLabelCondition
extends VariableConditionAdapter

This variable condition checks if an instantiation for term labels contains a specific term label.

Author:

Michael Kirsten

Field Summary

Fields

Modifier and Type	Field and Description
private TermLabelSV	l
private Name	ln
private boolean	negated

Constructor Summary

Constructors

Constructor and Description
TermLabelCondition(TermLabelSV l, java.lang.String t, boolean negated)

Method Summary

Modifier and Type	Method and Description
boolean	check(SchemaVariable var, SVSubstitute instCandidate, SVInstantiations instMap, Services services) checks if the condition for a correct instantiation is fulfilled
(package private) static boolean	hasLabel(ImmutableArray<?> labels, Name name) Checks if an array of label contains the label specified in this condition
java.lang.String	toString()

Methods inherited from class de.uka.ilkd.key.rule.VariableConditionAdapter

check

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

l

private final TermLabelSV l

ln

private final Name ln

negated

private final boolean negated

Constructor Detail

TermLabelCondition

public TermLabelCondition(TermLabelSV l,
                          java.lang.String t,
                          boolean negated)

Method Detail

check

public boolean check(SchemaVariable var,
                     SVSubstitute instCandidate,
                     SVInstantiations instMap,
                     Services services)

Description copied from class: VariableConditionAdapter

checks if the condition for a correct instantiation is fulfilled

Specified by:

check in class VariableConditionAdapter

Parameters:

var - the template Variable to be instantiated

instMap - the MatchCondition with the current matching state and in particular the SVInstantiations that are already known to be needed

services - the program information object

Returns:

true iff condition is fulfilled

hasLabel

static boolean hasLabel(ImmutableArray<?> labels,
                        Name name)

Checks if an array of label contains the label specified in this condition

Parameters:

labels - array of labels in the term to be matched

name - name of the label specified in this condition

Returns:

true if label matches, false if not

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object