de.uka.ilkd.key.rule.inst

Class GenericSortCondition.GSCIdentity

java.lang.Object

de.uka.ilkd.key.rule.inst.GenericSortCondition

de.uka.ilkd.key.rule.inst.GenericSortCondition.GSCIdentity

Enclosing class:

GenericSortCondition

static class GenericSortCondition.GSCIdentity
extends GenericSortCondition

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.inst.GenericSortCondition

GenericSortCondition.GSCForceInstantiation, GenericSortCondition.GSCIdentity, GenericSortCondition.GSCSupersort

Field Summary

Fields

Modifier and Type	Field and Description
(package private) Sort	s

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	GSCIdentity(GenericSort p_gs, Sort p_s)

Method Summary

Modifier and Type	Method and Description
boolean	check(Sort p_s, GenericSortInstantiations insts) tests if p_s is identical to @link GSCIdentity#getSort()
Sort	getSort()
java.lang.String	toString() toString

Methods inherited from class de.uka.ilkd.key.rule.inst.GenericSortCondition

createCondition, createCondition, createCondition, createForceInstantiationCondition, createIdentityCondition, createSupersortCondition, forceInstantiation, getGenericSort, subSortsAllowed

Methods inherited from class java.lang.Object

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

Field Detail

s

Sort s

Constructor Detail

GSCIdentity

protected GSCIdentity(GenericSort p_gs,
                      Sort p_s)

Method Detail

getSort

public Sort getSort()

check

public boolean check(Sort p_s,
                     GenericSortInstantiations insts)

tests if p_s is identical to @link GSCIdentity#getSort()

Specified by:

check in class GenericSortCondition

Parameters:

p_s - the Sort to check

insts - a map containing already found instantiations

Returns:

true if the given sort s satisfies this generic sort condition

toString

public java.lang.String toString()

toString

Overrides:

toString in class java.lang.Object