de.uka.ilkd.key.proof

Class MultiThreadedTacletIndex.TacletSetMatchTask

java.lang.Object

de.uka.ilkd.key.proof.MultiThreadedTacletIndex.TacletSetMatchTask

All Implemented Interfaces:

java.util.concurrent.Callable<java.util.List<NoPosTacletApp>>

Enclosing class:

MultiThreadedTacletIndex

static class MultiThreadedTacletIndex.TacletSetMatchTask
extends java.lang.Object
implements java.util.concurrent.Callable<java.util.List<NoPosTacletApp>>

The callable implementing the actual matching task.

Field Summary

Fields

Modifier and Type	Field and Description
private int	lower
private PosInOccurrence	pos
private RuleFilter	ruleFilter
private Services	services
private NoPosTacletApp[]	toMatch
private int	upper

Constructor Summary

Constructors

Constructor and Description
TacletSetMatchTask(NoPosTacletApp[] toMatch, int lower, int upper, PosInOccurrence pos, RuleFilter ruleFilter, Services services) Creates a task which matches all taclets in toMatch from lower including to upper excluding against the term at position pos.

Method Summary

Modifier and Type	Method and Description
java.util.List<NoPosTacletApp>	call()

Methods inherited from class java.lang.Object

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

Field Detail

toMatch

private NoPosTacletApp[] toMatch

lower

private final int lower

upper

private final int upper

services

private Services services

pos

private PosInOccurrence pos

ruleFilter

private RuleFilter ruleFilter

Constructor Detail

TacletSetMatchTask

public TacletSetMatchTask(NoPosTacletApp[] toMatch,
                          int lower,
                          int upper,
                          PosInOccurrence pos,
                          RuleFilter ruleFilter,
                          Services services)

Creates a task which matches all taclets in toMatch from lower including to upper excluding against the term at position pos. Only taclets passing the filter ruleFilter are considered

Parameters:

toMatch - the list containing the taclets to be matched

lower - the index (incl.) where to start

upper - the index (excl.) where to stop

pos - the PosInOccurrence refering to the term to match

ruleFilter - RuleFilter constraining the taclets to be matched

services - the Services

Method Detail

call

public java.util.List<NoPosTacletApp> call()

Specified by:

call in interface java.util.concurrent.Callable<java.util.List<NoPosTacletApp>>