de.uka.ilkd.key.rule.inst

Class GenericSortCondition.GSCSupersort

java.lang.Object

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

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

Enclosing class:

GenericSortCondition

static class GenericSortCondition.GSCSupersort
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	GSCSupersort(GenericSort p_gs, Sort p_s)

Method Summary

Modifier and Type	Method and Description
boolean	check(Sort p_s, GenericSortInstantiations insts) checks if sort p_s is a supersort of the getSubsort
Sort	getSubsort()
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

GSCSupersort

protected GSCSupersort(GenericSort p_gs,
                       Sort p_s)

Method Detail

getSubsort

public Sort getSubsort()

check

public boolean check(Sort p_s,
                     GenericSortInstantiations insts)

checks if sort p_s is a supersort of the getSubsort

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