final class MultiThreadedTacletIndex extends TacletIndex
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)
.TacletIndex
,
TacletIndexKit
Modifier and Type | Class and Description |
---|---|
(package private) static class |
MultiThreadedTacletIndex.TacletSetMatchTask
The callable implementing the actual matching task.
|
Modifier and Type | Field and Description |
---|---|
private static java.util.concurrent.ForkJoinPool |
execs |
antecList, noFindList, partialInstantiatedRuleApps, rwList, succList
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) |
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
|
add, add, addTaclets, allNoPosTacletApps, clone, getAntecedentTaclet, getNoFindTaclet, getPartialInstantiatedApps, getRewriteTaclet, getSuccedentTaclet, lookup, lookup, remove, removeTaclets, toNoPosTacletApp, toString
MultiThreadedTacletIndex(java.lang.Iterable<Taclet> tacletSet)
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)
public TacletIndex copy()
copy
in class TacletIndex
protected ImmutableList<NoPosTacletApp> matchTaclets(ImmutableList<NoPosTacletApp> tacletApps, RuleFilter p_filter, PosInOccurrence pos, Services services)
matchTaclets
in class TacletIndex