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.*;
017: import de.uka.ilkd.key.rule.FindTaclet;
018: import de.uka.ilkd.key.rule.Taclet;
019: import de.uka.ilkd.key.util.LRUCache;
020:
021: /**
022: * Cache that is used for accelerating <code>TermTacletAppIndex</code>.
023: * Basically, this is a mapping from terms to objects of
024: * <code>TermTacletAppIndex</code>, following the idea that the same taclets
025: * will be applicable to an occurrence of the same term in different places.
026: *
027: * There are different categories of locations/areas in a term that have to be
028: * separated, because different taclets could be applicable. These are:
029: * <ul>
030: * <li>Toplevel in the antecedent</li>
031: * <li>Toplevel in the succedent</li>
032: * <li>Non-toplevel, but not below updates or programs and not below "bad"
033: * operators that we do not know (defined by
034: * <code>TermTacletAppIndexCacheSet.isAcceptedOperator</code>). In this case
035: * we also have to distinguish different prefixes of a position, i.e., different
036: * sets of variables that are bound above a position.</li>
037: * <li>Below updates, but not below programs. We do not cache at all in such
038: * places.</li>
039: * <li>Below programs. Again, we also have to distinguish different prefixes of
040: * a position.</li>
041: * <li>Below other "bad" operators. We do not cache at all in such places.</li>
042: * </ul>
043: *
044: * We identify these different areas with an automaton that walks
045: * from the root of a formula to a subformula or subterm, roughly following the
046: * state design pattern. The transition function is realised by the method
047: * <code>ITermTacletAppIndexCache.descend</code>.
048: */
049: public class TermTacletAppIndexCacheSet {
050:
051: /** max. entries in the backend <code>LRUCache</code> */
052: private final static int MAX_INDEX_ENTRIES = 5000;
053:
054: /**
055: * max. instances of <code>ITermTacletAppIndexCache</code> that are kept
056: * in this set (e.g., for different prefixes of quantified variables)
057: */
058: private final static int MAX_CACHE_ENTRIES = 100;
059:
060: /**
061: * we use the same backend <code>LRUCache</code> for all actual caches.
062: * This ensures that the total memory consumption of the caches is bounded
063: * (well, almost), and that different proofs and different areas within one
064: * proof compete for cache space
065: */
066: private final static Map cacheBackend = new LRUCache(
067: MAX_INDEX_ENTRIES);
068:
069: /**
070: * dummy cache that is not caching at all, and from which no other cache is
071: * reachable
072: */
073: private final static ITermTacletAppIndexCache noCache = new ITermTacletAppIndexCache() {
074: public ITermTacletAppIndexCache descend(Term t, int subtermIndex) {
075: return this ;
076: }
077:
078: public TermTacletAppIndex getIndexForTerm(Term t) {
079: return null;
080: }
081:
082: public void putIndexForTerm(Term t, TermTacletAppIndex index) {
083: }
084: };
085:
086: /**
087: * the toplevel caches for the antecedent and the succedent. These are the
088: * starting points when determining the cache for an arbitrary position
089: */
090: private final ITermTacletAppIndexCache antecCache = new TopLevelCache(
091: SLListOfQuantifiableVariable.EMPTY_LIST);
092: private final ITermTacletAppIndexCache succCache = new TopLevelCache(
093: SLListOfQuantifiableVariable.EMPTY_LIST);
094:
095: /**
096: * cache for locations that are not below updates, programs or in the scope
097: * of binders
098: */
099: private final ITermTacletAppIndexCache topLevelCacheEmptyPrefix = new TopLevelCache(
100: SLListOfQuantifiableVariable.EMPTY_LIST);
101:
102: /**
103: * caches for locations that are not below updates or programs, but in the
104: * scope of binders. this is a mapping from
105: * <code>ListOfQuantifiedVariable</code> to <code>TopLevelCache</code>
106: */
107: private final LRUCache topLevelCaches = new LRUCache(
108: MAX_CACHE_ENTRIES);
109:
110: /**
111: * cache for locations that are below updates, but not below programs or in
112: * the scope of binders
113: */
114: private final ITermTacletAppIndexCache belowUpdateCacheEmptyPrefix = new BelowUpdateCache(
115: SLListOfQuantifiableVariable.EMPTY_LIST);
116:
117: /**
118: * cache for locations that are below programs, but not in the scope of
119: * binders
120: */
121: private final ITermTacletAppIndexCache belowProgCacheEmptyPrefix = new BelowProgCache(
122: SLListOfQuantifiableVariable.EMPTY_LIST);
123:
124: /**
125: * caches for locations that are both below programs and in the scope of
126: * binders. this is a mapping from <code>ListOfQuantifiedVariable</code>
127: * to <code>BelowProgCache</code>
128: */
129: private final LRUCache belowProgCaches = new LRUCache(
130: MAX_CACHE_ENTRIES);
131:
132: ////////////////////////////////////////////////////////////////////////////
133:
134: /**
135: * @return the cache for top-level locations in the antecedent
136: */
137: public ITermTacletAppIndexCache getAntecCache() {
138: return antecCache;
139: }
140:
141: /**
142: * @return the cache for top-level locations in the succedent
143: */
144: public ITermTacletAppIndexCache getSuccCache() {
145: return succCache;
146: }
147:
148: /**
149: * @return a dummy cache that is not caching at all, and from which no other
150: * cache is reachable
151: */
152: public ITermTacletAppIndexCache getNoCache() {
153: return noCache;
154: }
155:
156: /**
157: * @return <code>true</code> iff <code>t</code> is a taclet that might
158: * possibly be cached by any of the caches of this set
159: */
160: public boolean isRelevantTaclet(Taclet t) {
161: return t instanceof FindTaclet;
162: }
163:
164: ////////////////////////////////////////////////////////////////////////////
165:
166: /**
167: * @return the cache for locations that are not below updates or programs
168: * and in the scope of binders binding <code>prefix</code> (which
169: * might be empty)
170: */
171: private ITermTacletAppIndexCache getTopLevelCache(
172: ListOfQuantifiableVariable prefix) {
173: if (prefix.isEmpty())
174: return topLevelCacheEmptyPrefix;
175: ITermTacletAppIndexCache res = (ITermTacletAppIndexCache) topLevelCaches
176: .get(prefix);
177: if (res == null) {
178: res = new TopLevelCache(prefix);
179: topLevelCaches.put(prefix, res);
180: }
181: return res;
182: }
183:
184: /**
185: * @return the cache for locations that are below programs and in the scope
186: * of binders binding <code>prefix</code> (which might be empty)
187: */
188: private ITermTacletAppIndexCache getBelowProgCache(
189: ListOfQuantifiableVariable prefix) {
190: if (prefix.isEmpty())
191: return belowProgCacheEmptyPrefix;
192: ITermTacletAppIndexCache res = (ITermTacletAppIndexCache) belowProgCaches
193: .get(prefix);
194: if (res == null) {
195: res = new BelowProgCache(prefix);
196: belowProgCaches.put(prefix, res);
197: }
198: return res;
199: }
200:
201: /**
202: * @return the cache for locations that are below updates, but not below
203: * programs, and that are in the scope of binders binding
204: * <code>prefix</code> (which might be empty)
205: */
206: private ITermTacletAppIndexCache getBelowUpdateCache(
207: ListOfQuantifiableVariable prefix) {
208: if (prefix.isEmpty())
209: return belowUpdateCacheEmptyPrefix;
210: return new BelowUpdateCache(prefix);
211: }
212:
213: /**
214: * @return <code>true</code> if the head operator of <code>t</code> is
215: * an update and <code>subtermIndex</code> is the number of the
216: * target subterm of the update
217: */
218: private boolean isUpdateTargetPos(Term t, int subtermIndex) {
219: final Operator op = t.op();
220: if (!(op instanceof IUpdateOperator))
221: return false;
222:
223: final IUpdateOperator updOp = (IUpdateOperator) op;
224: return subtermIndex == updOp.targetPos();
225: }
226:
227: /**
228: * @return <code>true</code> if <code>op</code> is an operator below
229: * which we are caching
230: */
231: private boolean isAcceptedOperator(Operator op) {
232: return op instanceof AccessOp || op instanceof IfThenElse
233: || op instanceof Function || op instanceof Junctor
234: || op instanceof Equality || op instanceof Quantifier
235: || op instanceof IUpdateOperator
236: || op instanceof Modality;
237: }
238:
239: ////////////////////////////////////////////////////////////////////////////
240:
241: private class TopLevelCache extends
242: PrefixTermTacletAppIndexCacheImpl {
243: public TopLevelCache(ListOfQuantifiableVariable prefix) {
244: super (prefix, cacheBackend);
245: }
246:
247: public ITermTacletAppIndexCache descend(Term t, int subtermIndex) {
248: if (isUpdateTargetPos(t, subtermIndex))
249: return getBelowUpdateCache(getExtendedPrefix(t,
250: subtermIndex));
251:
252: final Operator op = t.op();
253: if (op instanceof Modality)
254: return getBelowProgCache(getExtendedPrefix(t,
255: subtermIndex));
256:
257: if (isAcceptedOperator(op))
258: return getTopLevelCache(getExtendedPrefix(t,
259: subtermIndex));
260:
261: return noCache;
262: }
263:
264: protected String name() {
265: return "TopLevelCache" + getPrefix();
266: }
267: }
268:
269: ////////////////////////////////////////////////////////////////////////////
270:
271: private class BelowUpdateCache extends
272: PrefixTermTacletAppIndexCache {
273: public BelowUpdateCache(ListOfQuantifiableVariable prefix) {
274: super (prefix);
275: }
276:
277: public ITermTacletAppIndexCache descend(Term t, int subtermIndex) {
278: final Operator op = t.op();
279: if (op instanceof Modality)
280: return getBelowProgCache(getExtendedPrefix(t,
281: subtermIndex));
282:
283: if (isAcceptedOperator(op))
284: return getBelowUpdateCache(getExtendedPrefix(t,
285: subtermIndex));
286:
287: return noCache;
288: }
289:
290: public TermTacletAppIndex getIndexForTerm(Term t) {
291: return null;
292: }
293:
294: public void putIndexForTerm(Term t, TermTacletAppIndex index) {
295: }
296: }
297:
298: ////////////////////////////////////////////////////////////////////////////
299:
300: private class BelowProgCache extends
301: PrefixTermTacletAppIndexCacheImpl {
302: public BelowProgCache(ListOfQuantifiableVariable prefix) {
303: super (prefix, cacheBackend);
304: }
305:
306: public ITermTacletAppIndexCache descend(Term t, int subtermIndex) {
307: if (isAcceptedOperator(t.op()))
308: return getBelowProgCache(getExtendedPrefix(t,
309: subtermIndex));
310:
311: return noCache;
312: }
313:
314: protected String name() {
315: return "BelowProgCache" + getPrefix();
316: }
317: }
318:
319: }
|