public class CloseAfterMergeRuleBuiltInRuleApp extends AbstractBuiltInRuleApp
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 |
builtInRule, ifInsts, pio
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) |
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.
|
execute, forceInstantiate, getHeapContext, ifInsts, isSufficientlyComplete, posInOccurrence, rule, setMutable, toString
private Node partnerNode
private Node correspondingMergeNode
private SymbolicExecutionState mergeNodeState
private SymbolicExecutionState partnerState
private Term pc
private java.util.Set<Name> newNames
public CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio, Node thePartnerNode, Node correspondingMergeNode, SymbolicExecutionState mergeNodeState, SymbolicExecutionState partnerState, Term pc, java.util.Set<Name> newNames)
public CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule, PosInOccurrence pio)
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 Node getThePartnerNode()
public void setThePartnerNode(Node thePartnerNode)
public Node getCorrespondingMergeNode()
public void setCorrespondingMergeNode(Node correspondingMergeNode)
public SymbolicExecutionState getMergeState()
public void setMergeNodeState(SymbolicExecutionState mergeState)
public SymbolicExecutionState getPartnerSEState()
public void setPartnerState(SymbolicExecutionState thisSEState)
public Term getPc()
public void setPc(Term pc)
public java.util.Set<Name> getNewNames()
public void setNewNames(java.util.Set<Name> newNames)