de.uka.ilkd.key.rule.label

Class FormulaTermLabelUpdate

java.lang.Object

de.uka.ilkd.key.rule.label.FormulaTermLabelUpdate

All Implemented Interfaces:

RuleSpecificTask, TermLabelUpdate

public class FormulaTermLabelUpdate
extends java.lang.Object
implements TermLabelUpdate

The TermLabelUpdate used to label predicates with a FormulaTermLabel of add clauses which were not labeled before.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
FormulaTermLabelUpdate()

Method Summary

Modifier and Type	Method and Description
ImmutableList<Name>	getSupportedRuleNames() Returns the supported rule Names or null or an empty list if all rules are supported.
protected TermLabel	getTermLabel(java.util.Set<TermLabel> labels, Name name) Returns the TermLabel with the given Name.
void	updateLabels(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Term modalityTerm, Rule rule, RuleApp ruleApp, java.lang.Object hint, Term tacletTerm, Operator newTermOp, ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars, JavaBlock newTermJavaBlock, java.util.Set<TermLabel> labels) This method can freely add, remove or sort the given TermLabel which will be added to the new Term.

Methods inherited from class java.lang.Object

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

Constructor Detail

FormulaTermLabelUpdate

public FormulaTermLabelUpdate()

Method Detail

getSupportedRuleNames

public ImmutableList<Name> getSupportedRuleNames()

Returns the supported rule Names or null or an empty list if all rules are supported.

Specified by:

getSupportedRuleNames in interface RuleSpecificTask

Returns:

The list of supported rule Names or null/empty list if all rules are supported.

updateLabels

public void updateLabels(TermLabelState state,
                         Services services,
                         PosInOccurrence applicationPosInOccurrence,
                         Term applicationTerm,
                         Term modalityTerm,
                         Rule rule,
                         RuleApp ruleApp,
                         java.lang.Object hint,
                         Term tacletTerm,
                         Operator newTermOp,
                         ImmutableArray<Term> newTermSubs,
                         ImmutableArray<QuantifiableVariable> newTermBoundVars,
                         JavaBlock newTermJavaBlock,
                         java.util.Set<TermLabel> labels)

This method can freely add, remove or sort the given TermLabel which will be added to the new Term.

Specified by:

updateLabels in interface TermLabelUpdate

Parameters:

state - The TermLabelState of the current rule application. return true keep TermLabel and add it to the new Term. false drop TermLabel and do not need it to the new Term.

services - The Services used by the Proof on which a Rule is applied right now.

applicationPosInOccurrence - The PosInOccurrence in the previous Sequent which defines the Term that is rewritten.

applicationTerm - The Term defined by the PosInOccurrence in the previous Sequent.

modalityTerm - The optional modality Term.

rule - The Rule which is applied.

ruleApp - The RuleApp which is currently performed.

hint - An optional hint passed from the active rule to describe the term which should be created.

tacletTerm - The optional Term in the taclet which is responsible to instantiate the new Term for the new proof node or null in case of built in rules.

newTermOp - The new Operator of the Term to create.

newTermSubs - The optional children of the Term to create.

newTermBoundVars - The optional QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

labels - The Set of TermLabels to modify.

getTermLabel

protected TermLabel getTermLabel(java.util.Set<TermLabel> labels,
                                 Name name)

Returns the TermLabel with the given Name.

Parameters:

labels - the TermLabels to search in.

name - The Name of the TermLabel to search.

Returns:

The found TermLabel or null if no element was found.