public abstract class PrefixTermTacletAppIndexCacheImpl
extends java.lang.Object
LRUCache
(the backend is stored in
TermTacletAppIndexCacheSet
). The backend is accessed in a way
that guarantees that two distinct instances of this class never interfere, by
choosing cache keys that are specific for a particular instance of
PrefixTermTacletAppIndexCacheImpl
and cannot be created by
other instances. This ensures that it is safe to use one instance of
LRUCache
for many instances of
PrefixTermTacletAppIndexCacheImpl
(different proofs, different
proof branches, different locations).Modifier and Type | Class and Description |
---|---|
static class |
PrefixTermTacletAppIndexCacheImpl.CacheKey |
Modifier | Constructor and Description |
---|---|
protected |
PrefixTermTacletAppIndexCacheImpl(ImmutableList<QuantifiableVariable> prefix,
java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<QuantifiableVariable> |
getExtendedPrefix(ImmutableArray<QuantifiableVariable> extension) |
protected ImmutableList<QuantifiableVariable> |
getExtendedPrefix(Term t,
int subtermIndex) |
TermTacletAppIndex |
getIndexForTerm(Term t) |
protected ImmutableList<QuantifiableVariable> |
getPrefix() |
protected abstract java.lang.String |
name()
Only used for debugging purposes
|
void |
putIndexForTerm(Term t,
TermTacletAppIndex index)
Put the taclet app index
index for the term t
in the cache |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
descend
protected PrefixTermTacletAppIndexCacheImpl(ImmutableList<QuantifiableVariable> prefix, java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache)
public TermTacletAppIndex getIndexForTerm(Term t)
t
, or
null
if no index for this term was found in the
cachepublic void putIndexForTerm(Term t, TermTacletAppIndex index)
ITermTacletAppIndexCache
index
for the term t
in the cacheprotected abstract java.lang.String name()
protected ImmutableList<QuantifiableVariable> getPrefix()
protected ImmutableList<QuantifiableVariable> getExtendedPrefix(ImmutableArray<QuantifiableVariable> extension)
protected ImmutableList<QuantifiableVariable> getExtendedPrefix(Term t, int subtermIndex)
Copyright © 2003-2019 The KeY-Project.