de.uka.ilkd.key.rule.label

Class StayOnOperatorTermLabelPolicy

java.lang.Object

de.uka.ilkd.key.rule.label.StayOnOperatorTermLabelPolicy

All Implemented Interfaces:

TermLabelPolicy

public class StayOnOperatorTermLabelPolicy
extends java.lang.Object
implements TermLabelPolicy

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.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
StayOnOperatorTermLabelPolicy()

Method Summary

Modifier and Type

Method and Description

TermLabel

keepLabel(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, TermLabel label) Decides to keep (add to term which will be created) or to drop (do not add label to new term) the given TermLabel provided by the application Term.

Methods inherited from class java.lang.Object

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

Constructor Detail

StayOnOperatorTermLabelPolicy

public StayOnOperatorTermLabelPolicy()

Method Detail

keepLabel

public TermLabel keepLabel(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,
                           TermLabel label)

Decides to keep (add to term which will be created) or to drop (do not add label to new term) the given TermLabel provided by the application Term.

Specified by:

keepLabel in interface TermLabelPolicy

Parameters:

state - The TermLabelState of the current rule application.

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.

rule - The Rule which is applied.

goal - The optional Goal on which the Term to create will be used.

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.

newTermOriginalLabels - The original TermLabels.

label - The TermLabel to decide if it should be kept or dropped.

Returns:

The TermLabel to keep which might be a different one (e.g. with changed parameters) or null if the TermLabel should be dropped.