de.uka.ilkd.key.macros

Class PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy

java.lang.Object

de.uka.ilkd.key.strategy.StaticFeatureCollection

de.uka.ilkd.key.strategy.AbstractFeatureStrategy

de.uka.ilkd.key.macros.PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy

All Implemented Interfaces:

Named, Feature, Strategy

Enclosing class:

PrepareInfFlowContractPreBranchesMacro

protected class PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy
extends AbstractFeatureStrategy

This strategy accepts all rule apps for which the rule name starts with a string in the admitted set and rejects everything else.

Field Summary

Fields

Modifier and Type	Field and Description
private Name	NAME

Constructor Summary

Constructors

Constructor and Description
RemovePostStrategy(Proof proof)

Method Summary

Modifier and Type	Method and Description
RuleAppCost	computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal) Evaluate the cost of a RuleApp.
private java.lang.String	getAppRuleName(Node parent)
protected RuleAppCost	instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal)
boolean	isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) Re-Evaluate a RuleApp.
boolean	isStopAtFirstNonCloseableGoal() Checks if the Strategy should stop at the first non closeable Goal.
Name	name() returns the name of this element

Methods inherited from class de.uka.ilkd.key.strategy.AbstractFeatureStrategy

bindRuleSet, bindRuleSet, bindRuleSet, bindRuleSet, clearRuleSetBindings, clearRuleSetBindings, disableInstantiate, enableInstantiate, forEach, getFilterFor, getHeuristic, getProof, ifHeuristics, ifHeuristics, ifHeuristics, instantiate, instantiate, instantiateApp, instantiateTriggeredVariable, oneOf, oneOf

Methods inherited from class de.uka.ilkd.key.strategy.StaticFeatureCollection

add, add, add, add, add, any, applyTF, applyTF, applyTFNonStrict, applyTFNonStrict, atomSmallerThan, blockContractExternalFeature, blockContractInternalFeature, c, contains, countOccurrences, eq, eq, eq, extendsTrans, ifZero, ifZero, ifZero, ifZero, implicitCastNecessary, inftyConst, inftyTermConst, instOf, instOfNonStrict, instOfTriggerVariable, isInstantiated, isSubSortFeature, isTriggerVariableInstantiated, leq, less, let, literalsSmallerThan, longConst, longTermConst, loopContractApplyHead, loopContractExternalFeature, loopContractInternalFeature, loopInvFeature, mergeRuleFeature, methodSpecFeature, monSmallerThan, not, not, op, opSub, opSub, opTerm, opTerm, opTerm, or, or, or, or, or, println, querySpecFeature, rec, sequentContainsNoPrograms, sub, sub, sub, subAt, sum, termSmallerThan

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.strategy.Strategy

updateStrategySettings

Field Detail

NAME

private final Name NAME

Constructor Detail

RemovePostStrategy

public RemovePostStrategy(Proof proof)

Method Detail

name

public Name name()

Description copied from interface: Named

returns the name of this element

Returns:

the name of the element

computeCost

public RuleAppCost computeCost(RuleApp ruleApp,
                               PosInOccurrence pio,
                               Goal goal)

Description copied from interface: Feature

Evaluate the cost of a RuleApp.

Parameters:

ruleApp - the RuleApp

pio - position where app is to be applied

goal - the goal on which app is to be applied

Returns:

the cost of the rule application expressed as a RuleAppCost object. TopRuleAppCost.INSTANCE indicates that the rule shall not be applied at all (it is discarded by the strategy).

isApprovedApp

public boolean isApprovedApp(RuleApp app,
                             PosInOccurrence pio,
                             Goal goal)

Description copied from interface: Strategy

Re-Evaluate a RuleApp. This method is called immediately before a rule is really applied

Returns:

true iff the rule should be applied, false otherwise

getAppRuleName

private java.lang.String getAppRuleName(Node parent)

instantiateApp

protected RuleAppCost instantiateApp(RuleApp app,
                                     PosInOccurrence pio,
                                     Goal goal)

Specified by:

instantiateApp in class AbstractFeatureStrategy

isStopAtFirstNonCloseableGoal

public boolean isStopAtFirstNonCloseableGoal()

Description copied from interface: Strategy

Checks if the Strategy should stop at the first non closeable Goal.

Returns:

true stop, false continue on other Goals.