public class SVInstantiations
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
SVInstantiations.UpdateLabelPair |
Modifier and Type | Field and Description |
---|---|
private static SchemaVariable |
CONTEXTSV
the context itself is not realised as a schemavariable, therefore we need
here a dummy SV for a more unified handling (key in map)
|
private static IllegalInstantiationException |
CONVERT_INSTANTIATION_EXCEPTION |
static SVInstantiations |
EMPTY_SVINSTANTIATIONS
the empty instantiation
|
private ImmutableList<GenericSortCondition> |
genericSortConditions
additional conditions for the generic sorts
|
private GenericSortInstantiations |
genericSortInstantiations
instantiations of generic sorts
|
private static SortException |
INCOMPATIBLE_INSTANTIATION_EXCEPTION |
private ImmutableMap<SchemaVariable,InstantiationEntry<?>> |
interesting
just a list of "interesting" instantiations: these instantiations are not
100% predetermined and worth saving in a proof
|
private ImmutableMap<SchemaVariable,InstantiationEntry<?>> |
map
the map with the instantiations to logic terms
|
private static SortException |
UNSOLVABLE_SORT_CONDITIONS_EXCEPTION |
private ImmutableList<SVInstantiations.UpdateLabelPair> |
updateContext
updates may be ignored when matching, therefore they need to be added
after the application around the added/replaced parts.
|
Modifier | Constructor and Description |
---|---|
private |
SVInstantiations()
creates a new SVInstantions object with an empty map
|
private |
SVInstantiations(ImmutableMap<SchemaVariable,InstantiationEntry<?>> map,
ImmutableMap<SchemaVariable,InstantiationEntry<?>> interesting,
ImmutableList<SVInstantiations.UpdateLabelPair> updateContext,
GenericSortInstantiations genericSortInstantiations,
ImmutableList<GenericSortCondition> genericSortConditions) |
private |
SVInstantiations(ImmutableMap<SchemaVariable,InstantiationEntry<?>> map,
ImmutableMap<SchemaVariable,InstantiationEntry<?>> interesting,
ImmutableList<SVInstantiations.UpdateLabelPair> updateContext,
ImmutableList<GenericSortCondition> genericSortConditions)
creates a new SVInstantions object using the given map
|
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) |
private SVInstantiations |
checkCondition(GenericSortCondition p_c,
boolean p_forceRebuild,
Services services) |
private SVInstantiations |
checkSorts(SchemaVariable p_sv,
InstantiationEntry<?> p_entry,
boolean p_forceRebuild,
Services services) |
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
|
private SVInstantiations |
rebuildSorts(Services services) |
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
private static final SchemaVariable CONTEXTSV
private final ImmutableMap<SchemaVariable,InstantiationEntry<?>> map
private final ImmutableMap<SchemaVariable,InstantiationEntry<?>> interesting
private final ImmutableList<SVInstantiations.UpdateLabelPair> updateContext
private GenericSortInstantiations genericSortInstantiations
private final ImmutableList<GenericSortCondition> genericSortConditions
private static final SortException INCOMPATIBLE_INSTANTIATION_EXCEPTION
private static final IllegalInstantiationException CONVERT_INSTANTIATION_EXCEPTION
private static final SortException UNSOLVABLE_SORT_CONDITIONS_EXCEPTION
private SVInstantiations()
private SVInstantiations(ImmutableMap<SchemaVariable,InstantiationEntry<?>> map, ImmutableMap<SchemaVariable,InstantiationEntry<?>> interesting, ImmutableList<SVInstantiations.UpdateLabelPair> updateContext, ImmutableList<GenericSortCondition> genericSortConditions)
map
- the ImmMapprivate SVInstantiations(ImmutableMap<SchemaVariable,InstantiationEntry<?>> map, ImmutableMap<SchemaVariable,InstantiationEntry<?>> interesting, ImmutableList<SVInstantiations.UpdateLabelPair> updateContext, GenericSortInstantiations genericSortInstantiations, ImmutableList<GenericSortCondition> genericSortConditions)
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 toprivate SVInstantiations checkSorts(SchemaVariable p_sv, InstantiationEntry<?> p_entry, boolean p_forceRebuild, Services services)
private SVInstantiations checkCondition(GenericSortCondition p_c, boolean p_forceRebuild, Services services)
private SVInstantiations rebuildSorts(Services services)
public 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)