public interface TermLabelMerger
A TermLabelMerger
is used by
TermLabelManager.mergeLabels(Services, de.uka.ilkd.key.logic.SequentChangeInfo)
to merge TermLabel
s in case a SequentFormula
was
rejected to be added to the resulting Sequent
.
For more information about TermLabel
s and how they are maintained
during prove read the documentation of interface TermLabel
.
TermLabel
,
TermLabelManager
Modifier and Type | Method and Description |
---|---|
boolean |
mergeLabels(SequentFormula existingSF,
Term existingTerm,
TermLabel existingLabel,
SequentFormula rejectedSF,
Term rejectedTerm,
TermLabel rejectedLabel,
java.util.List<TermLabel> mergedLabels)
Merges the existing and the rejected
TermLabel by updating the merged List . |
boolean mergeLabels(SequentFormula existingSF, Term existingTerm, TermLabel existingLabel, SequentFormula rejectedSF, Term rejectedTerm, TermLabel rejectedLabel, java.util.List<TermLabel> mergedLabels)
TermLabel
by updating the merged List
.existingSF
- The existing SequentFormula
.existingTerm
- The Term
of the existing SequentFormula
.existingLabel
- The existing TermLabel
if available or null
otherwise.rejectedSF
- The rejected SequentFormula
.rejectedTerm
- The Term
of the rejected SequentFormula
.rejectedLabel
- The rejected TermLabel
.mergedLabels
- The List
with new TermLabel
s which will be visible in the resulting Sequent
.true
if the List
of TermLabel
was modified and false
otherwise.