de.uka.ilkd.key.strategy

Class FocussedBreakpointRuleApplicationManager

java.lang.Object

de.uka.ilkd.key.strategy.FocussedBreakpointRuleApplicationManager

All Implemented Interfaces:

NewRuleListener, AutomatedRuleApplicationManager, DelegationBasedAutomatedRuleApplicationManager

public class FocussedBreakpointRuleApplicationManager
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 java.util.Optional<java.lang.String>	breakpoint
private AutomatedRuleApplicationManager	delegate

Constructor Summary

Constructors

Modifier	Constructor and Description
	FocussedBreakpointRuleApplicationManager(AutomatedRuleApplicationManager delegate, Goal goal, java.util.Optional<PosInOccurrence> focussedSubterm, java.util.Optional<java.lang.String> breakpoint)
private	FocussedBreakpointRuleApplicationManager(AutomatedRuleApplicationManager delegate, java.util.Optional<java.lang.String> breakpoint)

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 static boolean	isJavaPIO(PosInOccurrence pio)
private boolean	mayAddRule(RuleApp rule, PosInOccurrence pos)
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

breakpoint

private final java.util.Optional<java.lang.String> breakpoint

Constructor Detail

FocussedBreakpointRuleApplicationManager

private FocussedBreakpointRuleApplicationManager(AutomatedRuleApplicationManager delegate,
                                                 java.util.Optional<java.lang.String> breakpoint)

FocussedBreakpointRuleApplicationManager

public FocussedBreakpointRuleApplicationManager(AutomatedRuleApplicationManager delegate,
                                                Goal goal,
                                                java.util.Optional<PosInOccurrence> focussedSubterm,
                                                java.util.Optional<java.lang.String> breakpoint)

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

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

mayAddRule

private boolean mayAddRule(RuleApp rule,
                           PosInOccurrence pos)

isJavaPIO

private static boolean isJavaPIO(PosInOccurrence pio)

getDelegate

public AutomatedRuleApplicationManager getDelegate()

Specified by:

getDelegate in interface DelegationBasedAutomatedRuleApplicationManager

Returns:

The delegate.