de.uka.ilkd.key.rule.merge

Class MergeRuleBuiltInRuleApp

java.lang.Object

de.uka.ilkd.key.rule.AbstractBuiltInRuleApp

de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp

All Implemented Interfaces:

IBuiltInRuleApp, RuleApp

public class MergeRuleBuiltInRuleApp
extends AbstractBuiltInRuleApp

Rule application class for merge rule applications. Is complete iff the mergePartners field as well as the concrete MergeProcedure to be used have been set by the corresponding setter function.

Author:

Dominic Scheurer

Field Summary

Fields

Modifier and Type	Field and Description
private MergeProcedure	concreteRule
private Term	distForm
private Node	mergeNode
private ImmutableList<MergePartner>	mergePartners
private ImmutableList<SymbolicExecutionState>	mergePartnerStates
private java.util.ArrayList<MergeRule.MergeRuleProgressListener>	progressListeners
private SymbolicExecutionStateWithProgCnt	thisSEState

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

builtInRule, ifInsts, pio

Constructor Summary

Constructors

Modifier	Constructor and Description
	MergeRuleBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio)
protected	MergeRuleBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts)
	MergeRuleBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts, Node mergeNode, ImmutableList<MergePartner> mergePartners, MergeProcedure concreteRule, SymbolicExecutionStateWithProgCnt thisSEState, ImmutableList<SymbolicExecutionState> mergePartnerStates, Term distForm, java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners)

Method Summary

Modifier and Type	Method and Description
void	clearProgressListeners()
boolean	complete() returns true if all variables are instantiated
private boolean	distinguishablePathConditionsRequirement()
void	fireProgressChange(int progress)
MergeProcedure	getConcreteRule()
Term	getDistinguishingFormula()
Node	getMergeNode()
ImmutableList<MergePartner>	getMergePartners()
ImmutableList<SymbolicExecutionState>	getMergePartnerStates()
SymbolicExecutionStateWithProgCnt	getMergeSEState()
void	registerProgressListener(MergeRule.MergeRuleProgressListener listener)
boolean	removeProgressListener(MergeRule.MergeRuleProgressListener listener)
AbstractBuiltInRuleApp	replacePos(PosInOccurrence newPos)
void	setConcreteRule(MergeProcedure concreteRule)
void	setDistinguishingFormula(Term distForm)
IBuiltInRuleApp	setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
void	setMergeNode(Node mergeNode)
void	setMergePartners(ImmutableList<MergePartner> mergePartners)
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

mergeNode

private Node mergeNode

mergePartners

private ImmutableList<MergePartner> mergePartners

concreteRule

private MergeProcedure concreteRule

thisSEState

private SymbolicExecutionStateWithProgCnt thisSEState

mergePartnerStates

private ImmutableList<SymbolicExecutionState> mergePartnerStates

distForm

private Term distForm

progressListeners

private java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners

Constructor Detail

MergeRuleBuiltInRuleApp

public MergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
                               PosInOccurrence pio)

MergeRuleBuiltInRuleApp

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

MergeRuleBuiltInRuleApp

public MergeRuleBuiltInRuleApp(BuiltInRule rule,
                               PosInOccurrence pio,
                               ImmutableList<PosInOccurrence> ifInsts,
                               Node mergeNode,
                               ImmutableList<MergePartner> mergePartners,
                               MergeProcedure concreteRule,
                               SymbolicExecutionStateWithProgCnt thisSEState,
                               ImmutableList<SymbolicExecutionState> mergePartnerStates,
                               Term distForm,
                               java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners)

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

distinguishablePathConditionsRequirement

private boolean distinguishablePathConditionsRequirement()

getMergePartners

public ImmutableList<MergePartner> getMergePartners()

setMergePartners

public void setMergePartners(ImmutableList<MergePartner> mergePartners)

getConcreteRule

public MergeProcedure getConcreteRule()

setConcreteRule

public void setConcreteRule(MergeProcedure concreteRule)

getMergeNode

public Node getMergeNode()

setMergeNode

public void setMergeNode(Node mergeNode)

setDistinguishingFormula

public void setDistinguishingFormula(Term distForm)

getDistinguishingFormula

public Term getDistinguishingFormula()

getMergeSEState

public SymbolicExecutionStateWithProgCnt getMergeSEState()

getMergePartnerStates

public ImmutableList<SymbolicExecutionState> getMergePartnerStates()

registerProgressListener

public void registerProgressListener(MergeRule.MergeRuleProgressListener listener)

clearProgressListeners

public void clearProgressListeners()

removeProgressListener

public boolean removeProgressListener(MergeRule.MergeRuleProgressListener listener)

fireProgressChange

public void fireProgressChange(int progress)