de.uka.ilkd.key.rule.inst

Class GenericSortCondition.GSCForceInstantiation

java.lang.Object

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

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

Enclosing class:

GenericSortCondition

static class GenericSortCondition.GSCForceInstantiation
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) boolean	maximum

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	GSCForceInstantiation(GenericSort p_gs, boolean p_maximum)

Method Summary

Modifier and Type	Method and Description
boolean	check(Sort p_s, GenericSortInstantiations insts) checks if @link GenericSortcondition#getgenericSort() has been already instantiated by some sort (maximum, minimum is currently not checked)
boolean	getMaximum()
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

maximum

boolean maximum

Constructor Detail

GSCForceInstantiation

protected GSCForceInstantiation(GenericSort p_gs,
                                boolean p_maximum)

Method Detail

getMaximum

public boolean getMaximum()

check

public boolean check(Sort p_s,
                     GenericSortInstantiations insts)

checks if @link GenericSortcondition#getgenericSort() has been already instantiated by some sort (maximum, minimum is currently not checked)

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