de.uka.ilkd.key.rule.label

Class FormulaTermLabelMerger

java.lang.Object

de.uka.ilkd.key.rule.label.FormulaTermLabelMerger

All Implemented Interfaces:

TermLabelMerger

public class FormulaTermLabelMerger
extends java.lang.Object
implements TermLabelMerger

The TermLabelMerger used to merge FormulaTermLabels.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
FormulaTermLabelMerger()

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.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

FormulaTermLabelMerger

public FormulaTermLabelMerger()

Method Detail

mergeLabels

public 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.

Specified by:

mergeLabels in interface TermLabelMerger

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.