Package | Description |
---|---|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.rule.label |
Modifier and Type | Method and Description |
---|---|
ImmutableList<TermLabelPolicy> |
TermLabelManager.TermLabelConfiguration.getApplicationTermPolicies()
Returns the
TermLabelPolicy instances applied on the application term. |
ImmutableList<TermLabelPolicy> |
TermLabelManager.TermLabelConfiguration.getModalityTermPolicies()
Returns the
TermLabelPolicy instances applied on the modality term. |
Modifier and Type | Method and Description |
---|---|
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
Constructor and Description |
---|
TermLabelConfiguration(Name termLabelName,
TermLabelFactory<?> factory,
ImmutableList<TermLabelPolicy> applicationTermPolicies,
ImmutableList<TermLabelPolicy> modalityTermPolicies,
ImmutableList<ChildTermLabelPolicy> directChildTermLabelPolicies,
ImmutableList<ChildTermLabelPolicy> childAndGrandchildTermLabelPolicies,
ImmutableList<TermLabelUpdate> termLabelUpdates,
ImmutableList<TermLabelRefactoring> termLabelRefactorings,
TermLabelMerger termLabelMerger)
Constructor.
|
TermLabelConfiguration(Name termLabelName,
TermLabelFactory<?> factory,
ImmutableList<TermLabelPolicy> applicationTermPolicies,
ImmutableList<TermLabelPolicy> modalityTermPolicies,
ImmutableList<ChildTermLabelPolicy> directChildTermLabelPolicies,
ImmutableList<ChildTermLabelPolicy> childAndGrandchildTermLabelPolicies,
ImmutableList<TermLabelUpdate> termLabelUpdates,
ImmutableList<TermLabelRefactoring> termLabelRefactorings,
TermLabelMerger termLabelMerger)
Constructor.
|
Modifier and Type | Class and Description |
---|---|
class |
OriginTermLabelPolicy
Policy for
OriginTermLabel s. |
class |
PerpetualTermLabelPolicy
This policy always maintains a label.
|
class |
StayOnFormulaTermLabelPolicy
This
TermLabelPolicy maintains a FormulaTermLabel on predicates. |
class |
StayOnOperatorTermLabelPolicy
This
TermLabelPolicy maintains a TermLabel as long
the new Term has the same Operator as the
previous best matching Term from which it was created. |
Copyright © 2003-2019 The KeY-Project.