de.uka.ilkd.key.proof

Class TermTacletAppIndexCacheSet

java.lang.Object

de.uka.ilkd.key.proof.TermTacletAppIndexCacheSet

public class TermTacletAppIndexCacheSet
extends java.lang.Object

Cache that is used for accelerating TermTacletAppIndex. Basically, this is a mapping from terms to objects of TermTacletAppIndex, following the idea that the same taclets will be applicable to an occurrence of the same term in different places. There are different categories of locations/areas in a term that have to be separated, because different taclets could be applicable. These are:

• Toplevel in the antecedent
• Toplevel in the succedent
• Non-toplevel, but not below updates or programs and not below "bad" operators that we do not know (defined by TermTacletAppIndexCacheSet.isAcceptedOperator). In this case we also have to distinguish different prefixes of a position, i.e., different sets of variables that are bound above a position.
• Below updates, but not below programs. We do not cache at all in such places.
• Below programs. Again, we also have to distinguish different prefixes of a position.
• Below other "bad" operators. We do not cache at all in such places.

We identify these different areas with an automaton that walks from the root of a formula to a subformula or subterm, roughly following the state design pattern. The transition function is realised by the method ITermTacletAppIndexCache.descend.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	TermTacletAppIndexCacheSet.BelowProgCache
private class	TermTacletAppIndexCacheSet.BelowUpdateCache
private class	TermTacletAppIndexCacheSet.TopLevelCache

Field Summary

Fields

Modifier and Type	Field and Description
private ITermTacletAppIndexCache	antecCache the toplevel caches for the antecedent and the succedent.
private ITermTacletAppIndexCache	belowProgCacheEmptyPrefix cache for locations that are below programs, but not in the scope of binders
private LRUCache<ImmutableList<QuantifiableVariable>,ITermTacletAppIndexCache>	belowProgCaches caches for locations that are both below programs and in the scope of binders. this is a mapping from IList to BelowProgCache
private ITermTacletAppIndexCache	belowUpdateCacheEmptyPrefix cache for locations that are below updates, but not below programs or in the scope of binders
private java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex>	cache
private static int	MAX_CACHE_ENTRIES max. instances of ITermTacletAppIndexCache that are kept in this set (e.g., for different prefixes of quantified variables)
private static ITermTacletAppIndexCache	noCache dummy cache that is not caching at all, and from which no other cache is reachable
private ITermTacletAppIndexCache	succCache
private ITermTacletAppIndexCache	topLevelCacheEmptyPrefix cache for locations that are not below updates, programs or in the scope of binders
private LRUCache<ImmutableList<QuantifiableVariable>,ITermTacletAppIndexCache>	topLevelCaches caches for locations that are not below updates or programs, but in the scope of binders. this is a mapping from IList to TopLevelCache

Constructor Summary

Constructors

Constructor and Description
TermTacletAppIndexCacheSet(java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache)

Method Summary

Modifier and Type	Method and Description
ITermTacletAppIndexCache	getAntecCache()
private ITermTacletAppIndexCache	getBelowProgCache(ImmutableList<QuantifiableVariable> prefix)
private ITermTacletAppIndexCache	getBelowUpdateCache(ImmutableList<QuantifiableVariable> prefix)
ITermTacletAppIndexCache	getNoCache()
ITermTacletAppIndexCache	getSuccCache()
private ITermTacletAppIndexCache	getTopLevelCache(ImmutableList<QuantifiableVariable> prefix)
private boolean	isAcceptedOperator(Operator op)
boolean	isRelevantTaclet(Taclet t)
private boolean	isUpdateTargetPos(Term t, int subtermIndex)

Methods inherited from class java.lang.Object

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

Field Detail

MAX_CACHE_ENTRIES

private static final int MAX_CACHE_ENTRIES

max. instances of ITermTacletAppIndexCache that are kept in this set (e.g., for different prefixes of quantified variables)

See Also:

Constant Field Values

noCache

private static final ITermTacletAppIndexCache noCache

dummy cache that is not caching at all, and from which no other cache is reachable

antecCache

private final ITermTacletAppIndexCache antecCache

the toplevel caches for the antecedent and the succedent. These are the starting points when determining the cache for an arbitrary position

succCache

private final ITermTacletAppIndexCache succCache

topLevelCacheEmptyPrefix

private final ITermTacletAppIndexCache topLevelCacheEmptyPrefix

cache for locations that are not below updates, programs or in the scope of binders

topLevelCaches

private final LRUCache<ImmutableList<QuantifiableVariable>,ITermTacletAppIndexCache> topLevelCaches

caches for locations that are not below updates or programs, but in the scope of binders. this is a mapping from IList to TopLevelCache

belowUpdateCacheEmptyPrefix

private final ITermTacletAppIndexCache belowUpdateCacheEmptyPrefix

cache for locations that are below updates, but not below programs or in the scope of binders

belowProgCacheEmptyPrefix

private final ITermTacletAppIndexCache belowProgCacheEmptyPrefix

cache for locations that are below programs, but not in the scope of binders

belowProgCaches

private final LRUCache<ImmutableList<QuantifiableVariable>,ITermTacletAppIndexCache> belowProgCaches

caches for locations that are both below programs and in the scope of binders. this is a mapping from IList to BelowProgCache

cache

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

Constructor Detail

TermTacletAppIndexCacheSet

public TermTacletAppIndexCacheSet(java.util.Map<PrefixTermTacletAppIndexCacheImpl.CacheKey,TermTacletAppIndex> cache)

Method Detail

getAntecCache

public ITermTacletAppIndexCache getAntecCache()

Returns:

the cache for top-level locations in the antecedent

getSuccCache

public ITermTacletAppIndexCache getSuccCache()

Returns:

the cache for top-level locations in the succedent

getNoCache

public ITermTacletAppIndexCache getNoCache()

Returns:

a dummy cache that is not caching at all, and from which no other cache is reachable

isRelevantTaclet

public boolean isRelevantTaclet(Taclet t)

Returns:

true iff t is a taclet that might possibly be cached by any of the caches of this set

getTopLevelCache

private ITermTacletAppIndexCache getTopLevelCache(ImmutableList<QuantifiableVariable> prefix)

Returns:

the cache for locations that are not below updates or programs and in the scope of binders binding prefix (which might be empty)

getBelowProgCache

private ITermTacletAppIndexCache getBelowProgCache(ImmutableList<QuantifiableVariable> prefix)

Returns:

the cache for locations that are below programs and in the scope of binders binding prefix (which might be empty)

getBelowUpdateCache

private ITermTacletAppIndexCache getBelowUpdateCache(ImmutableList<QuantifiableVariable> prefix)

Returns:

the cache for locations that are below updates, but not below programs, and that are in the scope of binders binding prefix (which might be empty)

isUpdateTargetPos

private boolean isUpdateTargetPos(Term t,
                                  int subtermIndex)

Returns:

true if the head operator of t is an update and subtermIndex is the number of the target subterm of the update

isAcceptedOperator

private boolean isAcceptedOperator(Operator op)

Returns:

true if op is an operator below which we are caching