public class MergeRuleBuiltInRuleApp extends AbstractBuiltInRuleApp
MergeProcedure
to be used
have been set by the corresponding setter function.builtInRule, ifInsts, pio
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) |
execute, forceInstantiate, getHeapContext, ifInsts, isSufficientlyComplete, posInOccurrence, rule, setMutable, toString
public MergeRuleBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio)
protected MergeRuleBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts)
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)
public AbstractBuiltInRuleApp replacePos(PosInOccurrence newPos)
replacePos
in interface IBuiltInRuleApp
replacePos
in class AbstractBuiltInRuleApp
public IBuiltInRuleApp setIfInsts(ImmutableList<PosInOccurrence> ifInsts)
setIfInsts
in interface IBuiltInRuleApp
setIfInsts
in class AbstractBuiltInRuleApp
public AbstractBuiltInRuleApp tryToInstantiate(Goal goal)
IBuiltInRuleApp
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
.tryToInstantiate
in interface IBuiltInRuleApp
tryToInstantiate
in class AbstractBuiltInRuleApp
public boolean complete()
AbstractBuiltInRuleApp
complete
in interface RuleApp
complete
in class AbstractBuiltInRuleApp
public ImmutableList<MergePartner> getMergePartners()
public void setMergePartners(ImmutableList<MergePartner> mergePartners)
public MergeProcedure getConcreteRule()
public void setConcreteRule(MergeProcedure concreteRule)
public Node getMergeNode()
public void setMergeNode(Node mergeNode)
public void setDistinguishingFormula(Term distForm)
public Term getDistinguishingFormula()
public SymbolicExecutionStateWithProgCnt getMergeSEState()
public ImmutableList<SymbolicExecutionState> getMergePartnerStates()
public void registerProgressListener(MergeRule.MergeRuleProgressListener listener)
public void clearProgressListeners()
public boolean removeProgressListener(MergeRule.MergeRuleProgressListener listener)
public void fireProgressChange(int progress)
Copyright © 2003-2019 The KeY-Project.