public class MergeRule extends java.lang.Object implements BuiltInRule
The rule is applicable if the chosen subterm has the form { x := v || ... } PHI and there are potential merge candidates.
Any rule application returned will be incomplete; completion is handled by de.uka.ilkd.key.gui.mergerule.MergeRuleCompletion.
Modifier and Type | Class and Description |
---|---|
static interface |
MergeRule.MergeRuleProgressListener |
Modifier and Type | Field and Description |
---|---|
static MergeRule |
INSTANCE |
protected static boolean |
RIGHT_SIDE_EQUIVALENCE_ONLY_SYNTACTICAL
If set to true, merge rules are expected to check the equivalence for
right sides (for preserving idempotency) only on a pure syntactical
basis.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Goal> |
apply(Goal goal,
Services services,
RuleApp ruleApp)
the rule is applied on the given goal using the
information of rule application.
|
IBuiltInRuleApp |
createApp(PosInOccurrence pio,
TermServices services) |
java.lang.String |
displayName()
returns the display name of the rule
|
static ImmutableList<MergePartner> |
findPotentialMergePartners(Goal goal,
PosInOccurrence pio)
Finds all suitable merge partners
|
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
We admit top level formulas of the form \<{ ...
|
boolean |
isApplicableOnSubTerms() |
static boolean |
isOfAdmissibleForm(Goal goal,
PosInOccurrence pio,
boolean doMergePartnerCheck)
We admit top level formulas of the form \<{ ...
|
protected MergeProcedure.ValuesMergeResult |
mergeHeaps(MergeProcedure mergeRule,
LocationVariable heapVar,
Term heap1,
Term heap2,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term distinguishingFormula,
Services services)
Merges two heaps in a zip-like procedure.
|
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> |
mergeStates(MergeProcedure mergeRule,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term programCounter,
Term distinguishingFormula,
Services services)
Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method
MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. |
Name |
name()
the name of the rule
|
java.lang.String |
toString() |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
getOrigin
public static final MergeRule INSTANCE
protected static final boolean RIGHT_SIDE_EQUIVALENCE_ONLY_SYNTACTICAL
public java.lang.String displayName()
Rule
displayName
in interface Rule
public java.lang.String toString()
toString
in class java.lang.Object
public final ImmutableList<Goal> apply(Goal goal, Services services, RuleApp ruleApp) throws RuleAbortException
Rule
apply
in interface Rule
goal
- the Goal on which to apply ruleAppservices
- the Services with the necessary information
about the java programsruleApp
- the rule application to be executedRuleAbortException
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> mergeStates(MergeProcedure mergeRule, SymbolicExecutionState state1, SymbolicExecutionState state2, Term programCounter, Term distinguishingFormula, Services services)
MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. p must be the same in both states, so it is supplied separately.
Override this method for special merge procedures.
mergeRule
- The merge procedure to use for the merge.state1
- First state to merge.state2
- Second state to merge.programCounter
- The formula \<{ ... }\> phi consisting of the common
program counter and the post condition.distinguishingFormula
- The user-specified distinguishing formula. May be null (for
automatic generation).services
- The services object.protected MergeProcedure.ValuesMergeResult mergeHeaps(MergeProcedure mergeRule, LocationVariable heapVar, Term heap1, Term heap2, SymbolicExecutionState state1, SymbolicExecutionState state2, Term distinguishingFormula, Services services)
Override this method for specialized heap merge procedures.
heapVar
- The heap variable for which the values should be merged.heap1
- The first heap term.heap2
- The second heap term.state1
- SE state for the first heap term.state2
- SE state for the second heap termservices
- The services object.distinguishingFormula
- The user-specified distinguishing formula. May be null (for
automatic generation).public boolean isApplicable(Goal goal, PosInOccurrence pio)
isApplicable
in interface BuiltInRule
goal
- Current goal.pio
- Position of selected sequent formula.public static boolean isOfAdmissibleForm(Goal goal, PosInOccurrence pio, boolean doMergePartnerCheck)
goal
- Current goal.pio
- Position of selected sequent formula.doMergePartnerCheck
- Checks for available merge partners iff this flag is set to
true.public boolean isApplicableOnSubTerms()
isApplicableOnSubTerms
in interface BuiltInRule
public IBuiltInRuleApp createApp(PosInOccurrence pio, TermServices services)
createApp
in interface BuiltInRule
public static ImmutableList<MergePartner> findPotentialMergePartners(Goal goal, PosInOccurrence pio)
goal
- Current goal to merge.pio
- Position of update-program counter formula in goal.start
- Node to start the search with.services
- The services object.Copyright © 2003-2019 The KeY-Project.