de.uka.ilkd.key.strategy

Class QueueRuleApplicationManager

java.lang.Object

de.uka.ilkd.key.strategy.QueueRuleApplicationManager

All Implemented Interfaces:

NewRuleListener, AutomatedRuleApplicationManager

public class QueueRuleApplicationManager
extends java.lang.Object
implements AutomatedRuleApplicationManager

Implementation of AutomatedRuleApplicationManager that stores possible RuleApps in a priority queue. The element with highest priority in the queue can be obtained via next(). This operation will remove the element from the queue. The priority of a given RuleApp corresponds to its RuleAppCost. A RuleApp can be equipped with a RuleAppCost by converting it into a RuleAppContainer. The cost of a RuleApp is computed according to a given Strategy (see Feature.computeCost(RuleApp, PosInOccurrence, Goal)).

Field Summary

Fields

Modifier and Type	Field and Description
private Goal	goal The goal this manager belongs to.
private RuleApp	nextRuleApp The next automatic RuleApp determined by the strategy.
private long	nextRuleTime
private RuleAppContainer	previousMinimum The minimum RuleAppContainer from a previous round.
private ImmutableHeap<RuleAppContainer>	queue Priority queue containing all RuleAppContainers that are candidates for application on a Goal.

Constructor Summary

Constructors

Constructor and Description
QueueRuleApplicationManager()

Method Summary

Modifier and Type	Method and Description
void	clearCache() Clear the heap of applicable rules
private void	clearNextRuleApp()
java.lang.Object	clone()
private void	computeNextRuleApp(ImmutableHeap<RuleAppContainer> furtherAppsQueue) Helper method for peekNext().
AutomatedRuleApplicationManager	copy()
private void	ensureQueueExists() Add all rules to the heap that are not reported via the RuleListener connection
RuleApp	next()
RuleApp	peekNext()
private ImmutableHeap<RuleAppContainer>	push(java.util.Iterator<RuleAppContainer> it, ImmutableHeap<RuleAppContainer> sourceQueue) Add a number of new rule apps to the heap
private ImmutableHeap<RuleAppContainer>	push(RuleAppContainer c, ImmutableHeap<RuleAppContainer> sourceQueue) Add a new rule app to the heap, provided that the rule app is not infinitely expensive
void	ruleAdded(RuleApp rule, PosInOccurrence pos) Implementation of the method from NewRuleListener.
void	rulesAdded(ImmutableList<? extends RuleApp> rules, PosInOccurrence pos) Implementation of the method from NewRuleListener.
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

goal

private Goal goal

The goal this manager belongs to.

queue

private ImmutableHeap<RuleAppContainer> queue

Priority queue containing all RuleAppContainers that are candidates for application on a Goal.

previousMinimum

private RuleAppContainer previousMinimum

The minimum RuleAppContainer from a previous round. It is taken out of queue temporarily and is put back in during the next round. After all, the corresponding rule still needs to be taken into consideration for future rule applications.

nextRuleApp

private RuleApp nextRuleApp

The next automatic RuleApp determined by the strategy. Aka result of methods next() and peekNext().

nextRuleTime

private long nextRuleTime

Constructor Detail

QueueRuleApplicationManager

public QueueRuleApplicationManager()

Method Detail

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

clearCache

public void clearCache()

Clear the heap of applicable rules

Specified by:

clearCache in interface AutomatedRuleApplicationManager

ensureQueueExists

private void ensureQueueExists()

Add all rules to the heap that are not reported via the RuleListener connection

ruleAdded

public void ruleAdded(RuleApp rule,
                      PosInOccurrence pos)

Implementation of the method from NewRuleListener. The new rule app is added to the heap

Specified by:

ruleAdded in interface NewRuleListener

rulesAdded

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

Implementation of the method from NewRuleListener. The new rule app is added to the heap

Specified by:

rulesAdded in interface NewRuleListener

push

private ImmutableHeap<RuleAppContainer> push(java.util.Iterator<RuleAppContainer> it,
                                             ImmutableHeap<RuleAppContainer> sourceQueue)

Add a number of new rule apps to the heap

push

private ImmutableHeap<RuleAppContainer> push(RuleAppContainer c,
                                             ImmutableHeap<RuleAppContainer> sourceQueue)

Add a new rule app to the heap, provided that the rule app is not infinitely expensive

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 first applicable rule app, i.e. the least expensive element of the heap that is not obsolete

clearNextRuleApp

private void clearNextRuleApp()

computeNextRuleApp

private void computeNextRuleApp(ImmutableHeap<RuleAppContainer> furtherAppsQueue)

Helper method for peekNext(). Searches for the next rule application, at which the iteration includes all rule app containers that are contained either in primary or secondary queue.

copy

public AutomatedRuleApplicationManager copy()

Specified by:

copy in interface AutomatedRuleApplicationManager

clone

public java.lang.Object clone()

Overrides:

clone in class java.lang.Object