de.uka.ilkd.key.rule

Class AbstractBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

Direct Known Subclasses:

AbstractAuxiliaryContractBuiltInRuleApp, AbstractContractRuleApp, CloseAfterMergeRuleBuiltInRuleApp, DefaultBuiltInRuleApp, LoopApplyHeadBuiltInRuleApp, LoopInvariantBuiltInRuleApp, MergeRuleBuiltInRuleApp, RuleAppSMT

public abstract class AbstractBuiltInRuleApp
extends java.lang.Object
implements IBuiltInRuleApp

Field Summary

Fields

Modifier and Type	Field and Description
protected BuiltInRule	builtInRule
protected ImmutableList<PosInOccurrence>	ifInsts
protected PosInOccurrence	pio

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio)
protected	AbstractBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts)

Method Summary

Modifier and Type	Method and Description
boolean	complete() returns true if all variables are instantiated
ImmutableList<Goal>	execute(Goal goal, Services services) applies the specified rule at the specified position if all schema variables have been instantiated
AbstractBuiltInRuleApp	forceInstantiate(Goal goal)
java.util.List<LocationVariable>	getHeapContext()
ImmutableList<PosInOccurrence>	ifInsts()
boolean	isSufficientlyComplete() returns true if tryToInstantiate may be able to complete the app
PosInOccurrence	posInOccurrence() returns the PositionInOccurrence (representing a SequentFormula and a position in the corresponding formula) of this rule application
abstract AbstractBuiltInRuleApp	replacePos(PosInOccurrence newPos)
BuiltInRule	rule() returns the rule of this rule application
abstract IBuiltInRuleApp	setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
void	setMutable(ImmutableList<PosInOccurrence> ifInsts) HACK: but strategies do not work otherwise in the moment; I need to have a closer look on what is going on there This restores the behaviour as it was before my previous commit for the moment
java.lang.String	toString()
abstract AbstractBuiltInRuleApp	tryToInstantiate(Goal goal) Tries to complete the rule application from the available information.

Methods inherited from class java.lang.Object

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

Field Detail

builtInRule

protected final BuiltInRule builtInRule

pio

protected final PosInOccurrence pio

ifInsts

protected ImmutableList<PosInOccurrence> ifInsts

Constructor Detail

AbstractBuiltInRuleApp

protected AbstractBuiltInRuleApp(BuiltInRule rule,
                                 PosInOccurrence pio,
                                 ImmutableList<PosInOccurrence> ifInsts)

AbstractBuiltInRuleApp

protected AbstractBuiltInRuleApp(BuiltInRule rule,
                                 PosInOccurrence pio)

Method Detail

setMutable

public void setMutable(ImmutableList<PosInOccurrence> ifInsts)

HACK: but strategies do not work otherwise in the moment; I need to have a closer look on what is going on there This restores the behaviour as it was before my previous commit for the moment

rule

public BuiltInRule rule()

returns the rule of this rule application

Specified by:

rule in interface IBuiltInRuleApp

Specified by:

rule in interface RuleApp

posInOccurrence

public PosInOccurrence posInOccurrence()

returns the PositionInOccurrence (representing a SequentFormula and a position in the corresponding formula) of this rule application

Specified by:

posInOccurrence in interface RuleApp

execute

public ImmutableList<Goal> execute(Goal goal,
                                   Services services)

applies the specified rule at the specified position if all schema variables have been instantiated

Specified by:

execute in interface RuleApp

Parameters:

goal - the Goal where to apply the rule

services - the Services encapsulating all java information

Returns:

list of new created goals

replacePos

public abstract AbstractBuiltInRuleApp replacePos(PosInOccurrence newPos)

Specified by:

replacePos in interface IBuiltInRuleApp

setIfInsts

public abstract IBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)

Specified by:

setIfInsts in interface IBuiltInRuleApp

ifInsts

public ImmutableList<PosInOccurrence> ifInsts()

Specified by:

ifInsts in interface IBuiltInRuleApp

tryToInstantiate

public abstract AbstractBuiltInRuleApp tryToInstantiate(Goal goal)

Description copied from interface: IBuiltInRuleApp

Tries to complete the rule application from the available information. Attention: Do neither add GUI code to the rules nor use this method directly Instead ask the implementation of the UserInterfaceControl to complete a built-in rule. Returns a complete app only if there is exactly one contract. If you want a complete app for combined contracts, use forceInstantiate instead. For an example implementation see e.g. UseOperationContractRule or UseDependencyContractRule.

Specified by:

tryToInstantiate in interface IBuiltInRuleApp

forceInstantiate

public AbstractBuiltInRuleApp forceInstantiate(Goal goal)

Specified by:

forceInstantiate in interface IBuiltInRuleApp

isSufficientlyComplete

public boolean isSufficientlyComplete()

Description copied from interface: IBuiltInRuleApp

returns true if tryToInstantiate may be able to complete the app

Specified by:

isSufficientlyComplete in interface IBuiltInRuleApp

Returns:

getHeapContext

public java.util.List<LocationVariable> getHeapContext()

Specified by:

getHeapContext in interface IBuiltInRuleApp

complete

public boolean complete()

returns true if all variables are instantiated

Specified by:

complete in interface RuleApp

Returns:

true if all variables are instantiated

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object