public class JoinRule extends Object implements BuiltInRule
The rule is applicable if the chosen subterm has the form { x := v || ... } PHI and there are potential join candidates.
Any rule application returned will be incomplete; completion is handled by de.uka.ilkd.key.gui.joinrule.JoinRuleCompletion.
JoinRuleUtils
,
JoinWeaken
,
JoinIfThenElse
,
JoinIfThenElseAntecedent
,
JoinWithLatticeAbstraction
,
JoinWithSignLattice
,
JoinRuleCompletion
,
JoinPartnerSelectionDialog
Modifier and Type | Field and Description |
---|---|
private static String |
DISPLAY_NAME |
static JoinRule |
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, join 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 |
---|
JoinRule()
JoinRule 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) |
String |
displayName()
returns the display name of the rule
|
static ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> |
findPotentialJoinPartners(Goal goal,
PosInOccurrence pio)
Finds all suitable join partners.
|
static ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> |
findPotentialJoinPartners(Goal goal,
PosInOccurrence pio,
Node start)
Finds all suitable join partners below the start node.
|
boolean |
isApplicable(Goal goal,
PosInOccurrence pio)
We admit top level formulas of the form \<{ ...
|
boolean |
isApplicableOnSubTerms() |
static boolean |
isOfAdmissibleForm(Goal goal,
PosInOccurrence pio,
boolean doJoinPartnerCheck)
We admit top level formulas of the form \<{ ...
|
protected Triple<ImmutableSet<Term>,Term,ImmutableSet<Name>> |
joinHeaps(JoinProcedure joinRule,
LocationVariable heapVar,
Term heap1,
Term heap2,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term distinguishingFormula,
Services services)
Joins two heaps in a zip-like procedure.
|
protected Pair<SymbolicExecutionState,ImmutableSet<Name>> |
joinStates(JoinProcedure joinRule,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term programCounter,
Term distinguishingFormula,
Services services)
Joins two SE states (U1,C1,p) and (U2,C2,p) according to the method
JoinRule#joinValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. |
Name |
name()
the name of the rule
|
String |
toString() |
public static final JoinRule INSTANCE
private static final 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
JoinRule()
public String displayName()
Rule
displayName
in interface Rule
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 Pair<SymbolicExecutionState,ImmutableSet<Name>> joinStates(JoinProcedure joinRule, SymbolicExecutionState state1, SymbolicExecutionState state2, Term programCounter, Term distinguishingFormula, Services services)
JoinRule#joinValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. p must be the same in both states, so it is supplied separately.
Override this method for special join procedures.
joinRule
- The join procedure to use for the join.state1
- First state to join.state2
- Second state to join.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 Triple<ImmutableSet<Term>,Term,ImmutableSet<Name>> joinHeaps(JoinProcedure joinRule, LocationVariable heapVar, Term heap1, Term heap2, SymbolicExecutionState state1, SymbolicExecutionState state2, Term distinguishingFormula, Services services)
Override this method for specialized heap join procedures.
heapVar
- The heap variable for which the values should be joined.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 doJoinPartnerCheck)
goal
- Current goal.pio
- Position of selected sequent formula.doJoinPartnerCheck
- Checks for available join 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<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> findPotentialJoinPartners(Goal goal, PosInOccurrence pio)
goal
- Current goal to join.pio
- Position of update-program counter formula in goal.services
- The services object.public static ImmutableList<Triple<Goal,PosInOccurrence,HashMap<ProgramVariable,ProgramVariable>>> findPotentialJoinPartners(Goal goal, PosInOccurrence pio, Node start)
goal
- Current goal to join.pio
- Position of update-program counter formula in goal.start
- Node to start the search with.services
- The services object.