public class JoinRuleBuiltInRuleApp extends AbstractBuiltInRuleApp
Modifier and Type | Field and Description |
---|---|
private JoinProcedure |
concreteRule |
private Term |
distForm |
private Node |
joinNode |
private ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> |
joinPartners |
private ImmutableList<SymbolicExecutionState> |
joinPartnerStates |
private SymbolicExecutionStateWithProgCnt |
thisSEState |
builtInRule, ifInsts, pio
Modifier | Constructor and Description |
---|---|
|
JoinRuleBuiltInRuleApp(BuiltInRule builtInRule,
PosInOccurrence pio) |
protected |
JoinRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts) |
execute, forceInstantiate, getHeapContext, ifInsts, isSufficientlyComplete, posInOccurrence, rule, setMutable, toString
private Node joinNode
private ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> joinPartners
private JoinProcedure concreteRule
private SymbolicExecutionStateWithProgCnt thisSEState
private ImmutableList<SymbolicExecutionState> joinPartnerStates
private Term distForm
public JoinRuleBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio)
protected JoinRuleBuiltInRuleApp(BuiltInRule rule, PosInOccurrence pio, ImmutableList<PosInOccurrence> ifInsts)
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<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> getJoinPartners()
public void setJoinPartners(ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> joinPartners)
public JoinProcedure getConcreteRule()
public void setConcreteRule(JoinProcedure concreteRule)
public Node getJoinNode()
public void setJoinNode(Node joinNode)
public void setDistinguishingFormula(Term distForm)
public Term getDistinguishingFormula()
public SymbolicExecutionStateWithProgCnt getJoinSEState()
public ImmutableList<SymbolicExecutionState> getJoinPartnerStates()