| java.lang.Object
 de.uka.ilkd.key.rule.inst.SVInstantiations
| SVInstantiations | | public class SVInstantiations (Code) | | This class wraps a MapFromSchemaVariableToInstantiationEntry and is used to
store instantiations of schemavariables. The class is immutable, this means
changing its content will result in creating a new object.
|
| Method Summary | |
| public SVInstantiations | add(SchemaVariable sv, Term subst)
adds the given pair to the instantiations. | | public SVInstantiations | add(OperatorSV sv, de.uka.ilkd.key.logic.op.Operator op)
| | public SVInstantiations | add(SchemaVariable sv, ProgramElement pe, int instantiationType)
| | public SVInstantiations | add(SchemaVariable sv, ProgramList pes)
| | public SVInstantiations | add(SchemaVariable sv, ProgramElement pe)
adds the given pair to the instantiations. | | public SVInstantiations | add(PosInProgram prefix, PosInProgram postfix, ExecutionContext activeStatementContext, ProgramElement pe)
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. | | public SVInstantiations | add(SchemaVariable sv, InstantiationEntry entry)
adds the given pair to the instantiations. | | public SVInstantiations | add(GenericSortCondition p_c)
| | public SVInstantiations | addInteresting(SchemaVariable sv, Term subst)
| | public SVInstantiations | addInteresting(SchemaVariable sv, Name name)
| | public SVInstantiations | addInteresting(SchemaVariable sv, ProgramElement pe)
| | public SVInstantiations | addInteresting(SchemaVariable sv, InstantiationEntry entry)
| | public SVInstantiations | addInterestingList(SchemaVariable sv, Object[] list)
| | public SVInstantiations | addList(SchemaVariable sv, Object[] list)
| | public SVInstantiations | addUpdate(Term update)
| | public SVInstantiations | addUpdateList(ListOfUpdatePair updates)
| | public SVInstantiations | clearUpdateContext()
| | public boolean | equals(Object obj)
| | public ContextInstantiationEntry | getContextInstantiation()
| | public ExecutionContext | getExecutionContext()
| | public ListOfGenericSortCondition | getGenericSortConditions()
| | public GenericSortInstantiations | getGenericSortInstantiations()
| | public Object | getInstantiation(SchemaVariable sv)
| | public InstantiationEntry | getInstantiationEntry(SchemaVariable sv)
| | public Term | getTermInstantiation(SchemaVariable sv, ExecutionContext ec, Services services)
returns the instantiation of the given SchemaVariable as Term. | | public ListOfUpdatePair | getUpdateContext()
| | public int | hashCode()
| | public MapFromSchemaVariableToInstantiationEntry | interesting()
| | public boolean | isInstantiated(SchemaVariable sv)
| | public EntryOfSchemaVariableAndInstantiationEntry | lookupEntryForSV(Name name)
| | public Object | lookupValue(Name name)
| | public SchemaVariable | lookupVar(Name name)
| | public SVInstantiations | makeInteresting(SchemaVariable sv)
| | public IteratorOfEntryOfSchemaVariableAndInstantiationEntry | pairIterator()
| | public SVInstantiations | replace(SchemaVariable sv, InstantiationEntry entry)
replaces the given pair in the instantiations. | | public SVInstantiations | replace(SchemaVariable sv, Term term)
replaces the given pair in the instantiations. | | public SVInstantiations | replace(SchemaVariable sv, ProgramElement pe)
replaces the given pair in the instantiations. | | public SVInstantiations | replace(SchemaVariable sv, ArrayOfProgramElement pes)
replaces the given pair in the instantiations. | | public SVInstantiations | replace(PosInProgram prefix, PosInProgram postfix, ExecutionContext activeStatementContext, ProgramElement pe)
replaces the given pair in the instantiations. | | public int | size()
| | public IteratorOfSchemaVariable | svIterator()
| | public String | toString()
| | public SVInstantiations | union(SVInstantiations other)
|
| EMPTY_SVINSTANTIATIONS | | final public static SVInstantiations EMPTY_SVINSTANTIATIONS(Code) | | the empty instantiation
|
| add | | public SVInstantiations add(SchemaVariable sv, Term subst)(Code) | | adds the given pair to the instantiations. If the given SchemaVariable
has been instantiated already, the new pair is taken without a warning.
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
subst - the Term the SchemaVariable is instantiated with SVInstantiations the new SVInstantiations containing the givenpair |
| add | | public SVInstantiations add(SchemaVariable sv, ProgramElement pe)(Code) | | adds the given pair to the instantiations. If the given
SchemaVariable has been instantiated already, the new pair is
taken without a warning.
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
pe - the ProgramElement the SchemaVariable is instantiated with SVInstantiations the new SVInstantiations containingthe given pair |
| add | | public SVInstantiations add(PosInProgram prefix, PosInProgram postfix, ExecutionContext activeStatementContext, ProgramElement pe)(Code) | | 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.
Parameters:
prefix - the PosInProgram describing the prefix
Parameters:
postfix - the PosInProgram describing the postfix
Parameters:
activeStatementContext - the ExecutionContext of the first active statement
Parameters:
pe - the ProgramElement the context positions are related to SVInstantiations the new SVInstantiations containing the givenpair |
| add | | public SVInstantiations add(SchemaVariable sv, InstantiationEntry entry)(Code) | | adds the given pair to the instantiations. If the given SchemaVariable
has been instantiated already, the new pair is taken without a warning.
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
entry - the InstantiationEntry SVInstantiations the new SVInstantiations containing the givenpair |
| equals | | public boolean equals(Object obj)(Code) | | returns true if the given object and this one have the same mappings
true if the given object and this one have the same mappings |
| getContextInstantiation | | public ContextInstantiationEntry getContextInstantiation()(Code) | | returns the instantiation entry for the context "schema variable" or null
if non such exists
|
| getGenericSortConditions | | public ListOfGenericSortCondition getGenericSortConditions()(Code) | | |
| getInstantiation | | public Object getInstantiation(SchemaVariable sv)(Code) | | returns the instantiation of the given SchemaVariable
the Object the SchemaVariable will be instantiated with, null ifno instantiation is stored |
| getInstantiationEntry | | public InstantiationEntry getInstantiationEntry(SchemaVariable sv)(Code) | | returns the instantiation of the given SchemaVariable
the InstantiationEntry the SchemaVariable will be instantiatedwith, null if no instantiation is stored |
| getTermInstantiation | | public Term getTermInstantiation(SchemaVariable sv, ExecutionContext ec, Services services)(Code) | | returns the instantiation of the given SchemaVariable as Term. If the
instantiation is a program element it is tried to convert it to a term
otherwise an exception is thrown
the Object the SchemaVariable will be instantiated with, null ifno instantiation is stored |
| getUpdateContext | | public ListOfUpdatePair getUpdateContext()(Code) | | returns the update context
the update context |
| hashCode | | public int hashCode()(Code) | | |
| interesting | | public MapFromSchemaVariableToInstantiationEntry interesting()(Code) | | |
| isInstantiated | | public boolean isInstantiated(SchemaVariable sv)(Code) | | returns true iff the sv has been instantiated already
true iff the sv has been instantiated already |
| lookupEntryForSV | | public EntryOfSchemaVariableAndInstantiationEntry lookupEntryForSV(Name name)(Code) | | |
| pairIterator | | public IteratorOfEntryOfSchemaVariableAndInstantiationEntry pairIterator()(Code) | | returns iterator of the mapped pair (SchemaVariables, InstantiationEntry)
the IteratorOfEntryOfSchemaVariableAndInstantiationEntry |
| replace | | public SVInstantiations replace(SchemaVariable sv, InstantiationEntry entry)(Code) | | replaces the given pair in the instantiations. If the given
SchemaVariable has been instantiated already, the new pair is taken
without a warning.
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
entry - the InstantiationEntry the SchemaVariable is instantiated with |
| replace | | public SVInstantiations replace(SchemaVariable sv, Term term)(Code) | | replaces the given pair in the instantiations. If the given
SchemaVariable has been instantiated already, the new pair is taken
without a warning.
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
term - the Term the SchemaVariable is instantiated with |
| replace | | public SVInstantiations replace(SchemaVariable sv, ProgramElement pe)(Code) | | replaces the given pair in the instantiations. If the given
SchemaVariable has been instantiated already, the new pair is taken
without a warning.
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
pe - the ProgramElement the SchemaVariable is instantiated with |
| replace | | public SVInstantiations replace(SchemaVariable sv, ArrayOfProgramElement pes)(Code) | | replaces the given pair in the instantiations. If the given
SchemaVariable has been instantiated already, the new pair is taken
without a warning.
Parameters:
sv - the SchemaVariable to be instantiated
Parameters:
pes - the ArrayOfProgramElement the SchemaVariable is instantiatedwith |
| replace | | public SVInstantiations replace(PosInProgram prefix, PosInProgram postfix, ExecutionContext activeStatementContext, ProgramElement pe)(Code) | | replaces the given pair in the instantiations. If the context has been
instantiated already, the new pair is taken without a warning.
Parameters:
prefix - the PosInProgram describing the position of the firststatement after the prefix
Parameters:
postfix - the PosInProgram describing the position of the statement justbefore the postfix
Parameters:
activeStatementContext - the ExecutionContext of the first active statement
Parameters:
pe - the ProgramElement the context positions are related to |
| size | | public int size()(Code) | | returns the number of SchemaVariables of which an instantiation is known
int that is the number of SchemaVariables of which aninstantiation is known |
| svIterator | | public IteratorOfSchemaVariable svIterator()(Code) | | returns iterator of the SchemaVariables that have an instantiation
the IteratorOfSchemaVariable |
|
|