de.uka.ilkd.key.rule.merge

Class CloseAfterMergeRuleBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.merge.CloseAfterMergeRuleBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

public class CloseAfterMergeRuleBuiltInRuleApp
extends AbstractBuiltInRuleApp

Rule application class for close-after-merge rule applications.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private Node	correspondingMergeNode
private SymbolicExecutionState	mergeNodeState
private java.util.Set<Name>	newNames
private Node	partnerNode
private SymbolicExecutionState	partnerState
private Term	pc

Fields inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Constructor and Description
CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio)
CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio, Node thePartnerNode, Node correspondingMergeNode, SymbolicExecutionState mergeNodeState, SymbolicExecutionState partnerState, Term pc, java.util.Set<Name> newNames)

Method Summary

Modifier and Type	Method and Description
boolean	complete() returns true if all variables are instantiated
Node	getCorrespondingMergeNode()
SymbolicExecutionState	getMergeState()
java.util.Set<Name>	getNewNames()
SymbolicExecutionState	getPartnerSEState()
Term	getPc()
Node	getThePartnerNode()
AbstractBuiltInRuleApp	replacePos(PosInOccurrence newPos)
void	setCorrespondingMergeNode(Node correspondingMergeNode)
IBuiltInRuleApp	setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
void	setMergeNodeState(SymbolicExecutionState mergeState)
void	setNewNames(java.util.Set<Name> newNames)
void	setPartnerState(SymbolicExecutionState thisSEState)
void	setPc(Term pc)
void	setThePartnerNode(Node thePartnerNode)
AbstractBuiltInRuleApp	tryToInstantiate(Goal goal) Tries to complete the rule application from the available information.

Methods inherited from class de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

execute, forceInstantiate, getHeapContext, ifInsts, isSufficientlyComplete, posInOccurrence, rule, setMutable, toString

Methods inherited from class java.lang.Object

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

Field Detail

partnerNode

private Node partnerNode

correspondingMergeNode

private Node correspondingMergeNode

mergeNodeState

private SymbolicExecutionState mergeNodeState

partnerState

private SymbolicExecutionState partnerState

pc

private Term pc

newNames

private java.util.Set<Name> newNames

Constructor Detail

CloseAfterMergeRuleBuiltInRuleApp

public CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
                                         PosInOccurrence pio,
                                         Node thePartnerNode,
                                         Node correspondingMergeNode,
                                         SymbolicExecutionState mergeNodeState,
                                         SymbolicExecutionState partnerState,
                                         Term pc,
                                         java.util.Set<Name> newNames)

CloseAfterMergeRuleBuiltInRuleApp

public CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
                                         PosInOccurrence pio)

Method Detail

replacePos

public AbstractBuiltInRuleApp replacePos(PosInOccurrence newPos)

Specified by:

replacePos in interface IBuiltInRuleApp

Specified by:

replacePos in class AbstractBuiltInRuleApp

setIfInsts

public IBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)

Specified by:

setIfInsts in interface IBuiltInRuleApp

Specified by:

setIfInsts in class AbstractBuiltInRuleApp

tryToInstantiate

public 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

Specified by:

tryToInstantiate in class AbstractBuiltInRuleApp

complete

public boolean complete()

Description copied from class: AbstractBuiltInRuleApp

returns true if all variables are instantiated

Specified by:

complete in interface RuleApp

Overrides:

complete in class AbstractBuiltInRuleApp

Returns:

true if all variables are instantiated

getThePartnerNode

public Node getThePartnerNode()

setThePartnerNode

public void setThePartnerNode(Node thePartnerNode)

getCorrespondingMergeNode

public Node getCorrespondingMergeNode()

setCorrespondingMergeNode

public void setCorrespondingMergeNode(Node correspondingMergeNode)

getMergeState

public SymbolicExecutionState getMergeState()

setMergeNodeState

public void setMergeNodeState(SymbolicExecutionState mergeState)

getPartnerSEState

public SymbolicExecutionState getPartnerSEState()

setPartnerState

public void setPartnerState(SymbolicExecutionState thisSEState)

getPc

public Term getPc()

setPc

public void setPc(Term pc)

getNewNames

public java.util.Set<Name> getNewNames()

setNewNames

public void setNewNames(java.util.Set<Name> newNames)