public final class GenericSortInstantiations
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
static GenericSortInstantiations |
EMPTY_INSTANTIATIONS |
Modifier and Type | Method and Description |
---|---|
java.lang.Boolean |
checkCondition(GenericSortCondition p_condition) |
java.lang.Boolean |
checkSorts(SchemaVariable sv,
InstantiationEntry<?> p_entry) |
static GenericSortInstantiations |
create(ImmutableList<GenericSort> p_sorts,
ImmutableList<GenericSortCondition> p_conditions,
Services services)
Create an object that holds instantiations of the generic sorts
"p_sorts" satisfying the conditions "p_conditions"
|
static GenericSortInstantiations |
create(java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> p_instantiations,
ImmutableList<GenericSortCondition> p_conditions,
Services services)
Create an object that solves the conditions given by the
instantiation iterator, i.e.
|
ImmutableMap<GenericSort,Sort> |
getAllInstantiations()
ONLY FOR JUNIT TESTS
|
Sort |
getInstantiation(GenericSort p_gs) |
Sort |
getRealSort(SchemaVariable p_sv,
TermServices services) |
Sort |
getRealSort(Sort p_s,
TermServices services) |
boolean |
isEmpty() |
boolean |
isInstantiated(GenericSort p_gs) |
ImmutableList<GenericSortCondition> |
toConditions()
Create a list of conditions establishing the instantiations
stored by this object (not saying anything about further
generic sorts)
|
java.lang.String |
toString() |
public static final GenericSortInstantiations EMPTY_INSTANTIATIONS
public static GenericSortInstantiations create(java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> p_instantiations, ImmutableList<GenericSortCondition> p_conditions, Services services)
p_instantiations
- list of SV instantiationsp_conditions
- additional conditions for sort instantiationsGenericSortException
- iff the conditions could not be
solvedpublic static GenericSortInstantiations create(ImmutableList<GenericSort> p_sorts, ImmutableList<GenericSortCondition> p_conditions, Services services)
p_sorts
- generic sorts to instantiatep_conditions
- conditions the instantiations have to
satisfyGenericSortException
- if no instantiations has been
foundpublic java.lang.Boolean checkSorts(SchemaVariable sv, InstantiationEntry<?> p_entry)
public java.lang.Boolean checkCondition(GenericSortCondition p_condition)
public boolean isInstantiated(GenericSort p_gs)
public Sort getInstantiation(GenericSort p_gs)
public boolean isEmpty()
public ImmutableList<GenericSortCondition> toConditions()
public Sort getRealSort(SchemaVariable p_sv, TermServices services)
services
- the Services classGenericSortException
- iff p_s is a generic sort which is
not yet instantiatedpublic Sort getRealSort(Sort p_s, TermServices services)
public java.lang.String toString()
toString
in class java.lang.Object
public ImmutableMap<GenericSort,Sort> getAllInstantiations()
Copyright © 2003-2019 The KeY-Project.