public class SVInstantiations
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
SVInstantiations.UpdateLabelPair |
Modifier and Type | Field and Description |
---|---|
static SVInstantiations |
EMPTY_SVINSTANTIATIONS
the empty instantiation
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
add(GenericSortCondition p_c,
Services services)
Add the given additional condition for the generic sort instantiations
|
SVInstantiations |
add(ModalOperatorSV sv,
Operator op,
Services services) |
SVInstantiations |
add(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
Services services)
adds the given pair to the instantiations for the context.If the context
has been instantiated already, the new pair is taken without a warning.
|
SVInstantiations |
add(SchemaVariable sv,
ImmutableArray<TermLabel> labels,
Services services) |
SVInstantiations |
add(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
add(SchemaVariable sv,
ProgramElement pe,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
add(SchemaVariable sv,
ProgramList pes,
Services services) |
SVInstantiations |
add(SchemaVariable sv,
Term subst,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
addInteresting(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services) |
SVInstantiations |
addInteresting(SchemaVariable sv,
Name name,
Services services) |
SVInstantiations |
addInteresting(SchemaVariable sv,
ProgramElement pe,
Services services) |
SVInstantiations |
addInteresting(SchemaVariable sv,
Term subst,
Services services) |
SVInstantiations |
addInterestingList(SchemaVariable sv,
java.lang.Object[] list,
Services services) |
SVInstantiations |
addList(SchemaVariable sv,
java.lang.Object[] list,
Services services) |
SVInstantiations |
addUpdate(Term update,
ImmutableArray<TermLabel> updateApplicationlabels)
adds an update to the update context
|
SVInstantiations |
addUpdateList(ImmutableList<SVInstantiations.UpdateLabelPair> updates) |
SVInstantiations |
clearUpdateContext() |
boolean |
equals(java.lang.Object obj)
returns true if the given object and this one have the same mappings
|
ContextInstantiationEntry |
getContextInstantiation()
returns the instantiation entry for the context "schema variable" or null
if non such exists
|
ExecutionContext |
getExecutionContext() |
ImmutableList<GenericSortCondition> |
getGenericSortConditions() |
GenericSortInstantiations |
getGenericSortInstantiations() |
java.lang.Object |
getInstantiation(SchemaVariable sv)
returns the instantiation of the given SchemaVariable
|
InstantiationEntry<?> |
getInstantiationEntry(SchemaVariable sv)
returns the instantiation of the given SchemaVariable
|
Term |
getTermInstantiation(SchemaVariable sv,
ExecutionContext ec,
Services services)
returns the instantiation of the given SchemaVariable as Term.
|
ImmutableList<SVInstantiations.UpdateLabelPair> |
getUpdateContext()
returns the update context
|
int |
hashCode() |
ImmutableMap<SchemaVariable,InstantiationEntry<?>> |
interesting() |
boolean |
isEmpty()
returns true iff no instantiation of SchemaVariables are known
|
boolean |
isInstantiated(SchemaVariable sv)
returns true iff the sv has been instantiated already
|
ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>> |
lookupEntryForSV(Name name) |
java.lang.Object |
lookupValue(Name name) |
SchemaVariable |
lookupVar(Name name) |
SVInstantiations |
makeInteresting(SchemaVariable sv,
Services services)
adds the schemvariable to the set of interesting ones
|
java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> |
pairIterator()
returns iterator of the mapped pair (SchemaVariables, InstantiationEntry>)
|
SVInstantiations |
replace(PosInProgram prefix,
PosInProgram postfix,
ExecutionContext activeStatementContext,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
replace(SchemaVariable sv,
ImmutableArray<ProgramElement> pes,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
replace(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
replace(SchemaVariable sv,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
replace(SchemaVariable sv,
Term term,
Services services)
replaces the given pair in the instantiations.
|
int |
size()
returns the number of SchemaVariables of which an instantiation is known
|
java.util.Iterator<SchemaVariable> |
svIterator()
returns iterator of the SchemaVariables that have an instantiation
|
java.lang.String |
toString() |
SVInstantiations |
union(SVInstantiations other,
Services services) |
public static final SVInstantiations EMPTY_SVINSTANTIATIONS
public GenericSortInstantiations getGenericSortInstantiations()
public ImmutableList<GenericSortCondition> getGenericSortConditions()
public SVInstantiations add(SchemaVariable sv, Term subst, Services services)
sv
- the SchemaVariable to be instantiatedsubst
- the Term the SchemaVariable is instantiated withpublic SVInstantiations add(ModalOperatorSV sv, Operator op, Services services)
public SVInstantiations addInteresting(SchemaVariable sv, Term subst, Services services)
public SVInstantiations add(SchemaVariable sv, ProgramList pes, Services services)
public SVInstantiations add(SchemaVariable sv, ImmutableArray<TermLabel> labels, Services services)
public SVInstantiations addList(SchemaVariable sv, java.lang.Object[] list, Services services)
public SVInstantiations add(SchemaVariable sv, ProgramElement pe, Services services)
sv
- the SchemaVariable to be instantiatedpe
- the ProgramElement the SchemaVariable is instantiated withpublic SVInstantiations addInteresting(SchemaVariable sv, ProgramElement pe, Services services)
public SVInstantiations addInterestingList(SchemaVariable sv, java.lang.Object[] list, Services services)
public SVInstantiations add(PosInProgram prefix, PosInProgram postfix, ExecutionContext activeStatementContext, ProgramElement pe, Services services)
prefix
- the PosInProgram describing the prefixpostfix
- the PosInProgram describing the postfixactiveStatementContext
- the ExecutionContext of the first active statementpe
- the ProgramElement the context positions are related topublic SVInstantiations add(SchemaVariable sv, InstantiationEntry<?> entry, Services services)
sv
- the SchemaVariable to be instantiatedentry
- the InstantiationEntry>public SVInstantiations addInteresting(SchemaVariable sv, InstantiationEntry<?> entry, Services services)
public SVInstantiations addInteresting(SchemaVariable sv, Name name, Services services)
public SVInstantiations replace(SchemaVariable sv, InstantiationEntry<?> entry, Services services)
sv
- the SchemaVariable to be instantiatedentry
- the InstantiationEntry> the SchemaVariable is instantiated withpublic SVInstantiations makeInteresting(SchemaVariable sv, Services services)
IllegalInstantiationException,
- if sv has not yet been instantiatedpublic SVInstantiations replace(SchemaVariable sv, Term term, Services services)
sv
- the SchemaVariable to be instantiatedterm
- the Term the SchemaVariable is instantiated withpublic SVInstantiations replace(SchemaVariable sv, ProgramElement pe, Services services)
sv
- the SchemaVariable to be instantiatedpe
- the ProgramElement the SchemaVariable is instantiated withpublic SVInstantiations replace(SchemaVariable sv, ImmutableArray<ProgramElement> pes, Services services)
sv
- the SchemaVariable to be instantiatedpes
- the ArrayOfpublic SVInstantiations replace(PosInProgram prefix, PosInProgram postfix, ExecutionContext activeStatementContext, ProgramElement pe, Services services)
prefix
- the PosInProgram describing the position of the first
statement after the prefixpostfix
- the PosInProgram describing the position of the statement just
before the postfixactiveStatementContext
- the ExecutionContext of the first active statementpe
- the ProgramElement the context positions are related topublic boolean isInstantiated(SchemaVariable sv)
public InstantiationEntry<?> getInstantiationEntry(SchemaVariable sv)
public java.lang.Object getInstantiation(SchemaVariable sv)
public Term getTermInstantiation(SchemaVariable sv, ExecutionContext ec, Services services)
public SVInstantiations addUpdate(Term update, ImmutableArray<TermLabel> updateApplicationlabels)
updateApplicationlabels
- the TermLabels attached to the application operator termpublic SVInstantiations addUpdateList(ImmutableList<SVInstantiations.UpdateLabelPair> updates)
public SVInstantiations clearUpdateContext()
public ContextInstantiationEntry getContextInstantiation()
public java.util.Iterator<SchemaVariable> svIterator()
public java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> pairIterator()
public int size()
public boolean isEmpty()
public ImmutableList<SVInstantiations.UpdateLabelPair> getUpdateContext()
public boolean equals(java.lang.Object obj)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public SVInstantiations union(SVInstantiations other, Services services)
public ImmutableMap<SchemaVariable,InstantiationEntry<?>> interesting()
public java.lang.String toString()
toString
in class java.lang.Object
public SVInstantiations add(GenericSortCondition p_c, Services services) throws SortException
SortException
public ExecutionContext getExecutionContext()
public ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>> lookupEntryForSV(Name name)
public SchemaVariable lookupVar(Name name)
public java.lang.Object lookupValue(Name name)
Copyright © 2003-2019 The KeY-Project.