001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof;
012:
013: import java.util.Map;
014:
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.op.ListOfQuantifiableVariable;
017:
018: /**
019: * The abstract superclass of caches for taclet app indexes that are implemented
020: * using a common backend <code>LRUCache</code> (the backend is stored in
021: * <code>TermTacletAppIndexCacheSet</code>). The backend is accessed in a way
022: * that guarantees that two distinct instances of this class never interfere, by
023: * choosing cache keys that are specific for a particular instance of
024: * <code>PrefixTermTacletAppIndexCacheImpl</code> and cannot be created by
025: * other instances. This ensures that it is safe to use one instance of
026: * <code>LRUCache</code> for many instances of
027: * <code>PrefixTermTacletAppIndexCacheImpl</code> (different proofs, different
028: * proof branches, different locations).
029: */
030: abstract class PrefixTermTacletAppIndexCacheImpl extends
031: PrefixTermTacletAppIndexCache {
032:
033: private final Map cache;
034:
035: protected PrefixTermTacletAppIndexCacheImpl(
036: ListOfQuantifiableVariable prefix, Map cache) {
037: super (prefix);
038: this .cache = cache;
039: }
040:
041: public TermTacletAppIndex getIndexForTerm(Term t) {
042: final TermTacletAppIndex res = (TermTacletAppIndex) cache
043: .get(getQueryKey(t));
044:
045: // countAccess ( res != null );
046:
047: return res;
048: }
049:
050: private int hits = 0, total = 0;
051:
052: private void countAccess(boolean hit) {
053: ++total;
054: if (hit)
055: ++hits;
056: if (total % 1000 == 0 && total != 0) {
057: System.out.println(name() + " " + hashCode() + ", size "
058: + cache.size() + ": " + ((double) hits)
059: / (double) total);
060: }
061: }
062:
063: public void putIndexForTerm(Term t, TermTacletAppIndex index) {
064: cache.put(getNewKey(t), index);
065: }
066:
067: /**
068: * Only used for debugging purposes
069: */
070: protected abstract String name();
071:
072: /**
073: * @return a freshly created key for the term <code>t</code> that can be
074: * stored in the <code>cache</code>
075: */
076: private CacheKey getNewKey(Term t) {
077: return new CacheKey(this , t);
078: }
079:
080: /**
081: * @return a key for the term <code>t</code> that can be used for cache
082: * queries. Calling this method twice will return the same object
083: * (with different attribute values), i.e., the result is not
084: * supposed to be stored anywhere
085: */
086: private CacheKey getQueryKey(Term t) {
087: queryCacheKey.analysedTerm = t;
088: return queryCacheKey;
089: }
090:
091: private final CacheKey queryCacheKey = new CacheKey(this , null);
092:
093: private static class CacheKey {
094: private final PrefixTermTacletAppIndexCacheImpl parent;
095: public Term analysedTerm;
096:
097: public CacheKey(PrefixTermTacletAppIndexCacheImpl parent,
098: Term analysedTerm) {
099: this .parent = parent;
100: this .analysedTerm = analysedTerm;
101: }
102:
103: public boolean equals(Object obj) {
104: if (!(obj instanceof CacheKey))
105: return false;
106:
107: final CacheKey objKey = (CacheKey) obj;
108: return parent == objKey.parent
109: && analysedTerm.equals(objKey.analysedTerm);
110: }
111:
112: public int hashCode() {
113: return parent.hashCode() * 3784831
114: + analysedTerm.hashCode();
115: }
116: }
117: }
|