de.uka.ilkd.key.strategy

Class FocussedRuleApplicationManager

java.lang.Object

de.uka.ilkd.key.strategy.FocussedRuleApplicationManager

All Implemented Interfaces:

NewRuleListener, AutomatedRuleApplicationManager, DelegationBasedAutomatedRuleApplicationManager

public class FocussedRuleApplicationManager
extends java.lang.Object
implements DelegationBasedAutomatedRuleApplicationManager

A rule app manager that ensures that rules are only applied to a certain subterm within the proof (within a goal). The real work is delegated to a second manager (delegate pattern), this class only filters rule applications

Field Summary

Fields

Modifier and Type	Field and Description
private AutomatedRuleApplicationManager	delegate
private FormulaTag	focussedFormula
private PosInOccurrence	focussedSubterm
private Goal	goal
private boolean	onlyModifyFocussedFormula
QueueRuleApplicationManager	rootManager

Constructor Summary

Constructors

Modifier	Constructor and Description
private	FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate, Goal goal, FormulaTag focussedFormula, PosInOccurrence focussedSubterm, boolean onlyModifyFocussedFormula)
	FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate, Goal goal, PosInOccurrence focussedSubterm)

Method Summary

Modifier and Type	Method and Description
void	clearCache() Clear existing caches of applicable rules
java.lang.Object	clone()
AutomatedRuleApplicationManager	copy()
AutomatedRuleApplicationManager	getDelegate()
private PosInOccurrence	getPIOForFocussedSubterm()
private boolean	isBelow(PosInOccurrence over, PosInOccurrence under)
protected boolean	isRuleApplicationForFocussedFormula(RuleApp rule, PosInOccurrence pos)
private boolean	isSameFormula(PosInOccurrence pio1, PosInOccurrence pio2)
RuleApp	next()
RuleApp	peekNext()
void	ruleAdded(RuleApp rule, PosInOccurrence pos) Called when a new RuleApp is added
void	rulesAdded(ImmutableList<? extends RuleApp> rules, PosInOccurrence pos) Called when a collection of new RuleApps is added
void	setGoal(Goal p_goal) Set the goal this is the rule app manager for

Methods inherited from class java.lang.Object

equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

delegate

private final AutomatedRuleApplicationManager delegate

rootManager

public final QueueRuleApplicationManager rootManager

focussedFormula

private final FormulaTag focussedFormula

focussedSubterm

private final PosInOccurrence focussedSubterm

goal

private Goal goal

onlyModifyFocussedFormula

private boolean onlyModifyFocussedFormula

Constructor Detail

FocussedRuleApplicationManager

private FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate,
                                       Goal goal,
                                       FormulaTag focussedFormula,
                                       PosInOccurrence focussedSubterm,
                                       boolean onlyModifyFocussedFormula)

FocussedRuleApplicationManager

public FocussedRuleApplicationManager(AutomatedRuleApplicationManager delegate,
                                      Goal goal,
                                      PosInOccurrence focussedSubterm)

Method Detail

clearCache

public void clearCache()

Description copied from interface: AutomatedRuleApplicationManager

Clear existing caches of applicable rules

Specified by:

clearCache in interface AutomatedRuleApplicationManager

copy

public AutomatedRuleApplicationManager copy()

Specified by:

copy in interface AutomatedRuleApplicationManager

clone

public java.lang.Object clone()

Overrides:

clone in class java.lang.Object

peekNext

public RuleApp peekNext()

Specified by:

peekNext in interface AutomatedRuleApplicationManager

Returns:

the first applicable rule app, i.e. the least expensive element of the heap that is not obsolete and caches the result of this operation to save some time the next time the method nextAndCache() or next() is called. A call of next() empties the cache again.

next

public RuleApp next()

Specified by:

next in interface AutomatedRuleApplicationManager

Returns:

the next rule that is supposed to be applied

setGoal

public void setGoal(Goal p_goal)

Description copied from interface: AutomatedRuleApplicationManager

Set the goal this is the rule app manager for

Specified by:

setGoal in interface AutomatedRuleApplicationManager

ruleAdded

public void ruleAdded(RuleApp rule,
                      PosInOccurrence pos)

Description copied from interface: NewRuleListener

Called when a new RuleApp is added

Specified by:

ruleAdded in interface NewRuleListener

isRuleApplicationForFocussedFormula

protected boolean isRuleApplicationForFocussedFormula(RuleApp rule,
                                                      PosInOccurrence pos)

rulesAdded

public void rulesAdded(ImmutableList<? extends RuleApp> rules,
                       PosInOccurrence pos)

Description copied from interface: NewRuleListener

Called when a collection of new RuleApps is added

Specified by:

rulesAdded in interface NewRuleListener

isSameFormula

private boolean isSameFormula(PosInOccurrence pio1,
                              PosInOccurrence pio2)

getPIOForFocussedSubterm

private PosInOccurrence getPIOForFocussedSubterm()

isBelow

private boolean isBelow(PosInOccurrence over,
                        PosInOccurrence under)

getDelegate

public AutomatedRuleApplicationManager getDelegate()

Specified by:

getDelegate in interface DelegationBasedAutomatedRuleApplicationManager

Returns:

The delegate.