| java.lang.Object
 de.uka.ilkd.key.proof.TermTacletAppIndexCacheSet
| TermTacletAppIndexCacheSet | | public class TermTacletAppIndexCacheSet (Code) | | 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.
|
| isRelevantTaclet | | public boolean isRelevantTaclet(Taclet t)(Code) | | true iff t is a taclet that mightpossibly be cached by any of the caches of this set |
|
|