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.
MergeRuleUtils
,
MergeTotalWeakening
,
MergeByIfThenElse
,
MergeIfThenElseAntecedent
,
MergeWithLatticeAbstraction
,
MergeWithPredicateAbstraction
,
MergeRuleCompletion
,
MergePartnerSelectionDialog
Modifier and Type | Class and Description |
---|---|
static interface |
MergeRule.MergeRuleProgressListener |
Modifier and Type | Field and Description |
---|---|
private static java.lang.String |
DISPLAY_NAME |
static MergeRule |
INSTANCE |
private static int |
MAX_UPDATE_TERM_DEPTH_FOR_CHECKING
Thresholds the maximum depth of right sides in updates for which an
equivalence proof is started.
|
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.
|
private static Name |
RULE_NAME |
private static int |
SIMPLIFICATION_TIMEOUT_MS
Time threshold in milliseconds for the automatic simplification of
formulae (side proofs are stopped after that amount of time).
|
Constructor and Description |
---|
MergeRule()
MergeRule is a Singleton class, therefore constructor only
package-wide visible. |
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 \<{ ... }\> phi and U
\<{ ... }\> phi, where U must be an update in normal form, i.e. a
parallel update of elementary updates.
|
boolean |
isApplicableOnSubTerms() |
static boolean |
isOfAdmissibleForm(Goal goal,
PosInOccurrence pio,
boolean doMergePartnerCheck)
We admit top level formulas of the form \<{ ... }\> phi and U
\<{ ... }\> phi, where U must be an update in normal form, i.e. a
parallel update of elementary updates.
|
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)
. p must be the same in both states, so it is supplied separately. |
Name |
name()
the name of the rule
|
java.lang.String |
toString() |
public static final MergeRule INSTANCE
private static final java.lang.String DISPLAY_NAME
private static final Name RULE_NAME
protected static final boolean RIGHT_SIDE_EQUIVALENCE_ONLY_SYNTACTICAL
private static final int MAX_UPDATE_TERM_DEPTH_FOR_CHECKING
private static final int SIMPLIFICATION_TIMEOUT_MS
MergeRule()
MergeRule
is a Singleton class, therefore constructor only
package-wide visible.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.