de.uka.ilkd.key.proof

Class MultiThreadedTacletIndex

java.lang.Object

de.uka.ilkd.key.proof.TacletIndex

de.uka.ilkd.key.proof.MultiThreadedTacletIndex

final class MultiThreadedTacletIndex
extends TacletIndex

A multi-threaded taclet index implementation. It executes method matchTaclets(ImmutableList, RuleFilter, PosInOccurrence, Services) using multiple threads (depending on the number of taclets being matched and number of available processors). Do not create this index directly. Use the TacletIndexKit.createTacletIndex() resp. TacletIndexKit.createTacletIndex(Iterable).

See Also:

TacletIndex, TacletIndexKit

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
(package private) static class	MultiThreadedTacletIndex.TacletSetMatchTask The callable implementing the actual matching task.

Field Summary

Fields

Modifier and Type	Field and Description
private static java.util.concurrent.ForkJoinPool	execs

Fields inherited from class de.uka.ilkd.key.proof.TacletIndex

antecList, noFindList, partialInstantiatedRuleApps, rwList, succList

Constructor Summary

Constructors

Modifier	Constructor and Description
(package private)	MultiThreadedTacletIndex()
private	MultiThreadedTacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList, java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList, java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList, ImmutableList<NoPosTacletApp> noFindList, java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps)
(package private)	MultiThreadedTacletIndex(java.lang.Iterable<Taclet> tacletSet)

Method Summary

Modifier and Type	Method and Description
TacletIndex	copy() copies the index
protected ImmutableList<NoPosTacletApp>	matchTaclets(ImmutableList<NoPosTacletApp> tacletApps, RuleFilter p_filter, PosInOccurrence pos, Services services) Filter the given list of taclet apps, and match their find parts at the given position of the sequent

Methods inherited from class de.uka.ilkd.key.proof.TacletIndex

add, add, addTaclets, allNoPosTacletApps, clone, getAntecedentTaclet, getNoFindTaclet, getPartialInstantiatedApps, getRewriteTaclet, getSuccedentTaclet, lookup, lookup, remove, removeTaclets, toNoPosTacletApp, toString

Methods inherited from class java.lang.Object

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

Field Detail

execs

private static java.util.concurrent.ForkJoinPool execs

Constructor Detail

MultiThreadedTacletIndex

MultiThreadedTacletIndex(java.lang.Iterable<Taclet> tacletSet)

MultiThreadedTacletIndex

MultiThreadedTacletIndex()

MultiThreadedTacletIndex

private MultiThreadedTacletIndex(java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> rwList,
                                 java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> antecList,
                                 java.util.HashMap<java.lang.Object,ImmutableList<NoPosTacletApp>> succList,
                                 ImmutableList<NoPosTacletApp> noFindList,
                                 java.util.HashSet<NoPosTacletApp> partialInstantiatedRuleApps)

Method Detail

copy

public TacletIndex copy()

copies the index

Specified by:

copy in class TacletIndex

matchTaclets

protected ImmutableList<NoPosTacletApp> matchTaclets(ImmutableList<NoPosTacletApp> tacletApps,
                                                     RuleFilter p_filter,
                                                     PosInOccurrence pos,
                                                     Services services)

Filter the given list of taclet apps, and match their find parts at the given position of the sequent

Specified by:

matchTaclets in class TacletIndex