de.uka.ilkd.key.rule.label

Interface TermLabelMerger

All Known Implementing Classes:

FormulaTermLabelMerger

public interface TermLabelMerger

A TermLabelMerger is used by TermLabelManager.mergeLabels(Services, de.uka.ilkd.key.logic.SequentChangeInfo) to merge TermLabels in case a SequentFormula was rejected to be added to the resulting Sequent.

For more information about TermLabels and how they are maintained during prove read the documentation of interface TermLabel.

Author:

Martin Hentschel

See Also:

TermLabel, TermLabelManager

Method Summary

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.

Method Detail

mergeLabels

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.

Parameters:

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 TermLabels which will be visible in the resulting Sequent.

Returns:

true if the List of TermLabel was modified and false otherwise.