de.uka.ilkd.key.proof

Class PrefixTermTacletAppIndexCacheImpl

java.lang.Object

de.uka.ilkd.key.proof.PrefixTermTacletAppIndexCache

de.uka.ilkd.key.proof.PrefixTermTacletAppIndexCacheImpl

All Implemented Interfaces:

ITermTacletAppIndexCache

Direct Known Subclasses:

TermTacletAppIndexCacheSet.BelowProgCache, TermTacletAppIndexCacheSet.TopLevelCache

public abstract class PrefixTermTacletAppIndexCacheImpl
extends PrefixTermTacletAppIndexCache

The abstract superclass of caches for taclet app indexes that are implemented using a common backend 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).

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	PrefixTermTacletAppIndexCacheImpl.CacheKey

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex>	cache
private int	hits
private PrefixTermTacletAppIndexCacheImpl.CacheKey	queryCacheKey
private int	total

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	PrefixTermTacletAppIndexCacheImpl(ImmutableList<QuantifiableVariable> prefix, java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache)

Method Summary

Modifier and Type	Method and Description
private void	countAccess(boolean hit)
TermTacletAppIndex	getIndexForTerm(Term t)
private PrefixTermTacletAppIndexCacheImpl.CacheKey	getNewKey(Term t)
private PrefixTermTacletAppIndexCacheImpl.CacheKey	getQueryKey(Term t)
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

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

getExtendedPrefix, getExtendedPrefix, getPrefix

Methods inherited from class java.lang.Object

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

Methods inherited from interface de.uka.ilkd.key.proof.ITermTacletAppIndexCache

descend

Field Detail

cache

private final java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache

hits

private int hits

total

private int total

queryCacheKey

private final PrefixTermTacletAppIndexCacheImpl.CacheKey queryCacheKey

Constructor Detail

PrefixTermTacletAppIndexCacheImpl

protected PrefixTermTacletAppIndexCacheImpl(ImmutableList<QuantifiableVariable> prefix,
                                            java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache)

Method Detail

getIndexForTerm

public TermTacletAppIndex getIndexForTerm(Term t)

Returns:

the taclet app index for the term t, or null if no index for this term was found in the cache

countAccess

private void countAccess(boolean hit)

putIndexForTerm

public void putIndexForTerm(Term t,
                            TermTacletAppIndex index)

Description copied from interface: ITermTacletAppIndexCache

Put the taclet app index index for the term t in the cache

name

protected abstract java.lang.String name()

Only used for debugging purposes

getNewKey

private PrefixTermTacletAppIndexCacheImpl.CacheKey getNewKey(Term t)

Returns:

a freshly created key for the term t that can be stored in the cache

getQueryKey

private PrefixTermTacletAppIndexCacheImpl.CacheKey getQueryKey(Term t)

Returns:

a key for the term t that can be used for cache queries. Calling this method twice will return the same object (with different attribute values), i.e., the result is not supposed to be stored anywhere