public class MergeRuleBuiltInRuleApp extends AbstractBuiltInRuleApp
MergeProcedure
to be used
have been set by the corresponding setter function.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 |
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
private Node mergeNode
private ImmutableList<MergePartner> mergePartners
private MergeProcedure concreteRule
private SymbolicExecutionStateWithProgCnt thisSEState
private ImmutableList<SymbolicExecutionState> mergePartnerStates
private Term distForm
private java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners
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
private boolean distinguishablePathConditionsRequirement()
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)